Secure Messaging

Blueprint Summary🔗

Overview
Total entries27completed: 0; deps incomplete: 0; sorries: 0; no proof: 16
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed0Local code and prerequisite closure are both complete.
Actionable priorities3Entries ready now and already unlocking downstream work.
Ready next (3)
Entry index (27)
Definitions11completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Theorems16completed: 0; deps incomplete: 0; sorries: 0; no proof: 16
Informal-only entries27
Definition Index (11)
Theorem / Proposition / Lemma / Corollary Index (16)
By parent groups (4)
Triple Ratchet SM. (4)
Double Ratchet SM - Signal. (4)
Double Ratchet SM - Abstract. (4)
SCKA SM. (4)
Dependency insights
Statement-used entries22Entries reused in statement dependencies.
Tracked parent groups5Grouped health rollups for parents with more than one child entry.
Most used in statements (22)
Group health (5)
  • Double Ratchet.secure_messaging_double_ratchet
    Grouped view over entries sharing the same parent.
    total: 5closed: 0local-only: 0ready: 1blocked: 4incomplete Lean: 0unlock score: 17
    Next: secure_messaging_double_ratchet_scheme stage: statementdownstream unlocks: 14
  • SCKA SM.secure_messaging_scka
    Grouped view over entries sharing the same parent.
    total: 6closed: 0local-only: 0ready: 1blocked: 5incomplete Lean: 0unlock score: 12
    Next: secure_messaging_scka_scheme stage: statementdownstream unlocks: 5
  • Triple Ratchet SM.secure_messaging_triple_ratchet
    Grouped view over entries sharing the same parent.
    total: 6closed: 0local-only: 0ready: 1blocked: 5incomplete Lean: 0unlock score: 12
    Next: secure_messaging_triple_ratchet_scheme stage: statementdownstream unlocks: 5
  • Double Ratchet SM - Abstract.secure_messaging_abstract_protocol_double_ratchet
    Grouped view over entries sharing the same parent.
    total: 5closed: 0local-only: 0ready: 0blocked: 5incomplete Lean: 0unlock score: 18
    Next: no ready child currently unlocks downstream work.
  • Double Ratchet SM - Signal.secure_messaging_signal_protocol_double_ratchet
    Grouped view over entries sharing the same parent.
    total: 5closed: 0local-only: 0ready: 0blocked: 5incomplete Lean: 0unlock score: 7
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner27
Missing effort27
Untagged27
Missing owner (27)
Missing effort (27)
Untagged (27)
Structure and coverage
Informal-only27Statements with no associated Lean code yet.
Heaviest prerequisites (24)
  • secure_messaging_triple_ratchet_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 5proof deps: 0direct uses: 4downstream unlocks: 4
  • secure_messaging_abstract_double_ratchet_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • secure_messaging_abstract_double_ratchet_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 5downstream unlocks: 9
  • secure_messaging_double_ratchet_security(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • secure_messaging_scka_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • secure_messaging_scka_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 4
  • secure_messaging_signal_double_ratchet_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • secure_messaging_signal_double_ratchet_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 4
  • secure_messaging_triple_ratchet_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • secure_messaging_signal_double_ratchet_authenticity(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  • Show all 14 more heaviest-prerequisite entries
No prerequisites (3)
No dependents (5)