structure
definition
PublicInvariant
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cryptography.ECDLPWatch on GitHub at line 129.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
126 family := inst.family
127
128/-- A watch invariant is admissible only if it is computed from public data. -/
129structure PublicInvariant where
130 score : ∀ {p : ℕ}, PublicECDLPData p → ℝ
131
132/-- Known weak-curve classes must be separated from any standard-curve claim. -/
133def isKnownWeakFamily : CurveFamily → Prop
134 | CurveFamily.anomalous => True
135 | CurveFamily.supersingular => True
136 | CurveFamily.smallEmbeddingDegree => True
137 | _ => False
138
139/-- Watch predicate: a candidate invariant is being tested only on public data
140and against an explicitly tagged curve family. This carries no security claim. -/
141structure InvariantWatchRecord (I : PublicInvariant) where
142 family : CurveFamily
143 weak_family_tagged : isKnownWeakFamily family ∨ ¬ isKnownWeakFamily family
144
145end ECDLPWatch
146end Cryptography
147end IndisputableMonolith