Secure Messaging

Blueprint Summary🔗

Overview
Total entries14completed: 13; deps incomplete: 0; sorries: 0; no proof: 1
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed13Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Missing informal coverage4Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (4)
Entry index (14)
Definitions9completed: 9; deps incomplete: 0; sorries: 0; no proof: 0
Theorems5completed: 4; deps incomplete: 0; sorries: 0; no proof: 1
Informal-only entries1
Definition Index (9)
Theorem / Proposition / Lemma / Corollary Index (5)
By parent groups (2)
Encrypt-then-MAC. (2)
GCM. (2)
Dependency insights
Statement-used entries9Entries reused in statement dependencies.
Tracked parent groups2Grouped health rollups for parents with more than one child entry.
Most used in statements (9)
Group health (2)
  • GCM.aead_gcm
    Grouped view over entries sharing the same parent.
    total: 3closed: 2local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
  • Encrypt-then-MAC.aead_encrypt_then_mac
    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 owner14
Missing effort14
Untagged14
Missing owner (14)
Missing effort (14)
Untagged (14)
Structure and coverage
Informal-only1Statements with no associated Lean code yet.
Fully closed13Local code and ancestor closure are both complete.
Heaviest prerequisites (13)
  • aead_etm_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • aead_etm_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • aead_gcm_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • aead_gcm_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  • aead_guess_dist_advantage(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • aead_security_exp(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 6
    Associated lean decls (3)
  • aead_correctness(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
  • aead_decrypt_query_bound(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
  • aead_dist_advantage(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    Associated lean decls (2)
  • aead_etm_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
  • Show all 3 more heaviest-prerequisite entries
    • aead_gcm_spec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
      Associated lean decls (1)
    • aead_guess_advantage(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • aead_oracles(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
      Associated lean decls (2)
No prerequisites (1)
No dependents (5)