Secure Messaging

Blueprint Summary🔗

Overview
Total entries17completed: 13; deps incomplete: 0; sorries: 0; no proof: 3
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed13Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Missing informal coverage3Entries with Lean code but missing an informal statement or proof block.
Ready next (1)
  • frodo_kem_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
Missing informal coverage (3)
Entry index (17)
Definitions11completed: 10; deps incomplete: 0; sorries: 0; no proof: 0
Theorems6completed: 3; deps incomplete: 0; sorries: 0; no proof: 3
Informal-only entries4
Definition Index (11)
Theorem / Proposition / Lemma / Corollary Index (6)
By parent groups (3)
Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (3)
FrodoKEM, a Learning-With-Errors key encapsulation mechanism ( ). (2)
Incremental KEM from ML-KEM. (1)
Dependency insights
Statement-used entries9Entries reused in statement dependencies.
Tracked parent groups6Grouped health rollups for parents with more than one child entry.
Most used in statements (9)
Group health (6)
  • Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203).ml_kem
    Grouped view over entries sharing the same parent.
    total: 5closed: 4local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 8
    Next: no ready child currently unlocks downstream work.
  • FrodoKEM, a Learning-With-Errors key encapsulation mechanism ( ).frodo_kem
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 2
    Next: frodo_kem_scheme stage: statementdownstream unlocks: 2
  • Online-Offline Key Encapsulation Mechanism (On-Off KEM).on_off_kem
    Grouped view over entries sharing the same parent.
    total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 13
    Next: no ready child currently unlocks downstream work.
  • Incremental Key Encapsulation Mechanism (Incremental KEM).incremental_kem
    Grouped view over entries sharing the same parent.
    total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • On-Off KEM from K-PKE.on_off_kem_from_kpke
    Grouped view over entries sharing the same parent.
    total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • Incremental KEM from ML-KEM.incremental_kem_incremental_kem_from_ml_kem
    Grouped view over entries sharing the same parent.
    total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner17
Missing effort17
Untagged17
Missing owner (17)
Missing effort (17)
Untagged (17)
Structure and coverage
Informal-only4Statements with no associated Lean code yet.
Fully closed13Local code and ancestor closure are both complete.
Heaviest prerequisites (13)
No prerequisites (4)
No dependents (8)