Secure Messaging

Blueprint Summary🔗

Overview
Total entries23completed: 0; deps incomplete: 0; sorries: 0; no proof: 14
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)
  • rkem_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 22downstream unlocks: 22
Entry index (23)
Definitions9completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Theorems14completed: 0; deps incomplete: 0; sorries: 0; no proof: 14
Informal-only entries23
Definition Index (9)
Theorem / Proposition / Lemma / Corollary Index (14)
By parent groups (5)
RKEM from DDH (FS). (3)
Katana RKEM (optimised). (3)
Katana RKEM (plain). (3)
RKEM from KEM. (3)
RKEM from DDH (non-FS). (2)
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)
  • rkem_scheme(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 22proof uses: 0direct uses: 22downstream unlocks: 22
  • rkem_correctness(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
  • rkem_ratchet_sim(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
  • rkem_forward_security(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
  • optimised_katana_rkem_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  • plain_katana_rkem_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  • rkem_from_ddh_fs_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  • rkem_from_kem_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  • rkem_from_ddh_nonfs_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Group health (6)
  • Ratcheting Key Encapsulation Mechanism (RKEM).rkem
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 1blocked: 3incomplete Lean: 0unlock score: 36
    Next: rkem_scheme stage: statementdownstream unlocks: 22
  • Katana RKEM (optimised).rkem_katana_rkem_optimised
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • Katana RKEM (plain).rkem_katana_rkem_plain
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • RKEM from DDH (FS).rkem_rkem_from_ddh_fs
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • RKEM from KEM.rkem_rkem_from_kem
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • RKEM from DDH (non-FS).rkem_rkem_from_ddh_non_fs
    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 owner23
Missing effort23
Untagged23
Missing owner (23)
Missing effort (23)
Untagged (23)
Structure and coverage
Informal-only23Statements with no associated Lean code yet.
Heaviest prerequisites (22)
  • optimised_katana_rkem_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • optimised_katana_rkem_forward_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • optimised_katana_rkem_ratchet_sim(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • plain_katana_rkem_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • plain_katana_rkem_forward_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • plain_katana_rkem_ratchet_sim(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • rkem_from_ddh_fs_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • rkem_from_ddh_fs_forward_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • rkem_from_ddh_fs_ratchet_sim(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • rkem_from_ddh_nonfs_correctness(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • Show all 12 more heaviest-prerequisite entries
    • rkem_from_ddh_nonfs_ratchet_sim(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • rkem_from_kem_correctness(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • rkem_from_kem_forward_security(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • rkem_from_kem_ratchet_sim(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • optimised_katana_rkem_spec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
    • plain_katana_rkem_spec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
    • rkem_correctness(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 5
    • rkem_forward_security(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 4
    • rkem_from_ddh_fs_spec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
    • rkem_from_ddh_nonfs_spec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    • rkem_from_kem_spec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
    • rkem_ratchet_sim(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 5
No prerequisites (1)
No dependents (14)