Trusted in part. The theorems of the default library (Computational/Theorems/ outside CliElfLib) use only ServiceIdParser, UuidParser, addrBytes, hyphenatedLength, kindByte, pniPrefix, serviceIdParse, tryParseHyphenated, utf8, uuidTryParse, hexNibble, decodeHex, decodeHex32, parseSimple, hyphen, parseHyphenated, urnPrefix from this file: read them. To trust the theorems of Computational/Theorems/Main.lean (CliElfLib), also read errTag. Everything else here is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

This file gives the separation-logic predicates that say how the Rust values the triple-ratchet entry points (LibsignalBinary/Specifications/LibsignalTripleRatchet.lean) read and write are laid out in memory, relating bytes to the session model (LibsignalBinary/Specifications/CryptoGames/Ratchet/LibsignalSession.lean). It extends LibsignalBinary/Specifications/LibsignalSessionRepr.lean (whose predicates it reuses: chainAt, messageKeyAt, optChainKeyAt, VecGhost, VecPin, ...). The trusted part is the pure address-parsing model: uuidTryParse (uuid 1.26.1's Uuid::try_parse), serviceIdParse (libsignal's ServiceId::parse_from_service_id_string) and the per-address bytes addrBytes, from which serializeAddresses builds the sender / recipient address bytes.

Every layout fact below was read off the disassembly of the session image; the evidence is cited by instruction offset at each definition. Independently, a Rust replica of the types (110 const assertions compiled by rustc 1.98.1 for aarch64-unknown-linux-gnu) confirms every offset, size and niche, including the fields no instruction touches. The niche choices (-1 for a single-niche Option, -2 for Result<Vec<u8>, SPE>::Ok, 2^63 + i for the SPE) depend on the rustc version: rerun the replica on any toolchain bump. Kernel-checked guards: issStr_lengths, macFailedStr_length, pniPrefix_word.

Glossary: SPE = SignalProtocolError (48 bytes); SS = proto::storage::SessionStructure (the payload of SessionState, 344 bytes); OTR / TR = OutgoingTripleRatchet (200 bytes) / TripleRatchet; IK = identity key; srk = sender ratchet key; pq / SPQR = the Sparse Post-Quantum Ratchet and its serialized state Vec<u8>; ISS = InvalidSessionStructure; UUID = universally unique identifier; ACI = Account Identity; PNI = Phone Number Identity; UTF-8 = 8-bit Unicode Transformation Format; LE = little-endian; RNG = random number generator; prost = the Rust protobuf (Protocol Buffers) library; niche = an invalid bit pattern of a field reused as an enum discriminant; sret = the caller-provided result buffer; Box<[u8]> = an owned byte slice (ptr, len) (no capacity word); rodata = the image's read-only data (↦ᵣ, duplicable read-only points-to).

• Option<Vec-like> (Option<Chain>, Option<chain::ChainKey>, Option<PendingPreKey>, Option<PendingKyberPreKey>, spqr::MessageKey): None = capacity word usize::MAX (noneCap). Evidence: OTR::apply_to_session_state 0xbd00: cmn x22, #1 (SS + 0x90); clear_unacknowledged_pre_key_message writes -1 to SS + 0xf8 and SS + 0x128.

• SPE: word 0 = 2^63 + variant index for every non-dataful variant (speWord).

• Result<Vec<u8>, SPE> (try_decrypt): Ok = word 0 -2 (okTagVec), the Vec at +8; Err = the SPE inline at +0. Result<T, SPE> for T = SignalMessage / OutgoingTripleRatchet: Ok = the payload at +0; Err = word 0 -1 (errTag), the SPE at +8.

alice_base_key, the registration ids, the pending pre-key's ids / timestamp, the whole pending_kyber_pre_key, and every Vec the session model does not determine (VecGhost).

• uuidTryParse (with hexNibble, decodeHex, decodeHex32, parseSimple, parseHyphenated, hyphen, urnPrefix): the model of uuid 1.26.1's Uuid::try_parse.

• serviceIdParse (with tryParseHyphenated, hyphenatedLength, pniPrefix): the model of ServiceId::parse_from_service_id_string; ServiceIdParser / UuidParser are their types.

• addrBytes, kindByte, serializeAddresses: the 36-byte sender / recipient encoding (serialize_addresses).

• utf8: a string literal's UTF-8 bytes.

• noneCap, errTag, okTagVec, speWord: the niche / tag words.

• speAt, vecResultAt, errResultAt, signalMessageResultAt, otrResultAt: an SPE and the Result buffers of the entry points.

• signalMessageAt, protocolAddressAt, sessionStateAt, otrAt: a SignalMessage, a ProtocolAddress, a SessionStructure and an OutgoingTripleRatchet in memory (with their ghost structures).

• tapeAt, tapeAfter, coinsOf, decryptDraws: the HookRng random tape and how much of it a decrypt draws.

• SessionGhost.AfterTryDecrypt, SessionGhost.AgreeExceptPq, SessionGhost.AfterOutgoingRatchetApply: how the ghost layout may change across each entry point.

Upstream: ~/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/uuid-1.26.1/src/parser.rs. Uuid::try_parse(&str) (:110–112) = try_parse_ascii(input.as_bytes()) (:136–144), which maps try_parse (:147–163) to Ok(Uuid::from_bytes(bytes)) (the 16 bytes, unchanged) or to Err(Error(ErrorKind::ParseOther)) on every failure. try_parse dispatches on the length:

• 32 bytes: parse_simple (:188–225), 32 hex digits;

• 36 bytes: parse_hyphenated (:228–278), the whole input;

• 38 bytes {…}: parse_hyphenated of the 36 bytes inside the braces (:156);

• 45 bytes urn:uuid:…: parse_hyphenated of the 36 bytes after the prefix (:157);

• any other length or shape: Err (:161). decode_hex32 (:283–322) maps '0'..='9' to 0..9 and 'a'..='f' / 'A'..='F' (via | 0x20) to 10..15, and rejects every other byte; byte j of the UUID is (nibble 2j << 4) | nibble 2j+1.

libsignal only reaches the 36-byte (hyphenated) path: try_parse_hyphenated (core/src/address.rs:264–271, tryParseHyphenated below) checks the length is hyphenatedLength = 36 before it calls Uuid::try_parse. The other shapes are modelled so that uuidTryParse is the whole function, as compiled into the image.