Blueprint Summary
Overview
Total entries149completed: 88; deps incomplete: 0; sorries: 0; no proof: 40
Ready now19Entries with an actionable next formalization step.
Fully closed88Local code and prerequisite closure are both complete.
Actionable priorities9Entries ready now and already unlocking downstream work.
Missing informal coverage23Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (9)
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
-
Ready for statement work.
Missing informal coverage (23)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Entry index (149)
Definitions86completed: 65; deps incomplete: 0; sorries: 0; no proof: 0
Theorems63completed: 23; deps incomplete: 0; sorries: 0; no proof: 40
Informal-only entries61
Definition Index (86)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (7)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (8)
-
ErasureCode.ReedSolomon.Parameters -
ErasureCode.ReedSolomon.Parameters.sourceIndex -
ErasureCode.ReedSolomon.Parameters.sourcePoint -
ErasureCode.ReedSolomon.Parameters.encodingPolynomial -
ErasureCode.ReedSolomon.Parameters.encode -
ErasureCode.ReedSolomon.Parameters.decodingPolynomial -
ErasureCode.ReedSolomon.Parameters.decode -
ErasureCode.ReedSolomon.Parameters.erasureCode
-
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (8)
-
ErasureCodePayload.Streaming.EncoderState -
ErasureCodePayload.Streaming.EncoderState.init -
ErasureCodePayload.Streaming.EncoderState.nextChunk -
ErasureCodePayload.Streaming.DecoderState -
ErasureCodePayload.Streaming.DecoderState.empty -
ErasureCodePayload.Streaming.DecoderState.addChunk -
ErasureCodePayload.Streaming.DecoderState.decodedPayload -
ErasureCodePayload.Streaming.DecoderState.hasMessage
-
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (16)
-
CKAScheme.GameState -
CKAScheme.GameParams -
CKAScheme.isChallengeEpoch -
CKAScheme.allowCorrPCS -
CKAScheme.allowCorrFS -
CKAScheme.allowCorr -
CKAScheme.oracleSendA -
CKAScheme.oracleSendB -
CKAScheme.oracleSendArleak -
CKAScheme.oracleSendBrleak -
CKAScheme.oracleRecvA -
CKAScheme.oracleRecvB -
CKAScheme.oracleChallA -
CKAScheme.oracleChallB -
CKAScheme.oracleCorruptA -
CKAScheme.oracleCorruptB
-
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (17)
-
SCKAScheme.VulnerableEpochs -
SCKAScheme.GameState -
SCKAScheme.oracleSendA -
SCKAScheme.oracleSendB -
SCKAScheme.oracleSendArleak -
SCKAScheme.oracleSendBrleak -
SCKAScheme.oracleRecvA -
SCKAScheme.oracleRecvB -
SCKAScheme.oracleChall -
SCKAScheme.oracleCorruptA -
SCKAScheme.oracleCorruptB -
SCKAScheme.sckaCorrectnessSpec -
SCKAScheme.sckaCorrectnessImpl -
SCKAScheme.SCKACorrectnessAdversary -
SCKAScheme.sckaSecuritySpec -
SCKAScheme.sckaSecurityImpl -
SCKAScheme.SCKAAdversary
-
-
Associated lean decls (14)
-
RKEMScheme.RatchetSimulator -
RKEMScheme.keyBaseSimDistA -
RKEMScheme.keyBaseSimExpA -
RKEMScheme.keyUpdSimDistA -
RKEMScheme.keyUpdSimExpA -
RKEMScheme.ctxtSimDistB -
RKEMScheme.ctxtSimExpA -
RKEMScheme.keyBaseSimAdvantageA -
RKEMScheme.keyBaseSimAdvantage -
RKEMScheme.keyUpdSimAdvantageA -
RKEMScheme.keyUpdSimAdvantage -
RKEMScheme.ctxtSimAdvantageA -
RKEMScheme.ctxtSimAdvantage -
RKEMScheme.RatchetSimulatable
-
-
Associated lean decls (7)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (14)
-
MLKEM.KPKE.keygenFromSeed -
MLKEM.KPKE.encrypt -
MLKEM.KPKE.decrypt -
MLKEM.NTTRingOps -
MLKEM.Primitives.gKeygen -
MLKEM.Primitives.prfEta2 -
MLKEM.Primitives.publicMatrix -
MLKEM.Primitives.sampleVecEta1 -
MLKEM.Primitives.sampleVecEta2 -
MLKEM.Concrete.samplePolyCBD -
MLKEM.Concrete.compress -
MLKEM.Concrete.decompress -
MLKEM.Concrete.byteEncode -
MLKEM.Concrete.byteDecode
-
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
Theorem / Proposition / Lemma / Corollary Index (63)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
By parent groups (26)
Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
CKA from KEM. (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Reed–Solomon erasure codes over arbitrary fields. (1)
-
Associated lean decls (1)
The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization. (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
PRF-PRNG from PRP and PRG. (1)
Sparse Post-Quantum Ratchet (SPQR) ( ). (2)
RKEM from DDH (FS). (3)
CKA from DDH. (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
FrodoKEM, a Learning-With-Errors key encapsulation mechanism ( ). (2)
Opp-UniKEM-CKA. (2)
-
Associated lean decls (1)
Triple Ratchet SM. (4)
Katana RKEM (optimised). (3)
Double Ratchet SM - Signal. (4)
Opp-RKEM-CKA. (2)
Katana RKEM (plain). (3)
Encrypt-then-MAC. (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
ML-KEM Braid ( ). (2)
-
Associated lean decls (2)
Double Ratchet SM - Abstract. (4)
Incremental KEM from ML-KEM. (1)
-
Associated lean decls (1)
Opp-BiKEM-CKA. (2)
-
Associated lean decls (1)
FS-AEAD from AEAD and PRG. (2)
RKEM from KEM. (3)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
CKA from LWE. (2)
SCKA SM. (4)
RKEM from DDH (non-FS). (2)
-
Associated lean decls (5)
GCM. (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Dependency insights
Statement-used entries96Entries reused in statement dependencies.
Tracked parent groups38Grouped health rollups for parents with more than one child entry.
Most used in statements (96)
-
Reverse dependencies recorded in statement dependencies.statement uses: 24proof uses: 0direct uses: 24downstream unlocks: 33
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 36
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 28
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 26
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 24
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 24
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 7
Associated lean decls (3)
-
Show all 86 more statement-used entries
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 6
Associated lean decls (14)
-
RKEMScheme.RatchetSimulator -
RKEMScheme.keyBaseSimDistA -
RKEMScheme.keyBaseSimExpA -
RKEMScheme.keyUpdSimDistA -
RKEMScheme.keyUpdSimExpA -
RKEMScheme.ctxtSimDistB -
RKEMScheme.ctxtSimExpA -
RKEMScheme.keyBaseSimAdvantageA -
RKEMScheme.keyBaseSimAdvantage -
RKEMScheme.keyUpdSimAdvantageA -
RKEMScheme.keyUpdSimAdvantage -
RKEMScheme.ctxtSimAdvantageA -
RKEMScheme.ctxtSimAdvantage -
RKEMScheme.RatchetSimulatable
-
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 14
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 14
Associated lean decls (17)
-
SCKAScheme.VulnerableEpochs -
SCKAScheme.GameState -
SCKAScheme.oracleSendA -
SCKAScheme.oracleSendB -
SCKAScheme.oracleSendArleak -
SCKAScheme.oracleSendBrleak -
SCKAScheme.oracleRecvA -
SCKAScheme.oracleRecvB -
SCKAScheme.oracleChall -
SCKAScheme.oracleCorruptA -
SCKAScheme.oracleCorruptB -
SCKAScheme.sckaCorrectnessSpec -
SCKAScheme.sckaCorrectnessImpl -
SCKAScheme.SCKACorrectnessAdversary -
SCKAScheme.sckaSecuritySpec -
SCKAScheme.sckaSecurityImpl -
SCKAScheme.SCKAAdversary
-
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 11
Associated lean decls (8)
-
ErasureCodePayload.Streaming.EncoderState -
ErasureCodePayload.Streaming.EncoderState.init -
ErasureCodePayload.Streaming.EncoderState.nextChunk -
ErasureCodePayload.Streaming.DecoderState -
ErasureCodePayload.Streaming.DecoderState.empty -
ErasureCodePayload.Streaming.DecoderState.addChunk -
ErasureCodePayload.Streaming.DecoderState.decodedPayload -
ErasureCodePayload.Streaming.DecoderState.hasMessage
-
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 20
Associated lean decls (14)
-
MLKEM.KPKE.keygenFromSeed -
MLKEM.KPKE.encrypt -
MLKEM.KPKE.decrypt -
MLKEM.NTTRingOps -
MLKEM.Primitives.gKeygen -
MLKEM.Primitives.prfEta2 -
MLKEM.Primitives.publicMatrix -
MLKEM.Primitives.sampleVecEta1 -
MLKEM.Primitives.sampleVecEta2 -
MLKEM.Concrete.samplePolyCBD -
MLKEM.Concrete.compress -
MLKEM.Concrete.decompress -
MLKEM.Concrete.byteEncode -
MLKEM.Concrete.byteDecode
-
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
Associated lean decls (16)
-
CKAScheme.GameState -
CKAScheme.GameParams -
CKAScheme.isChallengeEpoch -
CKAScheme.allowCorrPCS -
CKAScheme.allowCorrFS -
CKAScheme.allowCorr -
CKAScheme.oracleSendA -
CKAScheme.oracleSendB -
CKAScheme.oracleSendArleak -
CKAScheme.oracleSendBrleak -
CKAScheme.oracleRecvA -
CKAScheme.oracleRecvB -
CKAScheme.oracleChallA -
CKAScheme.oracleChallB -
CKAScheme.oracleCorruptA -
CKAScheme.oracleCorruptB
-
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (8)
-
ErasureCode.ReedSolomon.Parameters -
ErasureCode.ReedSolomon.Parameters.sourceIndex -
ErasureCode.ReedSolomon.Parameters.sourcePoint -
ErasureCode.ReedSolomon.Parameters.encodingPolynomial -
ErasureCode.ReedSolomon.Parameters.encode -
ErasureCode.ReedSolomon.Parameters.decodingPolynomial -
ErasureCode.ReedSolomon.Parameters.decode -
ErasureCode.ReedSolomon.Parameters.erasureCode
-
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (7)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (7)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Group health (38)
-
CKA from LWE.Grouped view over entries sharing the same parent.total: 3closed: 1local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 2
-
FrodoKEM, a Learning-With-Errors key encapsulation mechanism ( ).Grouped view over entries sharing the same parent.total: 3closed: 1local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 2
-
Sparse Post-Quantum Ratchet (SPQR) ( ).Grouped view over entries sharing the same parent.total: 3closed: 1local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 2
-
Pseudorandom Function-Generator (PRF-PRNG).Grouped view over entries sharing the same parent.total: 2closed: 0local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 28
-
Forward-Secure AEAD (FS-AEAD).Grouped view over entries sharing the same parent.total: 2closed: 0local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 25
-
Double Ratchet.Grouped view over entries sharing the same parent.total: 5closed: 0local-only: 0ready: 1blocked: 4incomplete Lean: 0unlock score: 17
-
Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203).Grouped view over entries sharing the same parent.total: 5closed: 4local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 13
-
SCKA SM.Grouped view over entries sharing the same parent.total: 6closed: 0local-only: 0ready: 1blocked: 5incomplete Lean: 0unlock score: 12
-
Triple Ratchet SM.Grouped view over entries sharing the same parent.total: 6closed: 0local-only: 0ready: 1blocked: 5incomplete Lean: 0unlock score: 12
-
ML-KEM Braid ( ).Grouped view over entries sharing the same parent.total: 4closed: 3local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 7
-
Show all 28 more groups
-
Opp-UniKEM-CKA.Grouped view over entries sharing the same parent.total: 4closed: 3local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 4
-
Katana RKEM (optimised).Grouped view over entries sharing the same parent.total: 4closed: 0local-only: 0ready: 1blocked: 3incomplete Lean: 0unlock score: 3
-
Katana RKEM (plain).Grouped view over entries sharing the same parent.total: 4closed: 0local-only: 0ready: 1blocked: 3incomplete Lean: 0unlock score: 3
-
RKEM from DDH (FS).Grouped view over entries sharing the same parent.total: 4closed: 0local-only: 0ready: 1blocked: 3incomplete Lean: 0unlock score: 3
-
Opp-BiKEM-CKA.Grouped view over entries sharing the same parent.total: 3closed: 2local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 2
-
Opp-RKEM-CKA.Grouped view over entries sharing the same parent.total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 2
-
Ratcheting Key Encapsulation Mechanism (RKEM).Grouped view over entries sharing the same parent.total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 71Next: no ready child currently unlocks downstream work.
-
Erasure Codes.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 68Next: no ready child currently unlocks downstream work.
-
SCKA.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 52Next: no ready child currently unlocks downstream work.
-
Online-Offline Key Encapsulation Mechanism (On-Off KEM).Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 30Next: no ready child currently unlocks downstream work.
-
Incremental Key Encapsulation Mechanism (Incremental KEM).Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 20Next: no ready child currently unlocks downstream work.
-
Double Ratchet SM - Abstract.Grouped view over entries sharing the same parent.total: 5closed: 0local-only: 0ready: 0blocked: 5incomplete Lean: 0unlock score: 18Next: no ready child currently unlocks downstream work.
-
ML-KEM Braid.Grouped view over entries sharing the same parent.total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 15Next: no ready child currently unlocks downstream work.
-
The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 11Next: no ready child currently unlocks downstream work.
-
On-Off KEM from K-PKE.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 11Next: no ready child currently unlocks downstream work.
-
Reed–Solomon erasure codes over arbitrary fields.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 10Next: no ready child currently unlocks downstream work.
-
Unchunked SPQR core.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 10Next: no ready child currently unlocks downstream work.
-
Double Ratchet SM - Signal.Grouped view over entries sharing the same parent.total: 5closed: 0local-only: 0ready: 0blocked: 5incomplete Lean: 0unlock score: 7Next: no ready child currently unlocks downstream work.
-
Chunked SPQR.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 7Next: no ready child currently unlocks downstream work.
-
Incremental KEM from ML-KEM.Grouped view over entries sharing the same parent.total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 7Next: no ready child currently unlocks downstream work.
-
CKA from DDH.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 5Next: no ready child currently unlocks downstream work.
-
RKEM from KEM.Grouped view over entries sharing the same parent.total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 3Next: no ready child currently unlocks downstream work.
-
CKA from KEM.Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2Next: no ready child currently unlocks downstream work.
-
Encrypt-then-MAC.Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2Next: no ready child currently unlocks downstream work.
-
FS-AEAD from AEAD and PRG.Grouped view over entries sharing the same parent.total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2Next: no ready child currently unlocks downstream work.
-
GCM.Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2Next: no ready child currently unlocks downstream work.
-
RKEM from DDH (non-FS).Grouped view over entries sharing the same parent.total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2Next: no ready child currently unlocks downstream work.
-
PRF-PRNG from PRP and PRG.Grouped view over entries sharing the same parent.total: 2closed: 0local-only: 0ready: 0blocked: 2incomplete Lean: 0unlock score: 1Next: no ready child currently unlocks downstream work.
-
Metadata
Tags in use119Distinct tags currently attached to blueprint entries.
Tag rollups (119)
-
entries: 2actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
Show all 109 more tags
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 1actionable: 1quick wins: 0linked PRs: 0
-
entries: 3actionable: 0quick wins: 0linked PRs: 0
-
entries: 2actionable: 0quick wins: 0linked PRs: 0
-
entries: 2actionable: 0quick wins: 0linked PRs: 0
-
entries: 2actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
entries: 1actionable: 0quick wins: 0linked PRs: 0
-
Metadata audit
Missing owner149
Missing effort149
Untagged24
Missing owner (149)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Show all 139 more entries missing owner
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (16)
-
CKAScheme.GameState -
CKAScheme.GameParams -
CKAScheme.isChallengeEpoch -
CKAScheme.allowCorrPCS -
CKAScheme.allowCorrFS -
CKAScheme.allowCorr -
CKAScheme.oracleSendA -
CKAScheme.oracleSendB -
CKAScheme.oracleSendArleak -
CKAScheme.oracleSendBrleak -
CKAScheme.oracleRecvA -
CKAScheme.oracleRecvB -
CKAScheme.oracleChallA -
CKAScheme.oracleChallB -
CKAScheme.oracleCorruptA -
CKAScheme.oracleCorruptB
-
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (8)
-
ErasureCodePayload.Streaming.EncoderState -
ErasureCodePayload.Streaming.EncoderState.init -
ErasureCodePayload.Streaming.EncoderState.nextChunk -
ErasureCodePayload.Streaming.DecoderState -
ErasureCodePayload.Streaming.DecoderState.empty -
ErasureCodePayload.Streaming.DecoderState.addChunk -
ErasureCodePayload.Streaming.DecoderState.decodedPayload -
ErasureCodePayload.Streaming.DecoderState.hasMessage
-
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (14)
-
MLKEM.KPKE.keygenFromSeed -
MLKEM.KPKE.encrypt -
MLKEM.KPKE.decrypt -
MLKEM.NTTRingOps -
MLKEM.Primitives.gKeygen -
MLKEM.Primitives.prfEta2 -
MLKEM.Primitives.publicMatrix -
MLKEM.Primitives.sampleVecEta1 -
MLKEM.Primitives.sampleVecEta2 -
MLKEM.Concrete.samplePolyCBD -
MLKEM.Concrete.compress -
MLKEM.Concrete.decompress -
MLKEM.Concrete.byteEncode -
MLKEM.Concrete.byteDecode
-
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (8)
-
ErasureCode.ReedSolomon.Parameters -
ErasureCode.ReedSolomon.Parameters.sourceIndex -
ErasureCode.ReedSolomon.Parameters.sourcePoint -
ErasureCode.ReedSolomon.Parameters.encodingPolynomial -
ErasureCode.ReedSolomon.Parameters.encode -
ErasureCode.ReedSolomon.Parameters.decodingPolynomial -
ErasureCode.ReedSolomon.Parameters.decode -
ErasureCode.ReedSolomon.Parameters.erasureCode
-
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (7)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (14)
-
RKEMScheme.RatchetSimulator -
RKEMScheme.keyBaseSimDistA -
RKEMScheme.keyBaseSimExpA -
RKEMScheme.keyUpdSimDistA -
RKEMScheme.keyUpdSimExpA -
RKEMScheme.ctxtSimDistB -
RKEMScheme.ctxtSimExpA -
RKEMScheme.keyBaseSimAdvantageA -
RKEMScheme.keyBaseSimAdvantage -
RKEMScheme.keyUpdSimAdvantageA -
RKEMScheme.keyUpdSimAdvantage -
RKEMScheme.ctxtSimAdvantageA -
RKEMScheme.ctxtSimAdvantage -
RKEMScheme.RatchetSimulatable
-
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (17)
-
SCKAScheme.VulnerableEpochs -
SCKAScheme.GameState -
SCKAScheme.oracleSendA -
SCKAScheme.oracleSendB -
SCKAScheme.oracleSendArleak -
SCKAScheme.oracleSendBrleak -
SCKAScheme.oracleRecvA -
SCKAScheme.oracleRecvB -
SCKAScheme.oracleChall -
SCKAScheme.oracleCorruptA -
SCKAScheme.oracleCorruptB -
SCKAScheme.sckaCorrectnessSpec -
SCKAScheme.sckaCorrectnessImpl -
SCKAScheme.SCKACorrectnessAdversary -
SCKAScheme.sckaSecuritySpec -
SCKAScheme.sckaSecurityImpl -
SCKAScheme.SCKAAdversary
-
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (7)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing effort (149)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Show all 139 more entries missing effort
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (16)
-
CKAScheme.GameState -
CKAScheme.GameParams -
CKAScheme.isChallengeEpoch -
CKAScheme.allowCorrPCS -
CKAScheme.allowCorrFS -
CKAScheme.allowCorr -
CKAScheme.oracleSendA -
CKAScheme.oracleSendB -
CKAScheme.oracleSendArleak -
CKAScheme.oracleSendBrleak -
CKAScheme.oracleRecvA -
CKAScheme.oracleRecvB -
CKAScheme.oracleChallA -
CKAScheme.oracleChallB -
CKAScheme.oracleCorruptA -
CKAScheme.oracleCorruptB
-
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (8)
-
ErasureCodePayload.Streaming.EncoderState -
ErasureCodePayload.Streaming.EncoderState.init -
ErasureCodePayload.Streaming.EncoderState.nextChunk -
ErasureCodePayload.Streaming.DecoderState -
ErasureCodePayload.Streaming.DecoderState.empty -
ErasureCodePayload.Streaming.DecoderState.addChunk -
ErasureCodePayload.Streaming.DecoderState.decodedPayload -
ErasureCodePayload.Streaming.DecoderState.hasMessage
-
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (14)
-
MLKEM.KPKE.keygenFromSeed -
MLKEM.KPKE.encrypt -
MLKEM.KPKE.decrypt -
MLKEM.NTTRingOps -
MLKEM.Primitives.gKeygen -
MLKEM.Primitives.prfEta2 -
MLKEM.Primitives.publicMatrix -
MLKEM.Primitives.sampleVecEta1 -
MLKEM.Primitives.sampleVecEta2 -
MLKEM.Concrete.samplePolyCBD -
MLKEM.Concrete.compress -
MLKEM.Concrete.decompress -
MLKEM.Concrete.byteEncode -
MLKEM.Concrete.byteDecode
-
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (8)
-
ErasureCode.ReedSolomon.Parameters -
ErasureCode.ReedSolomon.Parameters.sourceIndex -
ErasureCode.ReedSolomon.Parameters.sourcePoint -
ErasureCode.ReedSolomon.Parameters.encodingPolynomial -
ErasureCode.ReedSolomon.Parameters.encode -
ErasureCode.ReedSolomon.Parameters.decodingPolynomial -
ErasureCode.ReedSolomon.Parameters.decode -
ErasureCode.ReedSolomon.Parameters.erasureCode
-
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (7)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (14)
-
RKEMScheme.RatchetSimulator -
RKEMScheme.keyBaseSimDistA -
RKEMScheme.keyBaseSimExpA -
RKEMScheme.keyUpdSimDistA -
RKEMScheme.keyUpdSimExpA -
RKEMScheme.ctxtSimDistB -
RKEMScheme.ctxtSimExpA -
RKEMScheme.keyBaseSimAdvantageA -
RKEMScheme.keyBaseSimAdvantage -
RKEMScheme.keyUpdSimAdvantageA -
RKEMScheme.keyUpdSimAdvantage -
RKEMScheme.ctxtSimAdvantageA -
RKEMScheme.ctxtSimAdvantage -
RKEMScheme.RatchetSimulatable
-
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (17)
-
SCKAScheme.VulnerableEpochs -
SCKAScheme.GameState -
SCKAScheme.oracleSendA -
SCKAScheme.oracleSendB -
SCKAScheme.oracleSendArleak -
SCKAScheme.oracleSendBrleak -
SCKAScheme.oracleRecvA -
SCKAScheme.oracleRecvB -
SCKAScheme.oracleChall -
SCKAScheme.oracleCorruptA -
SCKAScheme.oracleCorruptB -
SCKAScheme.sckaCorrectnessSpec -
SCKAScheme.sckaCorrectnessImpl -
SCKAScheme.SCKACorrectnessAdversary -
SCKAScheme.sckaSecuritySpec -
SCKAScheme.sckaSecurityImpl -
SCKAScheme.SCKAAdversary
-
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (7)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Untagged (24)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (16)
-
CKAScheme.GameState -
CKAScheme.GameParams -
CKAScheme.isChallengeEpoch -
CKAScheme.allowCorrPCS -
CKAScheme.allowCorrFS -
CKAScheme.allowCorr -
CKAScheme.oracleSendA -
CKAScheme.oracleSendB -
CKAScheme.oracleSendArleak -
CKAScheme.oracleSendBrleak -
CKAScheme.oracleRecvA -
CKAScheme.oracleRecvB -
CKAScheme.oracleChallA -
CKAScheme.oracleChallB -
CKAScheme.oracleCorruptA -
CKAScheme.oracleCorruptB
-
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (14)
-
MLKEM.KPKE.keygenFromSeed -
MLKEM.KPKE.encrypt -
MLKEM.KPKE.decrypt -
MLKEM.NTTRingOps -
MLKEM.Primitives.gKeygen -
MLKEM.Primitives.prfEta2 -
MLKEM.Primitives.publicMatrix -
MLKEM.Primitives.sampleVecEta1 -
MLKEM.Primitives.sampleVecEta2 -
MLKEM.Concrete.samplePolyCBD -
MLKEM.Concrete.compress -
MLKEM.Concrete.decompress -
MLKEM.Concrete.byteEncode -
MLKEM.Concrete.byteDecode
-
-
Show all 14 more untagged entries
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (17)
-
SCKAScheme.VulnerableEpochs -
SCKAScheme.GameState -
SCKAScheme.oracleSendA -
SCKAScheme.oracleSendB -
SCKAScheme.oracleSendArleak -
SCKAScheme.oracleSendBrleak -
SCKAScheme.oracleRecvA -
SCKAScheme.oracleRecvB -
SCKAScheme.oracleChall -
SCKAScheme.oracleCorruptA -
SCKAScheme.oracleCorruptB -
SCKAScheme.sckaCorrectnessSpec -
SCKAScheme.sckaCorrectnessImpl -
SCKAScheme.SCKACorrectnessAdversary -
SCKAScheme.sckaSecuritySpec -
SCKAScheme.sckaSecurityImpl -
SCKAScheme.SCKAAdversary
-
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Structure and coverage
Informal-only61Statements with no associated Lean code yet.
Ready to formalize19Entries with an actionable next formalization step.
Fully closed88Local code and ancestor closure are both complete.
Blocked or incomplete42Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (133)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 3downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 4downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 2downstream unlocks: 4
-
Show all 123 more heaviest-prerequisite entries
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 5downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (7)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 7
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
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)
-
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)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 4
Associated lean decls (3)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 7
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 4
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 5
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (2)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
Associated lean decls (16)
-
CKAScheme.GameState -
CKAScheme.GameParams -
CKAScheme.isChallengeEpoch -
CKAScheme.allowCorrPCS -
CKAScheme.allowCorrFS -
CKAScheme.allowCorr -
CKAScheme.oracleSendA -
CKAScheme.oracleSendB -
CKAScheme.oracleSendArleak -
CKAScheme.oracleSendBrleak -
CKAScheme.oracleRecvA -
CKAScheme.oracleRecvB -
CKAScheme.oracleChallA -
CKAScheme.oracleChallB -
CKAScheme.oracleCorruptA -
CKAScheme.oracleCorruptB
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 11
Associated lean decls (8)
-
ErasureCodePayload.Streaming.EncoderState -
ErasureCodePayload.Streaming.EncoderState.init -
ErasureCodePayload.Streaming.EncoderState.nextChunk -
ErasureCodePayload.Streaming.DecoderState -
ErasureCodePayload.Streaming.DecoderState.empty -
ErasureCodePayload.Streaming.DecoderState.addChunk -
ErasureCodePayload.Streaming.DecoderState.decodedPayload -
ErasureCodePayload.Streaming.DecoderState.hasMessage
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
Associated lean decls (8)
-
ErasureCode.ReedSolomon.Parameters -
ErasureCode.ReedSolomon.Parameters.sourceIndex -
ErasureCode.ReedSolomon.Parameters.sourcePoint -
ErasureCode.ReedSolomon.Parameters.encodingPolynomial -
ErasureCode.ReedSolomon.Parameters.encode -
ErasureCode.ReedSolomon.Parameters.decodingPolynomial -
ErasureCode.ReedSolomon.Parameters.decode -
ErasureCode.ReedSolomon.Parameters.erasureCode
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 5
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
-
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 (7)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 6
Associated lean decls (14)
-
RKEMScheme.RatchetSimulator -
RKEMScheme.keyBaseSimDistA -
RKEMScheme.keyBaseSimExpA -
RKEMScheme.keyUpdSimDistA -
RKEMScheme.keyUpdSimExpA -
RKEMScheme.ctxtSimDistB -
RKEMScheme.ctxtSimExpA -
RKEMScheme.keyBaseSimAdvantageA -
RKEMScheme.keyBaseSimAdvantage -
RKEMScheme.keyUpdSimAdvantageA -
RKEMScheme.keyUpdSimAdvantage -
RKEMScheme.ctxtSimAdvantageA -
RKEMScheme.ctxtSimAdvantage -
RKEMScheme.RatchetSimulatable
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 14
Associated lean decls (17)
-
SCKAScheme.VulnerableEpochs -
SCKAScheme.GameState -
SCKAScheme.oracleSendA -
SCKAScheme.oracleSendB -
SCKAScheme.oracleSendArleak -
SCKAScheme.oracleSendBrleak -
SCKAScheme.oracleRecvA -
SCKAScheme.oracleRecvB -
SCKAScheme.oracleChall -
SCKAScheme.oracleCorruptA -
SCKAScheme.oracleCorruptB -
SCKAScheme.sckaCorrectnessSpec -
SCKAScheme.sckaCorrectnessImpl -
SCKAScheme.SCKACorrectnessAdversary -
SCKAScheme.sckaSecuritySpec -
SCKAScheme.sckaSecurityImpl -
SCKAScheme.SCKAAdversary
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
-
No prerequisites (16)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (14)
-
MLKEM.KPKE.keygenFromSeed -
MLKEM.KPKE.encrypt -
MLKEM.KPKE.decrypt -
MLKEM.NTTRingOps -
MLKEM.Primitives.gKeygen -
MLKEM.Primitives.prfEta2 -
MLKEM.Primitives.publicMatrix -
MLKEM.Primitives.sampleVecEta1 -
MLKEM.Primitives.sampleVecEta2 -
MLKEM.Concrete.samplePolyCBD -
MLKEM.Concrete.compress -
MLKEM.Concrete.decompress -
MLKEM.Concrete.byteEncode -
MLKEM.Concrete.byteDecode
-
-
Associated lean decls (1)
-
Show all 6 more entries without prerequisites
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
No dependents (53)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Show all 43 more entries without dependents
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)