The 9 extern symbols de-hooked so the linked ELF bytes execute. Stock ld.lld cutover: memcpy and memset, whose .symtab definitions in the stock link are VerifiedLibraries.mallocngLib blocks 20 / 21. Earlier F3 + IO.6b allocator/IO cutover: 7 mangled symbols, the 5 Rust global-allocator symbols (rdl_shim.S → VerifiedLibraries.mallocngLib) and read_file / read_stdin (libsignal_cli_io). (<String as Clone>::clone becomes an intra-library libsignalSessionLib block under SC-1 route (I).)

Mangled-symbol PQXDH and SPQR primitive rows (18 rows) matching libsignalSessionMultiLib, with libcrux_hmac::hmac wired over shared mallocng at placement mmpl.

Mangled-symbol CLI hook table (37 rows) matching libsignalSessionMultiLib after the F3 + IO.6b allocator/IO cutover (5 __rust_* allocator rows, <String as Clone>::clone, read_file, and read_stdin removed so the linked ELF bytes execute; aes_256_cbc_{encrypt,decrypt} and libcrux_hmac::hmac wired over VerifiedLibraries.mallocngLib at placement mmpl) and the stock ld.lld cutover (memset and memcpy removed: they run as mallocngLib blocks 21 / 20).

The 18 mangled panic extern symbols of libsignalSessionMultiLib mapped to Rust.panicked.

Mangled-symbol CLI extern map under Obj.MultiPlacedLib (libsignalSessionLib + mallocngLib placement mmpl).

Kernel-checked guard that block 617 of libsignalSessionLib exists and shares the exact externs list of main's block (with main at offset 0), ensuring cliProgPlacedSig induces the same externAt? and Step relation as main's block without pinning main's block index.

Relocatable CliRunsTo under multi-block placements (mpl, mmpl).

Relocatable cliRunAbortOnPanic under multi-block placements (mpl, mmpl).

External resolution stubVa = mpl.ρ sym reaches the .symtab definition targetVa in elf: either directly (stubVa = targetVa, stock ld.lld link) or via a 4-byte-aligned executable (Perm.rx) 1-word unconditional branch B targetVa at stubVa (--branch-stubs slot in .img.text).

Relocatable CliElfCodeMatches under libsignalSessionLib placement mpl and VerifiedLibraries.mallocngLib placement mmpl (SR-28 #3 and GK2 K2/K3):

1. libsignalSessionLib placement, in-ELF match, and writable-data disjointness (mpl);

2. VerifiedLibraries.mallocngLib placement, in-ELF match, and writable-data disjointness (mmpl);

3. K3(a): cross-library code-block and writable-data disjointness plus externAt? = none across all mallocngLib code bytes and at every de-hooked resolution mpl.ρ sym;

4. K3(b): every sym ∈ cliDehookedSymsPlaced (the 9 external de-hooked symbols) resolves to a unique defined STT_FUNC .symtab entry targetVa in elf (DirectOrBranchStub elf (mpl.ρ sym) targetVa) with externAt? targetVa = none.

The inputs of the PQXDH-mode specs at model primitives W: the inputs of the calls of CliSpecPqxdh's five clauses and of CliSpecPqxdhNoMatch, for a party state st in the domain (PqxdhPartyInSpecDomain W st):

1. init <peer> bundle with no session, any typed bundle b and the 192 coin bytes t;

2. send <peer> of a plaintext m below 2^32 bytes with the 64 coin bytes r;

3. recv <peer> of 2 ‖ c with c below 2^32 bytes;

4. recv <peer> of 3 ‖ m.bytes for a typed pre-key message m whose inner message is below 2^32 - 2048 bytes, at any session state (no session, a matching one: CliSpecPqxdh; one that does not match: CliSpecPqxdhNoMatch);

5. recv <peer> of any input c below 2^32 bytes whose first byte is neither 2 nor 3, or of nothing. In 2–5 the receive coins rc are any 32 bytes.

Run on i under (mpl, mmpl) and W reaches s.status = .OutOfMemory (brk / mmap / mprotect / mremap exhaustion) from Placed.cliTokenPatchPlaced mpl s0 (DEV-CLI10, DEV-CLI15). By determinism of Step, reaching .OutOfMemory forces Placed.cliRunPlacedSig mpl mmpl elf W i = none and excludes .Exception, .Halted, and divergence.

CliSpecPqxdh total except .OutOfMemory (DEV-CLI15). CliSpecPqxdh run X W (PqDir.lean) with each clause's conclusion run i = some e replaced by OutcomeOrExcusedAbort exc run i (· = e): on the clause's input i the run is total with exactly the clause's outcome, except when run i = none and i is excused (exc i). The five clauses are CliSpecPqxdh's (1. init, 2. send, 3. recv of 2 ‖ c, 4. recv of a typed pre-key message with no session or a matching one, 5. recv of any other first byte or of nothing), in the same order, with the same binders, hypotheses and outcomes, including the stdinCapBytes / maxPlaintextBytes rejections (DEV-CLI21). With exc := fun _ => False it is equivalent to CliSpecPqxdh run X W.

CliSpecPqxdhNoMatch total except .OutOfMemory (DEV-CLI15). CliSpecPqxdhNoMatch run X W (PqDirNoMatch.lean) with its conclusion ∃ o, run i = some o ∧ OutcomeMatchesModelExceptPath … replaced by OutcomeOrExcusedAbort exc run i …, with the same binders, hypotheses and outcomes, including the stdinCapBytes rejection (DEV-CLI21). With exc := fun _ => False it is equivalent to CliSpecPqxdhNoMatch run X W.

Relocatable CliPqxdhElfCorrect under placements (mpl, mmpl), total except .OutOfMemory (DEV-CLI15). elf matches the placed code (Placed.CliElfCodeMatchesPlaced mpl mmpl elf), and for every choice of hooks W (no hypothesis on W) and every model extras X, the process Placed.cliRunPlacedSig mpl mmpl elf W is total and meets CliSpecPqxdh and CliSpecPqxdhNoMatch at ⟨W.C, W.Q⟩ except on inputs where the run reaches .OutOfMemory (CliReachesOOMPlaced mpl mmpl elf W).

Relocatable CliPqxdhBinaryCorrect: universally quantified over every pair of multi-block placements mpl (libsignalSessionLib.LinkedAt bytes mpl) and mmpl (VerifiedLibraries.mallocngLib.LinkedAt bytes mmpl).