Hooks.lean
Trusted in part. Only the CliElfLib theorems of {Computational,Symbolic}/ use this file (headlineδ does not; see Computational/); they unfold only these 10: libcruxHmacName, mlkemDecapsName, mlkemEncaps1Name, mlkemEncaps2Name, mlkemFromSeedName, mlkemPk1Name, mlkemPk2Name, mlkemValidatePkName, tokenName, tokenStorageName.
Defines the symbol names, image offsets, and Spec contracts (mlkemFromSeedSpec, mlkemPk1Spec, mlkemPk2Spec, mlkemEncaps1Spec, mlkemEncaps2Spec, mlkemDecapsSpec, mlkemValidatePkSpec, libcruxHmacSpec, plus onceCallName) bundled as SpqrHooks, together with TokenInit (tokenStorageOff, tokenOnceOff), which fixes the CPU feature-detection cells so that spqr takes the unaccelerated software $\mathrm{GF}(2^{16})$ path (DEV-SPQR1). Guards.lean verifies all symbol and stub offsets against the linked image.
@[expose] public sectionnamespace CryptoVerification.LibsignalSpqrV1open Arm64 ProofLib CryptoGames CryptoGames.HMAC CryptoGames.LibsignalSessionopen CryptoVerification.RustHeap CryptoVerification.LibsignalSessionRepropen CryptoVerification.LibsignalTripleRatchet18 declarations not shown (lines 42–86): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification.
2. TOKEN & STORAGE. (TokenInit)
abbrev tokenStorageName
spqr::encoding::gf::check_accelerated::use_accelerated::STORAGE. (0x9a038), a 1-byte AtomicU8 storing whether PMULL-accelerated GF(2¹⁶) multiplication is enabled (0#8 = false, 1#8 = true, 0xff#8 = uninitialized).
abbrev tokenStorageName : String :=
"spqr::encoding::gf::check_accelerated::use_accelerated::STORAGE.0"2 declarations not shown (lines 95–96): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification.
abbrev tokenName
spqr::encoding::gf::check_accelerated::TOKEN (0x9a040), a 16-byte std::sync::LazyLock<InitToken> whose std::sys::sync::once::futex::Once AtomicU32 state word resides at offset +8 (0x9a048, 0#32 = COMPLETE).
abbrev tokenName : String :=
"spqr::encoding::gf::check_accelerated::TOKEN"22 declarations not shown (lines 103–358): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., …
end CryptoVerification.LibsignalSpqrV1