ImageSymbolsProofDefs.lean🔗

Tier 2 · definitions used by the symbolic proof 1 headline theorem depend on it 18 of 56 lines trusted source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

No theorem of the theorem folders uses this file: only headline theorems stated in proof files do. The tier tables do not count it, and its trust banner refers to the theorems of the theorem folders.

Declarations on this page (11)

Proof-side cryptographic stub symbols

Defines StubSymbol constants for incremental ML-KEM-768, SHA-512 compression, and Ed25519 curve-core operations used by ExternInterpretationTotalOnUsedSymbols and extern-witness tests.

@[expose] public section

namespace DY.Libsignal.PQXDH.Refinement

open DY.Libsignal.Refinement (StubSymbol)

abbrev mlkem768FromSeedSymbol used only by headline theorems stated in proof filesL27–28 ↗#

abbrev mlkem768FromSeedSymbol : StubSymbol :=
  "<libcrux_ml_kem::mlkem768::incremental::KeyPairCompressedBytes>::from_seed"

abbrev mlkem768Encaps1Symbol used only by headline theorems stated in proof filesL30 ↗#

abbrev mlkem768Encaps1Symbol : StubSymbol := "libcrux_ml_kem::mlkem768::incremental::encapsulate1"

abbrev mlkem768Encaps2Symbol used only by headline theorems stated in proof filesL32 ↗#

abbrev mlkem768Encaps2Symbol : StubSymbol := "libcrux_ml_kem::mlkem768::incremental::encapsulate2"

abbrev mlkem768ValidatePkSymbol used only by headline theorems stated in proof filesL34–35 ↗#

abbrev mlkem768ValidatePkSymbol : StubSymbol :=
  "libcrux_ml_kem::mlkem768::incremental::validate_pk_bytes"

abbrev mlkem768DecapsSymbol used only by headline theorems stated in proof filesL37–38 ↗#

abbrev mlkem768DecapsSymbol : StubSymbol :=
  "libcrux_ml_kem::mlkem768::incremental::decapsulate_compressed_key"

abbrev sha512CompressSymbol used only by headline theorems stated in proof filesL40 ↗#

abbrev sha512CompressSymbol : StubSymbol := "sha2::sha512::compress512"

abbrev edwardsCompressSymbol used only by headline theorems stated in proof filesL42 ↗#

abbrev edwardsCompressSymbol : StubSymbol := "<curve25519_dalek::edwards::EdwardsPoint>::compress"

abbrev edwardsNegSymbol used only by headline theorems stated in proof filesL44–45 ↗#

abbrev edwardsNegSymbol : StubSymbol :=
  "<curve25519_dalek::edwards::EdwardsPoint as core::ops::arith::Neg>::neg"

abbrev doubleScalarMulSymbol used only by headline theorems stated in proof filesL47–48 ↗#

abbrev doubleScalarMulSymbol : StubSymbol :=
  "<curve25519_dalek::edwards::EdwardsPoint>::vartime_double_scalar_mul_basepoint"

abbrev scalarModOrderSymbol used only by headline theorems stated in proof filesL50–51 ↗#

abbrev scalarModOrderSymbol : StubSymbol :=
  "<curve25519_dalek::scalar::Scalar>::from_bytes_mod_order"

abbrev scalarModOrderWideSymbol used only by headline theorems stated in proof filesL53–54 ↗#

abbrev scalarModOrderWideSymbol : StubSymbol :=
  "<curve25519_dalek::scalar::Scalar>::from_bytes_mod_order_wide"

end DY.Libsignal.PQXDH.Refinement