Secure Messaging

Blueprint Summary🔗

Overview
Total entries5completed: 0; deps incomplete: 0; sorries: 0; no proof: 2
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed0Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Ready next (1)
  • fs_aead_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 4downstream unlocks: 4
Entry index (5)
Definitions3completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Theorems2completed: 0; deps incomplete: 0; sorries: 0; no proof: 2
Informal-only entries5
Definition Index (3)
Theorem / Proposition / Lemma / Corollary Index (2)
By parent groups (1)
FS-AEAD from AEAD and PRG. (2)
Dependency insights
Statement-used entries3Entries reused in statement dependencies.
Tracked parent groups2Grouped health rollups for parents with more than one child entry.
Most used in statements (3)
  • fs_aead_scheme(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
  • fs_aead_from_aead_prg_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  • fs_aead_security(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Group health (2)
  • Forward-Secure AEAD (FS-AEAD).fs_aead
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 5
    Next: fs_aead_scheme stage: statementdownstream unlocks: 4
  • FS-AEAD from AEAD and PRG.fs_aead_fs_aead_from_aead_prg
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner5
Missing effort5
Untagged5
Missing owner (5)
Missing effort (5)
Untagged (5)
Structure and coverage
Informal-only5Statements with no associated Lean code yet.
Heaviest prerequisites (4)
  • fs_aead_from_aead_prg_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
  • fs_aead_from_aead_prg_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • fs_aead_from_aead_prg_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
  • fs_aead_security(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
No prerequisites (1)
No dependents (2)