From 133eab8467303a58ba53979a051073cfffb91f09 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 4 Jul 2026 16:52:06 +0200 Subject: [PATCH] NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The complete non_adjacent_form(5) verification (four stages): - `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load. - `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul telescope), the carry-kill argument from V < 2^253, and the exit theorem. - `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the remaining-bits measure: per-step 64-bit window read (4-way word split), digit write via hcast/wrapping_sub (exact value window - 32*carry', oddness, |d| < 16), invariant carried through even/odd steps. - `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts DISCHARGED; the digits satisfy the NAF conditions and sum naf[k]*2^k = V EXACTLY (integers, no modular slack) for any scalar whose LE byte value V is below 2^253. And the campaign's brick 4, `Proofs/DsmMulSpec.lean`: - `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard base point: valid extended coordinates (X*Y = Z*T) and the curve equation, kernel-checked via denominator-free 121666-scaled witnesses. Includes the generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness. - `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of vartime_double_base::mul: for canonical scalars and a valid on-curve A, the result is valid, on-curve, and denotes dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256 with both digit arrays proven exact NAF encodings. Phase 2 (group semantics [a]A + [b]B) requires Edwards associativity — deferred and documented; nothing assumes it. Also: removed a vestigial pre-re-extraction axiom stub (backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal — a root-level leftover that shadowed the real namespaced definition during name resolution in proof files. Never referenced by any certificate (the #print-axioms audit guards against that); deleted for hygiene. CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec, non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec — each audited to exactly [propext, Classical.choice, Quot.sound]. Full check.sh green. Co-Authored-By: Claude Fable 5 --- verification/Proofs/DsmMulSpec.lean | 200 +++++++++ verification/Proofs/DsmNafLoopSpec.lean | 418 ++++++++++++++++++ verification/Proofs/DsmNafSpec.lean | 84 ++++ verification/check.sh | 9 + verification/gen/CurveField/FunsExternal.lean | 8 - 5 files changed, 711 insertions(+), 8 deletions(-) create mode 100644 verification/Proofs/DsmMulSpec.lean create mode 100644 verification/Proofs/DsmNafLoopSpec.lean create mode 100644 verification/Proofs/DsmNafSpec.lean diff --git a/verification/Proofs/DsmMulSpec.lean b/verification/Proofs/DsmMulSpec.lean new file mode 100644 index 0000000..7a47812 --- /dev/null +++ b/verification/Proofs/DsmMulSpec.lean @@ -0,0 +1,200 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/DsmMulSpec.lean — double-scalar-mul campaign, brick 4: + the basepoint constant and the public `vartime_double_base::mul` spec. + + · `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is a VALID + extended point ON THE CURVE denoting the standard base point + B = (x_B, y_B), x_B = 15112…202, y_B = 46316…960 + — kernel-checked literal arithmetic: the extended coherence X·Y = Z·T + and the (121666-scaled, denominator-free) curve equation + 121666·y² + 121665·x²y² ≡ 121666 + 121666·x² (mod p). + A corrupted basepoint constant would be caught here. + + · `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC: + for canonical scalars (byte values < 2^253) and a valid on-curve A, + `mul a A b` returns a valid on-curve R with + edPt R = dsmFold (digits of a) (digits of b) (edPt A) edBasePt edId 256 + where both digit arrays are proven NAF encodings of the scalars' exact + byte values (existentially exposed with their NafDigits + nafSum facts). + Composes non_adjacent_form_spec ×2, dsm_top_index_spec, naf_table_spec + ×2 (A and the basepoint), dsm_loop_spec, proj_as_extended_spec. + Phase 2 (reading dsmFold as [a]A + [b]B in the group) requires Edwards + associativity — deliberately deferred and documented; nothing here + assumes it. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.DsmNafSpec +open Aeneas Aeneas.Std Result ControlFlow +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false +set_option maxRecDepth 8000 +set_option exponentiation.threshold 600 + +namespace CurveFieldProofs + +open Aeneas.Std.WP + +/-- Generic mod-p witness → Fp product identity (abstract, no literal + crunching during cast distribution). -/ +theorem fp_mul_eq_of_witness (a b c : ℕ) (hmod : (a * b) % P = c % P) : + (a : Fp) * (b : Fp) = (c : Fp) := by + have h1 : ((a * b : ℕ) : Fp) = ((c : ℕ) : Fp) := by + rw [← ZMod.natCast_mod, hmod, ZMod.natCast_mod] + push_cast at h1 + exact h1 + +/-- Generic 121666-scaled curve-equation witness → OnCurve (abstract x, y). -/ +theorem onCurve_of_witness (x y : ℕ) + (hmod : (121666 * (y * y) + 121665 * (x * x) * (y * y)) % P + = (121666 + 121666 * (x * x)) % P) : + OnCurve (x : Fp) (y : Fp) := by + have h1 : ((121666 * (y * y) + 121665 * (x * x) * (y * y) : ℕ) : Fp) + = ((121666 + 121666 * (x * x) : ℕ) : Fp) := by + rw [← ZMod.natCast_mod, hmod, ZMod.natCast_mod] + push_cast at h1 + have h6 : (121666 : Fp) ≠ 0 := by + have h : ((121666 : ℕ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide) + simpa using h + have hd := edD_char + unfold OnCurve + apply mul_left_cancel₀ h6 + linear_combination h1 - (x : Fp)^2 * (y : Fp)^2 * hd + +/-- The standard Ed25519 base point, as ZMod literals. -/ +noncomputable def edBasePt : Fp × Fp := + ((15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp), + (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp)) + +/-- **The transpiled basepoint constant is the standard base point** — + valid, on-curve, kernel-audited literal arithmetic. -/ +theorem run_basepoint : + ∃ B : EdPoint, + backend.serial.u64.constants.ED25519_BASEPOINT_POINT = ok B ∧ + ExtValid B ∧ OnCurveExt B ∧ edPt B = edBasePt := by + -- the four coordinate denotations + have hXv : ⟪(Array.make 5#usize [1738742601995546#u64, 1146398526822698#u64, + 2070867633025821#u64, 562264141797630#u64, 587772402128613#u64] : + backend.serial.u64.field.FieldElement51)⟫ = + (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) := by + simp [denote, feVal, limbsVal, Array.make] + have hYv : ⟪(Array.make 5#usize [1801439850948184#u64, 1351079888211148#u64, + 450359962737049#u64, 900719925474099#u64, 1801439850948198#u64] : + backend.serial.u64.field.FieldElement51)⟫ = + (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) := by + simp [denote, feVal, limbsVal, Array.make] + have hZv : ⟪(Array.make 5#usize [1#u64, 0#u64, 0#u64, 0#u64, 0#u64] : + backend.serial.u64.field.FieldElement51)⟫ = (1 : Fp) := by + simp [denote, feVal, limbsVal, Array.make] + have hTv : ⟪(Array.make 5#usize [1841354044333475#u64, 16398895984059#u64, + 755974180946558#u64, 900171276175154#u64, 1821297809914039#u64] : + backend.serial.u64.field.FieldElement51)⟫ = + (46827403850823179245072216630277197565144205554125654976674165829533817101731 : Fp) := by + simp [denote, feVal, limbsVal, Array.make] + -- coherence of the affine literals: x·y = t (z = 1) + have hco : (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) * + (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) = + (46827403850823179245072216630277197565144205554125654976674165829533817101731 : Fp) := by + apply fp_mul_eq_of_witness + norm_num [P] + -- the curve equation for the affine literals (121666-scaled witness) + have hcv : OnCurve + (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) + (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) := by + have h := onCurve_of_witness + 15112221349535400772501151409588531511454012693041857206046113283949847762202 + 46316835694926478169428394003475163141307993866256225615783033603165251855960 + (by norm_num [P]) + push_cast at h + exact h + refine ⟨⟨Array.make 5#usize [1738742601995546#u64, 1146398526822698#u64, + 2070867633025821#u64, 562264141797630#u64, 587772402128613#u64], + Array.make 5#usize [1801439850948184#u64, 1351079888211148#u64, + 450359962737049#u64, 900719925474099#u64, 1801439850948198#u64], + Array.make 5#usize [1#u64, 0#u64, 0#u64, 0#u64, 0#u64], + Array.make 5#usize [1841354044333475#u64, 16398895984059#u64, + 755974180946558#u64, 900171276175154#u64, 1821297809914039#u64]⟩, + ?_, ⟨?_, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩ + · unfold backend.serial.u64.constants.ED25519_BASEPOINT_POINT + backend.serial.u64.field.FieldElement51.from_limbs + rfl + · simp [Bnd, Array.make] + · simp [Bnd, Array.make] + · simp [Bnd, Array.make] + · simp [Bnd, Array.make] + · show ⟪_⟫ ≠ 0 + rw [hZv]; exact one_ne_zero + · show ⟪_⟫ * ⟪_⟫ = ⟪_⟫ * ⟪_⟫ + rw [hXv, hYv, hZv, hTv, one_mul] + exact hco + · show OnCurve (edX _) (edY _) + unfold edX edY + simp only + rw [hXv, hYv, hZv, div_one, div_one] + exact hcv + · show (edX _, edY _) = edBasePt + unfold edX edY edBasePt + simp only + rw [hXv, hYv, hZv, div_one, div_one] + +/-- **vartime_double_base::mul — the phase-1 computational specification.** + For canonical scalars a, b (LE byte values Va, Vb < 2^253) and a valid + on-curve A: the result is a valid on-curve point denoting the abstract + double-and-add fold of the two proven NAF encodings over A and the + standard base point. -/ +theorem vartime_double_base_mul_spec + (a b : scalar.Scalar) (A : EdPoint) + (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 : Std.U8) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hab : (↑a.bytes : List Std.U8) = [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31]) + (hbb : (↑b.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) + (Va Vb : ℕ) + (hVa : Va = a0.val + a1.val * 2^8 + a2.val * 2^16 + a3.val * 2^24 + a4.val * 2^32 + a5.val * 2^40 + a6.val * 2^48 + a7.val * 2^56 + a8.val * 2^64 + a9.val * 2^72 + a10.val * 2^80 + a11.val * 2^88 + a12.val * 2^96 + a13.val * 2^104 + a14.val * 2^112 + a15.val * 2^120 + a16.val * 2^128 + a17.val * 2^136 + a18.val * 2^144 + a19.val * 2^152 + a20.val * 2^160 + a21.val * 2^168 + a22.val * 2^176 + a23.val * 2^184 + a24.val * 2^192 + a25.val * 2^200 + a26.val * 2^208 + a27.val * 2^216 + a28.val * 2^224 + a29.val * 2^232 + a30.val * 2^240 + a31.val * 2^248) + (hVb : Vb = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248) + (hValt : Va < 2^253) (hVblt : Vb < 2^253) + (hAv : ExtValid A) (hAc : OnCurveExt A) : + backend.serial.scalar_mul.vartime_double_base.mul a A b ⦃ R => + ExtValid R ∧ OnCurveExt R ∧ + ∃ (na nb : Std.Array Std.I8 256#usize), + NafDigits na ∧ NafDigits nb ∧ + nafSum na 256 = (Va : ℤ) ∧ nafSum nb 256 = (Vb : ℤ) ∧ + edPt R = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 ⦄ := by + obtain ⟨B, hBok, hBv, hBc, hBpt⟩ := run_basepoint + unfold backend.serial.scalar_mul.vartime_double_base.mul + -- the two NAF encodings + step with (non_adjacent_form_spec a + a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 + hab Va hVa hValt) as ⟨na, hnaD, hnaS⟩ + step with (non_adjacent_form_spec b + b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 + hbb Vb hVb hVblt) as ⟨nb, hnbD, hnbS⟩ + -- the top index (constant 255) + step with (dsm_top_index_spec na nb) as ⟨i, hi⟩ + -- table over A + step with (naf_table_spec A hAv hAc) as + ⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, ta, hlA, hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩ + -- the basepoint constant + rw [hBok] + simp only [bind_tc_ok] + -- table over B + step with (naf_table_spec B hBv hBc) as + ⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, tb, hlB, hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩ + -- the 256-step Straus loop + step with (dsm_loop_spec i (by rw [hi]; scalar_tac : i.val = 255) na nb ta tb A B + ⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, hlA, hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩ + ⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, hlB, hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩ + hnaD hnbD) as ⟨r, hrv, hrc, hrfold⟩ + -- the final projective → extended conversion + apply spec_mono (proj_as_extended_spec r hrv) + rintro R ⟨hRv, -, -, -, -, hRx, hRy⟩ + refine ⟨hRv, ?_, na, nb, hnaD, hnbD, hnaS, hnbS, ?_⟩ + · show OnCurve (edX R) (edY R) + rw [hRx, hRy] + exact hrc + · calc edPt R = (edX R, edY R) := rfl + _ = (projX r, projY r) := by rw [hRx, hRy] + _ = dsmFold (nafDigit na) (nafDigit nb) (edPt A) (edPt B) edId 256 := hrfold + _ = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 := by + rw [hBpt] + +end CurveFieldProofs diff --git a/verification/Proofs/DsmNafLoopSpec.lean b/verification/Proofs/DsmNafLoopSpec.lean new file mode 100644 index 0000000..9037d28 --- /dev/null +++ b/verification/Proofs/DsmNafLoopSpec.lean @@ -0,0 +1,418 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/DsmNafLoopSpec.lean — NAF campaign, stage 3: the w=5 digit loop, + by induction on the remaining-bits measure (no unrolling). + + State (naf, pos, carry); exact ℤ invariant (DsmNafMath): + carry ≤ 1 ∧ (carry = 1 → pos ≤ 254) ∧ digits ≥ pos all zero ∧ + digit conditions ∧ nafSum naf 256 + carry·2^pos = V mod 2^pos. + One symbolic body-walk per induction step: + · `naf_bitbuf_spec` — the (single|cross)-word 64-bit read at bit pos, + 4-way split on the word index, closed by naf_window_single/cross. + · `naf_update_spec` — the odd-digit write: hcast / wrapping_sub digit, + new carry ∈ {0,1}, exact digit value window − 32·carry′, oddness and + |d| < 16 (the strict lower bound needs the window's oddness). + · even step: pos+1 via naf_even_step / naf_carry_even; + odd step: pos+5 via nafSum_set / naf_odd_step / naf_carry_odd. + Exit (pos ≥ 256): naf_exit — the carry is provably dead and + nafSum naf 256 = V exactly (V < 2^253: canonical scalars, which is + what the mul call sites provide). + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.DsmNafMath +open Aeneas Aeneas.Std Result ControlFlow +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false +set_option maxRecDepth 8000 + +namespace CurveFieldProofs + +open Aeneas.Std.WP + +/-! ### Digit-array set plumbing -/ + +/-- Entries away from the written index are unchanged. -/ +theorem nafDigit_set_ne (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ) + (d : Std.I8) (hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d) + (k : ℕ) (hk : k < 256) (hne : k ≠ pos) : + nafDigit naf' k = nafDigit naf k := by + have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac + unfold nafDigit + rw [hset, getElem!_pos ((↑naf : List Std.I8).set pos d) k + (by rw [List.length_set]; omega), + List.getElem_set_ne (by omega), + ← getElem!_pos (↑naf : List Std.I8) k (by omega)] + +/-- The written entry holds the new digit. -/ +theorem nafDigit_set_eq (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ) + (d : Std.I8) (hpos : pos < 256) + (hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d) : + nafDigit naf' pos = d.val := by + have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac + unfold nafDigit + rw [hset, getElem!_pos ((↑naf : List Std.I8).set pos d) pos + (by rw [List.length_set]; omega), + List.getElem_set_self] + +/-! ### The 64-bit window read and the digit write -/ + +/-- The 64-bit buffer read of the digit loop at bit position pos: its masked + value is the 5-bit window of V at pos. Four word cases (the fifth word is + the zero pad), each closed by naf_window_single (bit_idx < 59) or + naf_window_cross. -/ +theorem naf_bitbuf_spec + (x_u64 : Std.Array Std.U64 5#usize) (v0 v1 v2 v3 : Std.U64) (V : ℕ) + (hx : (↑x_u64 : List Std.U64) = [v0, v1, v2, v3, 0#u64]) + (hVdef : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) + (u bidx : Usize) (pos : ℕ) (hposv : pos < 256) + (hu : u.val = pos / 64) (hbidx : bidx.val = pos % 64) : + (if bidx < 59#usize + then do + let i1 ← Array.index_usize x_u64 u + i1 >>> bidx + else + do + let i1 ← Array.index_usize x_u64 u + let i2 ← i1 >>> bidx + let i3 ← 1#usize + u + let i4 ← Array.index_usize x_u64 i3 + let i5 ← 64#usize - bidx + let i6 ← i4 <<< i5 + ok (i2 ||| i6)) + ⦃ buf => buf.val % 32 = (V / 2^pos) % 32 ⦄ := by + have hb0 : v0.val < 2^64 := by scalar_tac + have hb1 : v1.val < 2^64 := by scalar_tac + have hb2 : v2.val < 2^64 := by scalar_tac + have hb3 : v3.val < 2^64 := by scalar_tac + have hulen : u.val < 4 := by clear * - hu hposv; omega + have hsz : (U64.size : ℕ) = 2^64 := by scalar_tac + split + · -- single-word read + rename_i hblt + have hbv : pos % 64 < 59 := by + have h := hbidx ▸ (show bidx.val < 59 by clear * - hblt; scalar_tac) + omega + step as ⟨w, hw⟩ + step as ⟨buf, hbuf⟩ + rcases (show pos / 64 = 0 ∨ pos / 64 = 1 ∨ pos / 64 = 2 ∨ pos / 64 = 3 by omega) + with hc | hc | hc | hc + · have huv : u.val = 0 := by omega + simp only [hx, huv] at hw + simp at hw + rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow] + have hd : V = 0 + 2^0 * (v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) := by + rw [hVdef]; try ring + have h := naf_window_single V (0) v0.val (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) 0 (pos % 64) + hd (by norm_num) (by omega) + rw [show (0 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · have huv : u.val = 1 := by omega + simp only [hx, huv] at hw + simp at hw + rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow] + have hd : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by + rw [hVdef]; try ring + have h := naf_window_single V (v0.val) v1.val (v2.val + 2^64 * (v3.val + 2^64 * 0)) 64 (pos % 64) + hd (by omega) (by omega) + rw [show (64 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · have huv : u.val = 2 := by omega + simp only [hx, huv] at hw + simp at hw + rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow] + have hd : V = v0.val + 2^64 * v1.val + 2^128 * (v2.val + 2^64 * (v3.val + 2^64 * 0)) := by + rw [hVdef]; try ring + have h := naf_window_single V (v0.val + 2^64 * v1.val) v2.val (v3.val + 2^64 * 0) 128 (pos % 64) + hd (by omega) (by omega) + rw [show (128 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · have huv : u.val = 3 := by omega + simp only [hx, huv] at hw + simp at hw + rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow] + have hd : V = v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * (v3.val + 2^64 * (0)) := by + rw [hVdef]; try ring + have h := naf_window_single V (v0.val + 2^64 * v1.val + 2^128 * v2.val) v3.val (0) 192 (pos % 64) + hd (by omega) (by omega) + rw [show (192 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · -- cross-word read + rename_i hbge + have hbv : 59 ≤ pos % 64 := by + have h : ¬ (bidx.val < 59) := by clear * - hbge; scalar_tac + omega + step as ⟨w, hw⟩ + step as ⟨i2, hi2⟩ + step as ⟨i3, hi3⟩ + step as ⟨w', hw'⟩ + step as ⟨i5, hi5⟩ + step as ⟨i6, hi6⟩ + try simp only [spec_ok] + rcases (show pos / 64 = 0 ∨ pos / 64 = 1 ∨ pos / 64 = 2 ∨ pos / 64 = 3 by omega) + with hc | hc | hc | hc + · have huv : u.val = 0 := by omega + have hi3v : i3.val = 1 := by clear * - hi3 huv; omega + simp only [hx, huv] at hw + simp at hw + simp only [hx, hi3v] at hw' + simp at hw' + rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz, + Nat.shiftRight_eq_div_pow] + have hd : V = 0 + 2^0 * (v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) := by + rw [hVdef]; try simp; try ring + have h := naf_window_cross V (0) v0.val (v1.val) (v2.val + 2^64 * (v3.val + 2^64 * 0)) 0 (pos % 64) + hd (by norm_num) (by omega) (by omega) + rw [show (0 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · have huv : u.val = 1 := by omega + have hi3v : i3.val = 2 := by clear * - hi3 huv; omega + simp only [hx, huv] at hw + simp at hw + simp only [hx, hi3v] at hw' + simp at hw' + rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz, + Nat.shiftRight_eq_div_pow] + have hd : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by + rw [hVdef]; try simp; try ring + have h := naf_window_cross V (v0.val) v1.val (v2.val) (v3.val + 2^64 * 0) 64 (pos % 64) + hd (by omega) (by omega) (by omega) + rw [show (64 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · have huv : u.val = 2 := by omega + have hi3v : i3.val = 3 := by clear * - hi3 huv; omega + simp only [hx, huv] at hw + simp at hw + simp only [hx, hi3v] at hw' + simp at hw' + rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz, + Nat.shiftRight_eq_div_pow] + have hd : V = v0.val + 2^64 * v1.val + 2^128 * (v2.val + 2^64 * (v3.val + 2^64 * (0))) := by + rw [hVdef]; try simp; try ring + have h := naf_window_cross V (v0.val + 2^64 * v1.val) v2.val (v3.val) (0) 128 (pos % 64) + hd (by omega) (by omega) (by omega) + rw [show (128 : ℕ) + pos % 64 = pos from by omega] at h + exact h + · have huv : u.val = 3 := by omega + have hi3v : i3.val = 4 := by clear * - hi3 huv; omega + simp only [hx, huv] at hw + simp at hw + simp only [hx, hi3v] at hw' + simp at hw' + rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz, + Nat.shiftRight_eq_div_pow] + have hd : V = v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * (v3.val + 2^64 * ((0#u64).val + 2^64 * (0))) := by + rw [hVdef]; try simp; try ring + have h := naf_window_cross V (v0.val + 2^64 * v1.val + 2^128 * v2.val) v3.val ((0#u64).val) (0) 192 (pos % 64) + hd (by omega) (by omega) (by omega) + rw [show (192 : ℕ) + pos % 64 = pos from by omega] at h + exact h + +/-- The odd-digit write: hcast (or hcast + wrapping_sub) produces the digit + window − 32·carry′ with carry′ the ≥16 indicator; the digit is odd with + |d| < 16, and the entry is written at pos. -/ +theorem naf_update_spec (naf : Std.Array Std.I8 256#usize) (pos : Usize) (window : Std.U64) + (hpos : pos.val < 256) (hwle : window.val ≤ 32) (hwodd : window.val % 2 = 1) : + (if window < 16#u64 + then do + let i4 ← lift (UScalar.hcast .I8 window) + let a ← Array.update naf pos i4 + ok (a, 0#u64) + else + do + let i4 ← lift (UScalar.hcast .I8 window) + let i5 ← lift (UScalar.hcast .I8 32#u64) + let i6 ← lift (core.num.I8.wrapping_sub i4 i5) + let a ← Array.update naf pos i6 + ok (a, 1#u64)) + ⦃ p => ∃ d : Std.I8, (↑p.1 : List Std.I8) = (↑naf : List Std.I8).set pos.val d ∧ + p.2.val ≤ 1 ∧ + (d.val : ℤ) = (window.val : ℤ) - 32 * (p.2.val : ℤ) ∧ + d.val % 2 = 1 ∧ -16 < d.val ∧ d.val < 16 ∧ + ((window.val < 16 ∧ p.2.val = 0) ∨ (16 ≤ window.val ∧ p.2.val = 1)) ⦄ := by + split + · rename_i hlt + have hltv : window.val < 16 := by clear * - hlt; scalar_tac + step with (UScalar.hcast_inBounds_spec .I8 window + (by clear * - hltv; scalar_tac)) as ⟨d, hd⟩ + step as ⟨a, ha⟩ + try simp only [spec_ok] + refine ⟨d, by rw [ha, Array.set_val_eq], by simp, by simp [hd], ?_, ?_, ?_, + Or.inl ⟨hltv, by simp⟩⟩ + · rw [hd]; clear * - hwodd; omega + · rw [hd]; push_cast; omega + · rw [hd]; clear * - hltv; omega + · rename_i hge + have hgev : 16 ≤ window.val := by clear * - hge; scalar_tac + step with (UScalar.hcast_inBounds_spec .I8 window + (by clear * - hwle; scalar_tac)) as ⟨d0, hd0⟩ + step with (UScalar.hcast_inBounds_spec .I8 32#u64 + (by scalar_tac)) as ⟨t32, ht32⟩ + step as ⟨d, hd⟩ + step as ⟨a, ha⟩ + try simp only [spec_ok] + have hdv : (d.val : ℤ) = (window.val : ℤ) - 32 := by + rw [hd] + simp only [core.num.I8.wrapping_sub_val_eq, hd0, ht32] + have hb := Aeneas.Arith.Int.bmod_pow2_eq_of_inBounds' 8 ((window.val : ℤ) - 32) + (by norm_num) (by clear * - ; push_cast; omega) + (by clear * - hwle; push_cast; omega) + push_cast at hb ⊢ + convert hb using 2 <;> norm_num + refine ⟨d, by rw [ha, Array.set_val_eq], by simp, by simp [hdv], ?_, ?_, ?_, + Or.inr ⟨hgev, by simp⟩⟩ + · rw [hdv]; clear * - hwodd hgev; omega + · rw [hdv]; clear * - hgev hwodd; push_cast; omega + · rw [hdv]; clear * - hwle; omega + + +/-! ### The digit loop -/ + +/-- **The w=5 NAF digit loop**, by induction on the remaining-bits measure. + From any state satisfying the invariant, the loop returns a digit array + with the NAF digit conditions and exact value V. -/ +theorem naf_digit_loop_spec + (x_u64 : Std.Array Std.U64 5#usize) (v0 v1 v2 v3 : Std.U64) (V : ℕ) + (hx : (↑x_u64 : List Std.U64) = [v0, v1, v2, v3, 0#u64]) + (hVdef : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) + (hV : V < 2^253) (m : ℕ) : + ∀ (naf : Std.Array Std.I8 256#usize) (pos : Usize) (carry : Std.U64), + 256 - pos.val ≤ m → + carry.val ≤ 1 → + (carry.val = 1 → pos.val ≤ 254) → + (∀ k, pos.val ≤ k → k < 256 → nafDigit naf k = 0) → + (∀ k, k < 256 → (nafDigit naf k = 0 ∨ nafDigit naf k % 2 = 1) ∧ + -16 < nafDigit naf k ∧ nafDigit naf k < 16) → + nafSum naf 256 + carry.val * 2^pos.val = ((V % 2^pos.val : ℕ) : ℤ) → + scalar.Scalar.non_adjacent_form_loop1 5#usize naf x_u64 32#u64 31#u64 pos carry + ⦃ res => NafDigits res ∧ nafSum res 256 = (V : ℤ) ⦄ := by + induction m with + | zero => + intro naf pos carry hm hc hcp hzero hdig hinv + unfold scalar.Scalar.non_adjacent_form_loop1 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop1.body] + have hguard : ¬ (pos < 256#usize) := by clear * - hm; scalar_tac + rw [if_neg hguard] + try simp only [spec_ok] + exact ⟨hdig, naf_exit V pos.val carry.val _ hV (by clear * - hm; omega) hc hcp hinv⟩ + | succ m ih => + intro naf pos carry hm hc hcp hzero hdig hinv + unfold scalar.Scalar.non_adjacent_form_loop1 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop1.body] + by_cases hguard : pos < 256#usize + swap + · -- exit branch (measure slack) + rw [if_neg hguard] + try simp only [spec_ok] + have hge : 256 ≤ pos.val := by clear * - hguard; scalar_tac + exact ⟨hdig, naf_exit V pos.val carry.val _ hV hge hc hcp hinv⟩ + · rw [if_pos hguard] + have hposv : pos.val < 256 := by clear * - hguard; scalar_tac + -- u64_idx ← pos / 64 ; bit_idx ← pos % 64 ; i ← 64 − 5 + step as ⟨u, hu⟩ + step as ⟨bidx, hbidx⟩ + step as ⟨i59, hi59⟩ + have hi59v : i59 = 59#usize := by clear * - hi59; scalar_tac + rw [hi59v] + -- bit_buf: the 5-bit window of V at pos + step with (naf_bitbuf_spec x_u64 v0 v1 v2 v3 V hx hVdef u bidx pos.val + hposv hu hbidx) as ⟨buf, hbuf⟩ + -- i1 ← buf &&& 31 : the masked window + step as ⟨msk, hmsk⟩ + have hmskv : msk.val = (V / 2^pos.val) % 32 := by + rw [hmsk, UScalar.val_and] + rw [show (31#u64).val = 2^5 - 1 by scalar_tac, + Nat.and_two_pow_sub_one_eq_mod] + rw [show (2:ℕ)^5 = 32 from by norm_num] + exact hbuf + -- window ← carry + msk + step as ⟨win, hwin⟩ + have hwinv : win.val = carry.val + (V / 2^pos.val) % 32 := by + rw [hwin, hmskv] + have hwle : win.val ≤ 32 := by clear * - hwinv hc; omega + -- i2 ← win &&& 1 : the parity bit + step as ⟨par, hpar⟩ + have hparv : par.val = win.val % 2 := by + rw [hpar, UScalar.val_and] + rw [show (1#u64).val = 2^1 - 1 by scalar_tac, + Nat.and_two_pow_sub_one_eq_mod] + try norm_num + split + · -- EVEN window: digit 0, pos+1, carry unchanged + rename_i hz + have heven : (carry.val + (V / 2^pos.val) % 32) % 2 = 0 := by + have h : par.val = 0 := by rw [hz]; simp + rw [← hwinv, ← hparv] + exact h + step as ⟨pos1, hpos1⟩ + have hpos1v : pos1.val = pos.val + 1 := by clear * - hpos1; omega + try simp only [spec_ok] + apply ih naf pos1 carry (by clear * - hm hpos1v; omega) hc + (fun h1 => by have := naf_carry_even V pos.val carry.val hV hc heven h1 + clear * - this hpos1v; omega) + (fun k hk1 hk2 => hzero k (by clear * - hk1 hpos1v; omega) hk2) + hdig + (by rw [hpos1v] + exact naf_even_step V pos.val carry.val _ hc hinv heven) + · -- ODD window: write digit, pos+5, carry from the ≥16 test + rename_i hnz + have hwodd : win.val % 2 = 1 := by + have h : par.val ≠ 0 := by + clear * - hnz + intro h + exact hnz (by scalar_tac) + clear * - h hparv + omega + -- i3 ← 32 / 2 (= 16) + step as ⟨h16, hh16⟩ + have hh16v : h16 = 16#u64 := by clear * - hh16; scalar_tac + rw [hh16v] + -- the digit write (both branches of the < 16 test) + step with (naf_update_spec naf pos win hposv hwle hwodd) as + ⟨d, naf1, carry1, hset, hc1, hdval, hdodd, hdlo, hdhi, hcase⟩ + -- pos1 ← pos + 5 + step as ⟨pos1, hpos1⟩ + have hpos1v : pos1.val = pos.val + 5 := by clear * - hpos1; scalar_tac + try simp only [spec_ok] + -- the digit facts at the written index and away from it + have holdz : nafDigit naf pos.val = 0 := + hzero pos.val (le_refl _) hposv + have hsum1 : nafSum naf1 256 = nafSum naf 256 + d.val * 2^pos.val := + nafSum_set naf naf1 pos.val d hposv holdz hset + have hdig1 : ∀ k, k < 256 → nafDigit naf1 k = + if k = pos.val then d.val else nafDigit naf k := by + intro k hk + by_cases h : k = pos.val + · subst h + rw [nafDigit_set_eq naf naf1 pos.val d hk hset, if_pos rfl] + · rw [nafDigit_set_ne naf naf1 pos.val d hset k hk h, if_neg h] + -- the window as a ℕ fact for the step lemmas + have hwcase : (carry.val + (V / 2^pos.val) % 32 < 16 ∧ carry1.val = 0) ∨ + (16 ≤ carry.val + (V / 2^pos.val) % 32 ∧ carry1.val = 1) := by + rw [← hwinv] + exact hcase + apply ih naf1 pos1 carry1 (by clear * - hm hpos1v; omega) hc1 + (fun h1 => by + have := naf_carry_odd V pos.val carry.val carry1.val hV hc hwcase h1 + clear * - this hpos1v; omega) + (fun k hk1 hk2 => by + rw [hdig1 k hk2, if_neg (by clear * - hk1 hpos1v hposv; omega)] + exact hzero k (by clear * - hk1 hpos1v; omega) hk2) + (fun k hk => by + rw [hdig1 k hk] + by_cases h : k = pos.val + · rw [if_pos h] + exact ⟨Or.inr hdodd, hdlo, hdhi⟩ + · rw [if_neg h] + exact hdig k hk) + (by rw [hpos1v, hsum1] + have hd' : (d.val : ℤ) = (carry.val : ℤ) + + ((V / 2^pos.val) % 32 : ℕ) - 32 * carry1.val := by + rw [hdval, hwinv] + push_cast + ring + exact naf_odd_step V pos.val carry.val carry1.val _ d.val hinv hd') + + +end CurveFieldProofs diff --git a/verification/Proofs/DsmNafSpec.lean b/verification/Proofs/DsmNafSpec.lean new file mode 100644 index 0000000..01b8c32 --- /dev/null +++ b/verification/Proofs/DsmNafSpec.lean @@ -0,0 +1,84 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/DsmNafSpec.lean — NAF campaign, stage 4: the public spec of + `Scalar::non_adjacent_form(5)`. + + Composes the proven stages: both entry masserts DISCHARGED (w = 5 is in + [2,8]), the LE byte→word load (DsmNafLoadSpec), width = 1<<<5 = 32 and + window_mask = 31 computed, and the digit loop (DsmNafLoopSpec) seeded + with the all-zeros state whose invariant is trivial. + + POST: the 256 digits satisfy the NAF conditions (odd-or-zero, |d| < 16 — + exactly `NafDigits`, what dsm_loop_spec consumes) and their signed sum + reconstructs the scalar's little-endian byte value EXACTLY: + nafSum res 256 = V (as integers, no modular slack). + Requires V < 2^253 — canonical scalars, which the mul call sites provide. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.DsmNafLoadSpec +import Proofs.DsmNafLoopSpec +open Aeneas Aeneas.Std Result ControlFlow +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false +set_option maxRecDepth 8000 + +namespace CurveFieldProofs + +open Aeneas.Std.WP + +/-- **Scalar::non_adjacent_form(5)**: for a scalar whose 32-byte LE value V + is below 2^253, the result is a 256-entry NAF digit array — every digit + odd or zero with |d| < 16, and Σ naf[k]·2^k = V exactly. Both entry + masserts are discharged. -/ +theorem non_adjacent_form_spec (self : scalar.Scalar) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) + (V : ℕ) + (hVbytes : V = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248) + (hV : V < 2^253) : + scalar.Scalar.non_adjacent_form self 5#usize ⦃ res => + NafDigits res ∧ nafSum res 256 = (V : ℤ) ⦄ := by + unfold scalar.Scalar.non_adjacent_form + step with (massert_spec (5#usize ≥ 2#usize) (by scalar_tac)) as ⟨h2⟩ + step with (massert_spec (5#usize ≤ 8#usize) (by scalar_tac)) as ⟨h8⟩ + -- the LE load fills x_u64[0..3]; word 4 stays 0 + step with (naf_load_spec self (Array.repeat 5#usize 0#u64) + b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 + hb (by simp [List.replicate])) as ⟨v0, v1, v2, v3, ws, hws, hv0, hv1, hv2, hv3⟩ + -- width ← 1 <<< 5 (= 32), window_mask ← width − 1 (= 31) + step as ⟨wd, hwd⟩ + have hwdv : wd = 32#u64 := by clear * - hwd; scalar_tac + rw [hwdv] + step as ⟨mk, hmk⟩ + have hmkv : mk = 31#u64 := by clear * - hmk; scalar_tac + rw [hmkv] + -- the initial all-zeros digit state + have hz : ∀ k, k < 256 → nafDigit (Array.repeat 256#usize 0#i8) k = 0 := by + intro k hk + unfold nafDigit + rw [getElem!_pos (↑(Array.repeat 256#usize 0#i8) : List Std.I8) k + (by simp; omega)] + simp only [Array.repeat_val, List.getElem_replicate] + simp + have hsum0 : nafSum (Array.repeat 256#usize 0#i8) 256 = 0 := by + unfold nafSum + apply Finset.sum_eq_zero + intro k hk + rw [hz k (Finset.mem_range.mp hk)] + ring + -- the word-form value + have hVw : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by + rw [hVbytes, hv0, hv1, hv2, hv3] + ring + -- the digit loop from the trivial invariant + apply naf_digit_loop_spec ws v0 v1 v2 v3 V hws hVw hV 256 + (Array.repeat 256#usize 0#i8) 0#usize 0#u64 + (by scalar_tac) + (by scalar_tac) + (by intro h; simp at h) + (fun k _ hk => hz k hk) + (fun k hk => ⟨Or.inl (hz k hk), by rw [hz k hk]; norm_num, + by rw [hz k hk]; norm_num⟩) + (by simp [hsum0]) + +end CurveFieldProofs diff --git a/verification/check.sh b/verification/check.sh index 87e25a0..e80562a 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -57,6 +57,9 @@ PROOFS=( DsmLoopSpec DsmNafLoadSpec DsmNafMath + DsmNafLoopSpec + DsmNafSpec + DsmMulSpec ) # Fully-qualified certificate names; each must be axiom-clean. CERTS=( @@ -71,6 +74,10 @@ CERTS=( CurveFieldProofs.dsm_loop_spec CurveFieldProofs.naf_load_spec CurveFieldProofs.naf_exit + CurveFieldProofs.naf_digit_loop_spec + CurveFieldProofs.non_adjacent_form_spec + CurveFieldProofs.run_basepoint + CurveFieldProofs.vartime_double_base_mul_spec ) # Imports needed so every certificate in CERTS is in scope for the audit. AUDIT_IMPORTS=( @@ -81,6 +88,8 @@ AUDIT_IMPORTS=( Proofs.DsmLoopSpec Proofs.DsmNafLoadSpec Proofs.DsmNafMath + Proofs.DsmNafSpec + Proofs.DsmMulSpec ) # ── Phase 0: resource + integrity guards ──────────────────────────────────── diff --git a/verification/gen/CurveField/FunsExternal.lean b/verification/gen/CurveField/FunsExternal.lean index 8226dd4..ce51856 100644 --- a/verification/gen/CurveField/FunsExternal.lean +++ b/verification/gen/CurveField/FunsExternal.lean @@ -340,14 +340,6 @@ axiom axiom backend.serial.scalar_mul.variable_base.mul : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint -/-- [curve25519_dalek::backend::serial::scalar_mul::vartime_double_base::mul]: - Source: 'curve25519-dalek/src/backend/serial/scalar_mul/vartime_double_base.rs', lines 23:0-72:1 - Visibility: public -/ -axiom backend.serial.scalar_mul.vartime_double_base.mul - : - scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result - edwards.EdwardsPoint - /-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx2::mul]: Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2 Visibility: public -/