Secure Messaging

Blueprint Summary🔗

Overview
Total entries15completed: 12; deps incomplete: 0; sorries: 0; no proof: 2
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed12Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Missing informal coverage4Entries with Lean code but missing an informal statement or proof block.
Ready next (1)
  • cka_from_lwe_spec(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
Missing informal coverage (4)
Entry index (15)
Definitions9completed: 8; deps incomplete: 0; sorries: 0; no proof: 0
Theorems6completed: 4; deps incomplete: 0; sorries: 0; no proof: 2
Informal-only entries3
Definition Index (9)
Theorem / Proposition / Lemma / Corollary Index (6)
By parent groups (3)
CKA from KEM. (2)
CKA from DDH. (2)
CKA from LWE. (2)
Dependency insights
Statement-used entries8Entries reused in statement dependencies.
Tracked parent groups3Grouped health rollups for parents with more than one child entry.
Most used in statements (8)
Group health (3)
  • CKA from LWE.cka_cka_from_lwe
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 2
    Next: cka_from_lwe_spec stage: statementdownstream unlocks: 2
  • CKA from DDH.cka_cka_from_ddh
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 5
    Next: no ready child currently unlocks downstream work.
  • CKA from KEM.cka_cka_from_kem
    Grouped view over entries sharing the same parent.
    total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner15
Missing effort15
Untagged15
Missing owner (15)
Missing effort (15)
Untagged (15)
Structure and coverage
Informal-only3Statements with no associated Lean code yet.
Fully closed12Local code and ancestor closure are both complete.
Heaviest prerequisites (14)
No prerequisites (1)
No dependents (7)