mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-03 20:13:48 +00:00
mrwulf
0566733ca4
(sqrt_ratio_i_sq_spec, kernel-audited) The largest single proof of the decompress chain: for square u/v (witness x, v nonzero), the extracted sqrt_ratio_i returns choice 1 and the even-parity root - Bnd r (2^52), r^2 * v = u, r's canonical residue even. The walk composes every previously certified piece: the square/mul/pow_p58 candidate chain, sqrt_m1_spec, fe_ct_eq_spec x3 (the three constant-time residue checks), neg_spec, the Choice bitor, and fe_cond_assign_spec twice (root flip by sqrt(-1), then sign normalization via is_negative). Case analysis: sqrt_core's disjunction (v*r^2 = +/-u) against the check flags - u = 0 collapses everything to the zero root; u != 0 with v*r^2 = u kills both flip flags (u = -u forces u = 0 in odd characteristic; u = -u*i forces u*(1+i) = 0 with 1+i nonzero); with v*r^2 = -u the flip fires and (i*r)^2 * v = -(-u) = u. Parity: the odd- prime negation flip (ZMod.neg_val), zero-root edge included. New helpers: eq_neg_self_iff_zero, one_add_i_ne_zero. Certificate exact standard three; full button green fresh. Remaining: from_bytes walk, decompress_of_canonical, replication, pass 4. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveSig.llbc | ||
| extract.sh | ||
| lean-guard | ||