1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/reduce.src; edit the .src 2 import Base 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/crypto/secp256k1/field.bend as FS 5 import ../../../src/crypto/secp256k1/limbs.bend as L 6 import ../../lib/nat.bend as N 7 import ../../lib/logic.bend as Lg 8 import ../../lib/arith.bend as AR 9 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 10 import ../../math/natural/arith.bend as NR 11 import ../../math/typed/width.bend as WW 12 import ./semiring.bend as SR 13 import ./limbs.bend as LV 14 import ./ineq.bend as I 15 import ./bounds.bend as B 16 17 # The folding reduction modulo m = 2^256 - c (src/crypto/secp256k1/limbs.bend 18 # fold / rounds / canon): with x = lo + 2^256 hi, x = (lo + c hi) + m hi, so 19 # a fold keeps x mod m; bounds on the folds (the arguments of 20 # libsecp256k1's secp256k1_fe_mul_inner and secp256k1_scalar_reduce_512) 21 # bring a product below 2^256 in 3 folds for p and 4 for n; one conditional 22 # subtraction then gives x mod m. The modulus is written 1 + mp, the shape 23 # of the division lemmas (proofs/math/natural/arith.bend), and 2^256 is 24 # C.shift(256n, one) with one == 1. 25 26 # x = lo + hi 2^256 for lo, hi the first 16 limbs and the rest 27 def split256(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>) -> {LV.ev(xs) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat}: 28 %Equal.sym(Nat, LV.ev(xs), Nat.add(LV.ev(L.take(16n, xs)), LV.pos(16n, LV.ev(L.drop(16n, xs)))), LV.take_drop_v(16n, xs)) : {_ == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat} 29 %Equal.sym(Nat, LV.pos(16n, LV.ev(L.drop(16n, xs))), C.shift(256n, LV.ev(L.drop(16n, xs))), B.pos16(LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat} 30 %Equal.sym(Nat, C.shift(256n, LV.ev(L.drop(16n, xs))), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one)), WW.shift_mul_one(256n, one, h1, LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat} 31 {==} 32 33 def fold_v(+c: List<&2, Nat>, +xs: List<&2, Nat>) -> {LV.ev(L.fold(c, xs)) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))) : Nat}: 34 %Equal.sym(Nat, LV.ev(L.add(L.take(16n, xs), L.conv(L.drop(16n, xs), c))), Nat.add(LV.ev(L.take(16n, xs)), LV.ev(L.conv(L.drop(16n, xs), c))), LV.add_v(L.take(16n, xs), L.conv(L.drop(16n, xs), c))) : {_ == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))) : Nat} 35 %Equal.sym(Nat, LV.ev(L.conv(L.drop(16n, xs), c)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.conv_v(L.drop(16n, xs), c)) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))) : Nat} 36 {==} 37 38 # x = fold(x) + hi m 39 def fold_eq(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +xs: List<&2, Nat>) -> {LV.ev(xs) == Nat.add(LV.ev(L.fold(c, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat}: 40 %Equal.sym(Nat, LV.ev(xs), Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))), split256(one, h1, xs)) : {_ == Nat.add(LV.ev(L.fold(c, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 41 %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+mp, LV.ev(c)), Equal.sym(Nat, Nat.add(1n+mp, LV.ev(c)), C.shift(256n, one), hm)) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), _)) == Nat.add(LV.ev(L.fold(c, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 42 %Equal.sym(Nat, LV.ev(L.fold(c, xs)), Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), fold_v(c, xs)) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(1n+mp, LV.ev(c)))) == Nat.add(_, Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 43 %Equal.sym(Nat, 1n+mp, Nat.add(mp, 1n), SR.succ_add(1n, mp)) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(_, LV.ev(c)))) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 44 %Equal.sym(Nat, Nat.add(Nat.add(mp, 1n), LV.ev(c)), Nat.add(mp, Nat.add(1n, LV.ev(c))), NA.add_assoc(mp, 1n, LV.ev(c))) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), _)) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 45 %Equal.sym(Nat, Nat.add(1n, LV.ev(c)), Nat.add(LV.ev(c), 1n), NA.add_comm(1n, LV.ev(c))) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(mp, _))) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 46 %Equal.sym(Nat, Nat.add(mp, Nat.add(LV.ev(c), 1n)), Nat.add(LV.ev(c), Nat.add(mp, 1n)), NA.add_swap(mp, LV.ev(c), 1n)) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), _)) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 47 %Equal.sym(Nat, Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(LV.ev(c), Nat.add(mp, 1n))), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(mp, 1n))), NA.mul_add_left(LV.ev(L.drop(16n, xs)), LV.ev(c), Nat.add(mp, 1n))) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 48 %Equal.sym(Nat, Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(mp, 1n)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), Nat.mul(LV.ev(L.drop(16n, xs)), 1n)), NA.mul_add_left(LV.ev(L.drop(16n, xs)), mp, 1n)) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), _)) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 49 %Equal.sym(Nat, Nat.mul(LV.ev(L.drop(16n, xs)), 1n), LV.ev(L.drop(16n, xs)), NA.mul_one(LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), _))) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 50 %Equal.sym(Nat, Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.drop(16n, xs))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)), NA.add_comm(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.take(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), _)) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 51 %Equal.sym(Nat, Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), NA.add_swap(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 52 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(LV.ev(L.take(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)))), NA.add_swap(LV.ev(L.take(16n, xs)), LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)))) : {_ == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 53 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), NA.add_swap(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))) : {Nat.add(LV.ev(L.drop(16n, xs)), _) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 54 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))), NA.add_comm(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), _)) == Nat.add(Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 55 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs))), NA.add_comm(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(_, Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)) : Nat} 56 %Equal.sym(Nat, 1n+mp, Nat.add(mp, 1n), SR.succ_add(1n, mp)) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs))), Nat.mul(LV.ev(L.drop(16n, xs)), _)) : Nat} 57 %Equal.sym(Nat, Nat.mul(LV.ev(L.drop(16n, xs)), Nat.add(mp, 1n)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), Nat.mul(LV.ev(L.drop(16n, xs)), 1n)), NA.mul_add_left(LV.ev(L.drop(16n, xs)), mp, 1n)) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs))), _) : Nat} 58 %Equal.sym(Nat, Nat.mul(LV.ev(L.drop(16n, xs)), 1n), LV.ev(L.drop(16n, xs)), NA.mul_one(LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs))), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), _)) : Nat} 59 %Equal.sym(Nat, Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.drop(16n, xs))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)), NA.add_comm(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs))), _) : Nat} 60 %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(LV.ev(L.take(16n, xs)), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)))), NA.add_assoc(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.take(16n, xs)), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == _ : Nat} 61 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), Nat.add(LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))), NA.add_swap(LV.ev(L.take(16n, xs)), LV.ev(L.drop(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), _) : Nat} 62 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))), NA.add_comm(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), mp))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(LV.ev(L.drop(16n, xs)), _)) : Nat} 63 %Equal.sym(Nat, Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))), Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))), NA.add_swap(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) : {Nat.add(LV.ev(L.drop(16n, xs)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), mp), LV.ev(L.take(16n, xs))))) == _ : Nat} 64 {==} 65 66 def fold_mod(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +xs: List<&2, Nat>) -> {Nat.mod(LV.ev(L.fold(c, xs)), 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 67 %Equal.sym(Nat, LV.ev(xs), Nat.add(LV.ev(L.fold(c, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)), fold_eq(one, h1, mp, c, hm, xs)) : {Nat.mod(LV.ev(L.fold(c, xs)), 1n+mp) == Nat.mod(_, 1n+mp) : Nat} 68 %Equal.sym(Nat, Nat.add(LV.ev(L.fold(c, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp)), Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp), LV.ev(L.fold(c, xs))), NA.add_comm(LV.ev(L.fold(c, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp))) : {Nat.mod(LV.ev(L.fold(c, xs)), 1n+mp) == Nat.mod(_, 1n+mp) : Nat} 69 %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(LV.ev(L.drop(16n, xs)), 1n+mp), LV.ev(L.fold(c, xs))), 1n+mp), Nat.mod(LV.ev(L.fold(c, xs)), 1n+mp), NR.absorb(mp, LV.ev(L.drop(16n, xs)), LV.ev(L.fold(c, xs)))) : {Nat.mod(LV.ev(L.fold(c, xs)), 1n+mp) == _ : Nat} 70 {==} 71 72 # ---- bounds ---- 73 74 # T a < T b gives a < b 75 def mul_lt_cancel(+t: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(Nat.mul(a, t), Nat.mul(b, t)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}: 76 match c: 77 case True{}: 78 hc 79 case False{}: 80 +le = AR.mul_le(b, a, t, N.not_lt_le(a, b, hc)) 81 Empty.absurd({Nat.is_lt(a, b) == True{} : Bool}, Lg.true_not_false(Nat.is_lt(Nat.mul(a, t), Nat.mul(b, t)), h, N.le_not_lt(Nat.mul(a, t), Nat.mul(b, t), le))) 82 83 # the high part of x < 2^256 H is below H 84 def hi_lt(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hh: Nat, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(hh, C.shift(256n, one))) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.drop(16n, xs)), hh) == True{} : Bool}: 85 +t = C.shift(256n, one) 86 +hi = LV.ev(L.drop(16n, xs)) 87 +lo = LV.ev(L.take(16n, xs)) 88 +le = I.le_add_l(lo, Nat.mul(hi, t)) 89 +le2 = I.le_subst_r(Nat.mul(hi, t), Nat.add(lo, Nat.mul(hi, t)), LV.ev(xs), Equal.sym(Nat, LV.ev(xs), Nat.add(lo, Nat.mul(hi, t)), split256(one, h1, xs)), le) 90 mul_lt_cancel(t, hi, hh, N.le_lt_trans(Nat.mul(hi, t), LV.ev(xs), Nat.mul(hh, t), le2, hx), Nat.is_lt(hi, hh), {==}) 91 92 # a fold of x < 2^256 H (low 16 limbs fine) is below 2^256 + H c 93 def fold_lt1(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>, +hh: Nat, +hlo: {FS.limbs16(one, 16n, L.take(16n, xs)) == True{} : Bool}, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(hh, C.shift(256n, one))) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.fold(c, xs)), Nat.add(C.shift(256n, one), Nat.mul(hh, LV.ev(c)))) == True{} : Bool}: 94 +lo = LV.ev(L.take(16n, xs)) 95 +hi = LV.ev(L.drop(16n, xs)) 96 +ll = I.lt_subst_r(lo, LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, xs), hlo)) 97 +hl = AR.mul_le(hi, hh, LV.ev(c), N.lt_le(hi, hh, hi_lt(one, h1, xs, hh, hx))) 98 I.lt_subst_l(Nat.add(lo, Nat.mul(hi, LV.ev(c))), LV.ev(L.fold(c, xs)), Nat.add(C.shift(256n, one), Nat.mul(hh, LV.ev(c))), Equal.sym(Nat, LV.ev(L.fold(c, xs)), Nat.add(lo, Nat.mul(hi, LV.ev(c))), fold_v(c, xs)), I.lt_le_add(lo, Nat.mul(hi, LV.ev(c)), C.shift(256n, one), Nat.mul(hh, LV.ev(c)), ll, hl)) 99 100 # lo + h t < d when lo + (1 + h) t < t + d 101 def cancel_t(+t: Nat, +lo: Nat, +h: Nat, +d: Nat, +hx: {Nat.is_lt(Nat.add(lo, Nat.mul(1n+h, t)), Nat.add(t, d)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(lo, Nat.mul(h, t)), d) == True{} : Bool}: 102 %Equal.sym(Bool, Nat.is_lt(Nat.add(lo, Nat.mul(h, t)), d), Nat.is_lt(Nat.add(t, Nat.add(lo, Nat.mul(h, t))), Nat.add(t, d)), Equal.sym(Bool, Nat.is_lt(Nat.add(t, Nat.add(lo, Nat.mul(h, t))), Nat.add(t, d)), Nat.is_lt(Nat.add(lo, Nat.mul(h, t)), d), WW.lt_cancel_l(t, Nat.add(lo, Nat.mul(h, t)), d))) : {_ == True{} : Bool} 103 %Equal.sym(Nat, Nat.add(t, Nat.add(lo, Nat.mul(h, t))), Nat.add(lo, Nat.add(t, Nat.mul(h, t))), NA.add_swap(t, lo, Nat.mul(h, t))) : {Nat.is_lt(_, Nat.add(t, d)) == True{} : Bool} 104 hx 105 106 # (the hi >= 1 case) lo + h t < d with d + c <= t: h = 0, and then lo + c < t 107 def fold_lt2_h(+t: Nat, +lo: Nat, +cv: Nat, +d: Nat, +f: Nat, +hd: {Nat.is_le(Nat.add(d, cv), t) == True{} : Bool}, h: Nat, +hs: {Nat.is_lt(Nat.add(lo, Nat.mul(h, t)), d) == True{} : Bool}, +ef: {f == Nat.add(lo, Nat.mul(1n+h, cv)) : Nat}) -> {Nat.is_lt(f, t) == True{} : Bool}: 108 match h: 109 case 0n: 110 +hl = I.lt_subst_l(Nat.add(lo, 0n), lo, d, NA.add_zero(lo), hs) 111 +s1 = I.lt_le_add(lo, cv, d, cv, hl, N.le_refl(cv)) 112 +s2 = N.lt_le_trans(Nat.add(lo, cv), Nat.add(d, cv), t, s1, hd) 113 %Equal.sym(Nat, f, Nat.add(lo, Nat.mul(1n, cv)), ef) : {Nat.is_lt(_, t) == True{} : Bool} 114 %Equal.sym(Nat, Nat.mul(1n, cv), cv, SR.one_mul(cv)) : {Nat.is_lt(Nat.add(lo, _), t) == True{} : Bool} 115 s2 116 case 1n+ +g: 117 +le1 = N.le_trans(d, Nat.add(d, cv), t, N.le_add_right(d, cv), hd) 118 +le2 = N.le_trans(t, Nat.add(t, Nat.mul(g, t)), Nat.add(lo, Nat.add(t, Nat.mul(g, t))), N.le_add_right(t, Nat.mul(g, t)), I.le_add_l(lo, Nat.add(t, Nat.mul(g, t)))) 119 Empty.absurd({Nat.is_lt(f, t) == True{} : Bool}, Lg.true_not_false(Nat.is_lt(Nat.add(lo, Nat.add(t, Nat.mul(g, t))), d), hs, N.le_not_lt(Nat.add(lo, Nat.add(t, Nat.mul(g, t))), d, N.le_trans(d, t, Nat.add(lo, Nat.add(t, Nat.mul(g, t))), le1, le2)))) 120 121 # the hi = 0 case: the fold is lo 122 def fold_lt2_z(+t: Nat, +lo: Nat, +cv: Nat, +f: Nat, +ll: {Nat.is_lt(lo, t) == True{} : Bool}, +ef: {f == Nat.add(lo, Nat.mul(0n, cv)) : Nat}) -> {Nat.is_lt(f, t) == True{} : Bool}: 123 %Equal.sym(Nat, f, Nat.add(lo, Nat.mul(0n, cv)), ef) : {Nat.is_lt(_, t) == True{} : Bool} 124 %Equal.sym(Nat, Nat.mul(0n, cv), 0n, SR.zero_mul(cv)) : {Nat.is_lt(Nat.add(lo, _), t) == True{} : Bool} 125 %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {Nat.is_lt(_, t) == True{} : Bool} 126 ll 127 128 def fold_lt2_hi(+t: Nat, +lo: Nat, +cv: Nat, +d: Nat, +f: Nat, +x: Nat, +hd: {Nat.is_le(Nat.add(d, cv), t) == True{} : Bool}, +ll: {Nat.is_lt(lo, t) == True{} : Bool}, +hx: {Nat.is_lt(x, Nat.add(t, d)) == True{} : Bool}, hi: Nat, +ex: {x == Nat.add(lo, Nat.mul(hi, t)) : Nat}, +ef: {f == Nat.add(lo, Nat.mul(hi, cv)) : Nat}) -> {Nat.is_lt(f, t) == True{} : Bool}: 129 match hi: 130 case 0n: 131 fold_lt2_z(t, lo, cv, f, ll, ef) 132 case 1n+ +h: 133 fold_lt2_h(t, lo, cv, d, f, hd, h, cancel_t(t, lo, h, d, I.lt_subst_l(x, Nat.add(lo, Nat.mul(1n+h, t)), Nat.add(t, d), ex, hx)), ef) 134 135 # a fold of x < 2^256 + D (low 16 limbs fine), with D + c <= 2^256, is below 2^256 136 def fold_lt2(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>, +d: Nat, +hd: {Nat.is_le(Nat.add(d, LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hlo: {FS.limbs16(one, 16n, L.take(16n, xs)) == True{} : Bool}, +hx: {Nat.is_lt(LV.ev(xs), Nat.add(C.shift(256n, one), d)) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.fold(c, xs)), C.shift(256n, one)) == True{} : Bool}: 137 +t = C.shift(256n, one) 138 +lo = LV.ev(L.take(16n, xs)) 139 +ll = I.lt_subst_r(lo, LV.pos(16n, one), t, B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, xs), hlo)) 140 fold_lt2_hi(t, lo, LV.ev(c), d, LV.ev(L.fold(c, xs)), LV.ev(xs), hd, ll, hx, LV.ev(L.drop(16n, xs)), split256(one, h1, xs), fold_v(c, xs)) 141 142 # ---- selection ---- 143 144 def pick_one(+x: Nat, +y: Nat) -> {L.pick1(1n, x, y) == x : Nat}: 145 %Equal.sym(Nat, Nat.mul(x, 1n), x, NA.mul_one(x)) : {Nat.add(_, Nat.mul(y, 0n)) == x : Nat} 146 %Equal.sym(Nat, Nat.mul(y, 0n), 0n, NA.mul_zero(y)) : {Nat.add(x, _) == x : Nat} 147 %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {_ == x : Nat} 148 {==} 149 150 def pick_zero(+x: Nat, +y: Nat) -> {L.pick1(0n, x, y) == y : Nat}: 151 %Equal.sym(Nat, Nat.mul(x, 0n), 0n, NA.mul_zero(x)) : {Nat.add(_, Nat.mul(y, 1n)) == y : Nat} 152 %Equal.sym(Nat, Nat.mul(y, 1n), y, NA.mul_one(y)) : {Nat.add(0n, _) == y : Nat} 153 %Equal.sym(Nat, Nat.add(0n, y), y, SR.zero_add(y)) : {_ == y : Nat} 154 {==} 155 156 # select(1, xs, ys) == xs and select(0, xs, ys) == ys for lists of n limbs 157 def sel_one(+one: Nat, n: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, n, ys) == True{} : Bool}) -> {L.select(1n, xs, ys) == xs : List<&2, Nat>}: 158 match n xs ys: 159 case 0n Nil{} _: 160 {==} 161 case 0n x <> xt _: 162 Empty.absurd({L.select(1n, x <> xt, ys) == x <> xt : List<&2, Nat>}, Lg.false_true(hx)) 163 case 1n+k Nil{} _: 164 Empty.absurd({L.select(1n, [], ys) == [] : List<&2, Nat>}, Lg.false_true(hx)) 165 case 1n+k x <> xt Nil{}: 166 Empty.absurd({L.select(1n, x <> xt, []) == x <> xt : List<&2, Nat>}, Lg.false_true(hy)) 167 case 1n+ +k +x <> +xt +y <> +yt: 168 +e1 = sel_one(one, k, xt, yt, Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx), Lg.and_right(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)) 169 %Equal.sym(List<&2, Nat>, L.select(1n, xt, yt), xt, e1) : {L.pick1(1n, x, y) <> _ == x <> xt : List<&2, Nat>} 170 %Equal.sym(Nat, L.pick1(1n, x, y), x, pick_one(x, y)) : {_ <> xt == x <> xt : List<&2, Nat>} 171 {==} 172 173 def sel_zero(+one: Nat, n: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, n, ys) == True{} : Bool}) -> {L.select(0n, xs, ys) == ys : List<&2, Nat>}: 174 match n xs ys: 175 case 0n Nil{} Nil{}: 176 {==} 177 case 0n Nil{} y <> yt: 178 Empty.absurd({L.select(0n, [], y <> yt) == y <> yt : List<&2, Nat>}, Lg.false_true(hy)) 179 case 0n x <> xt _: 180 Empty.absurd({L.select(0n, x <> xt, ys) == ys : List<&2, Nat>}, Lg.false_true(hx)) 181 case 1n+k Nil{} _: 182 Empty.absurd({L.select(0n, [], ys) == ys : List<&2, Nat>}, Lg.false_true(hx)) 183 case 1n+k x <> xt Nil{}: 184 Empty.absurd({L.select(0n, x <> xt, []) == [] : List<&2, Nat>}, Lg.false_true(hy)) 185 case 1n+ +k +x <> +xt +y <> +yt: 186 +e1 = sel_zero(one, k, xt, yt, Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx), Lg.and_right(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)) 187 %Equal.sym(List<&2, Nat>, L.select(0n, xt, yt), yt, e1) : {L.pick1(0n, x, y) <> _ == y <> yt : List<&2, Nat>} 188 %Equal.sym(Nat, L.pick1(0n, x, y), y, pick_zero(x, y)) : {_ <> yt == y <> yt : List<&2, Nat>} 189 {==} 190 191 # ---- the conditional subtraction ---- 192 193 # v + cv = lo < t = m + cv: v < m, and v mod m = v 194 def canon0_val(+mp: Nat, +v: Nat, +cv: Nat, +lo: Nat, +t: Nat, +ht: {Nat.add(1n+mp, cv) == t : Nat}, +ll: {Nat.is_lt(lo, t) == True{} : Bool}, +eu: {Nat.add(v, cv) == lo : Nat}) -> {v == Nat.mod(v, 1n+mp) : Nat}: 195 +s1 = I.lt_subst_l(lo, Nat.add(v, cv), t, Equal.sym(Nat, Nat.add(v, cv), lo, eu), ll) 196 +s2 = I.lt_subst_r(Nat.add(v, cv), t, Nat.add(1n+mp, cv), Equal.sym(Nat, Nat.add(1n+mp, cv), t, ht), s1) 197 +s3 = Equal.trans(Bool, Nat.is_lt(v, 1n+mp), Nat.is_lt(Nat.add(v, cv), Nat.add(1n+mp, cv)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(v, cv), Nat.add(1n+mp, cv)), Nat.is_lt(v, 1n+mp), WW.lt_cancel_r(v, 1n+mp, cv)), s2) 198 Equal.sym(Nat, Nat.mod(v, 1n+mp), v, NR.mod_of(0n, mp, v, s3)) 199 200 # v + cv = lo + t with t = m + cv, v < t, cv + cv < t: v mod m = lo 201 def canon1_val(+mp: Nat, +v: Nat, +cv: Nat, +lo: Nat, +t: Nat, +ht: {Nat.add(1n+mp, cv) == t : Nat}, +hv: {Nat.is_lt(v, t) == True{} : Bool}, +hcc: {Nat.is_lt(Nat.add(cv, cv), t) == True{} : Bool}, +eu: {Nat.add(v, cv) == Nat.add(lo, t) : Nat}) -> {lo == Nat.mod(v, 1n+mp) : Nat}: 202 +m = {1n+mp : Nat} 203 # v = lo + m 204 +e1 = Equal.trans(Nat, Nat.add(v, cv), Nat.add(lo, t), Nat.add(Nat.add(lo, m), cv), eu, Equal.trans(Nat, Nat.add(lo, t), Nat.add(lo, Nat.add(m, cv)), Nat.add(Nat.add(lo, m), cv), Equal.cong(Nat, Nat, z => Nat.add(lo, z), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht)), Equal.sym(Nat, Nat.add(Nat.add(lo, m), cv), Nat.add(lo, Nat.add(m, cv)), NA.add_assoc(lo, m, cv)))) 205 +e2 = NR.add_cancel(cv, v, Nat.add(lo, m), Equal.trans(Nat, Nat.add(cv, v), Nat.add(v, cv), Nat.add(cv, Nat.add(lo, m)), NA.add_comm(cv, v), Equal.trans(Nat, Nat.add(v, cv), Nat.add(Nat.add(lo, m), cv), Nat.add(cv, Nat.add(lo, m)), e1, NA.add_comm(Nat.add(lo, m), cv)))) 206 # lo < cv < m 207 +s1 = I.lt_subst_l(v, Nat.add(lo, m), t, e2, hv) 208 +s2 = I.lt_subst_r(Nat.add(lo, m), t, Nat.add(cv, m), Equal.trans(Nat, t, Nat.add(m, cv), Nat.add(cv, m), Equal.sym(Nat, Nat.add(m, cv), t, ht), NA.add_comm(m, cv)), s1) 209 +s3 = Equal.trans(Bool, Nat.is_lt(lo, cv), Nat.is_lt(Nat.add(lo, m), Nat.add(cv, m)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(lo, m), Nat.add(cv, m)), Nat.is_lt(lo, cv), WW.lt_cancel_r(lo, cv, m)), s2) 210 +s4 = I.lt_subst_r(Nat.add(cv, cv), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht), hcc) 211 +s5 = Equal.trans(Bool, Nat.is_lt(cv, m), Nat.is_lt(Nat.add(cv, cv), Nat.add(m, cv)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(cv, cv), Nat.add(m, cv)), Nat.is_lt(cv, m), WW.lt_cancel_r(cv, m, cv)), s4) 212 +s6 = N.lt_trans(lo, cv, m, s3, s5) 213 # v mod m = (lo + 1 m) mod m = lo 214 %Equal.sym(Nat, v, Nat.add(lo, 1n+mp), e2) : {lo == Nat.mod(_, 1n+mp) : Nat} 215 %Equal.sym(Nat, Nat.add(lo, 1n+mp), Nat.add(1n+mp, lo), NA.add_comm(lo, 1n+mp)) : {lo == Nat.mod(_, 1n+mp) : Nat} 216 %Equal.sym(Nat, 1n+mp, Nat.mul(1n, 1n+mp), Equal.sym(Nat, Nat.mul(1n, 1n+mp), 1n+mp, SR.one_mul(1n+mp))) : {lo == Nat.mod(Nat.add(_, lo), 1n+mp) : Nat} 217 %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(1n, 1n+mp), lo), 1n+mp), Nat.mod(lo, 1n+mp), NR.absorb(mp, 1n, lo)) : {lo == _ : Nat} 218 %Equal.sym(Nat, Nat.mod(lo, 1n+mp), lo, NR.mod_of(0n, mp, lo, s6)) : {lo == _ : Nat} 219 {==} 220 221 def u_val(+c: List<&2, Nat>, +t: List<&2, Nat>) -> {LV.ev(L.carry(32n, L.add(t, c), 0n)) == Nat.add(LV.ev(t), LV.ev(c)) : Nat}: 222 %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(t, c), 0n)), Nat.add(0n, LV.ev(L.add(t, c))), LV.carry_v(32n, L.add(t, c), 0n)) : {_ == Nat.add(LV.ev(t), LV.ev(c)) : Nat} 223 %Equal.sym(Nat, LV.ev(L.add(t, c)), Nat.add(LV.ev(t), LV.ev(c)), LV.add_v(t, c)) : {Nat.add(0n, _) == Nat.add(LV.ev(t), LV.ev(c)) : Nat} 224 {==} 225 226 # the carried sum t + c is below 2 2^256, so its part above 2^256 is 0 or 1 227 def u_hi(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +t: List<&2, Nat>, +hv: {Nat.is_lt(LV.ev(t), C.shift(256n, one)) == True{} : Bool}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), 2n) == True{} : Bool}: 228 +tt = C.shift(256n, one) 229 +u = L.carry(32n, L.add(t, c), 0n) 230 +hc = N.le_lt_trans(LV.ev(c), Nat.add(LV.ev(c), LV.ev(c)), tt, N.le_add_right(LV.ev(c), LV.ev(c)), hcc) 231 +s1 = I.lt_le_add(LV.ev(t), LV.ev(c), tt, tt, hv, N.lt_le(LV.ev(c), tt, hc)) 232 +s2 = I.lt_subst_l(Nat.add(LV.ev(t), LV.ev(c)), LV.ev(u), Nat.add(tt, tt), Equal.sym(Nat, LV.ev(u), Nat.add(LV.ev(t), LV.ev(c)), u_val(c, t)), s1) 233 +s3 = I.lt_subst_r(LV.ev(u), Nat.add(tt, tt), Nat.mul(2n, tt), Equal.trans(Nat, Nat.add(tt, tt), Nat.add(tt, Nat.add(tt, 0n)), Nat.mul(2n, tt), Equal.cong(Nat, Nat, z => Nat.add(tt, z), tt, Nat.add(tt, 0n), Equal.sym(Nat, Nat.add(tt, 0n), tt, NA.add_zero(tt))), {==}), s2) 234 hi_lt(one, h1, u, 2n, s3) 235 236 def canon_u(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +t: List<&2, Nat>, +ht16: {FS.limbs16(one, 16n, t) == True{} : Bool}, +hv: {Nat.is_lt(LV.ev(t), C.shift(256n, one)) == True{} : Bool}, +htc: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, b: Nat, +eb: {LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))) == b : Nat}, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {LV.ev(L.select(b, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == Nat.mod(LV.ev(t), 1n+mp) : Nat}: 237 match b: 238 case 0n: 239 +u = L.carry(32n, L.add(t, c), 0n) 240 +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) 241 +ll = I.lt_subst_r(LV.ev(L.take(16n, u)), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, u), hu16)) 242 +es = Equal.trans(Nat, Nat.add(LV.ev(t), LV.ev(c)), LV.ev(u), LV.ev(L.take(16n, u)), Equal.sym(Nat, LV.ev(u), Nat.add(LV.ev(t), LV.ev(c)), u_val(c, t)), 243 Equal.trans(Nat, LV.ev(u), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), LV.ev(L.take(16n, u)), split256(one, h1, u), 244 Equal.trans(Nat, Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(0n, C.shift(256n, one))), LV.ev(L.take(16n, u)), Equal.cong(Nat, Nat, z => Nat.add(LV.ev(L.take(16n, u)), Nat.mul(z, C.shift(256n, one))), LV.ev(L.drop(16n, u)), 0n, eb), NA.add_zero(LV.ev(L.take(16n, u)))))) 245 %Equal.sym(List<&2, Nat>, L.select(0n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), t, sel_zero(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {LV.ev(_) == Nat.mod(LV.ev(t), 1n+mp) : Nat} 246 canon0_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, ll, es) 247 case 1n: 248 +u = L.carry(32n, L.add(t, c), 0n) 249 +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) 250 +es = Equal.trans(Nat, Nat.add(LV.ev(t), LV.ev(c)), LV.ev(u), Nat.add(LV.ev(L.take(16n, u)), C.shift(256n, one)), Equal.sym(Nat, LV.ev(u), Nat.add(LV.ev(t), LV.ev(c)), u_val(c, t)), 251 Equal.trans(Nat, LV.ev(u), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), C.shift(256n, one)), split256(one, h1, u), 252 Equal.trans(Nat, Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(1n, C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), C.shift(256n, one)), Equal.cong(Nat, Nat, z => Nat.add(LV.ev(L.take(16n, u)), Nat.mul(z, C.shift(256n, one))), LV.ev(L.drop(16n, u)), 1n, eb), Equal.cong(Nat, Nat, z => Nat.add(LV.ev(L.take(16n, u)), z), Nat.mul(1n, C.shift(256n, one)), C.shift(256n, one), SR.one_mul(C.shift(256n, one)))))) 253 %Equal.sym(List<&2, Nat>, L.select(1n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), L.take(16n, L.carry(32n, L.add(t, c), 0n)), sel_one(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {LV.ev(_) == Nat.mod(LV.ev(t), 1n+mp) : Nat} 254 canon1_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, hv, hcc, es) 255 case 2n+ +k: 256 Empty.absurd({LV.ev(L.select(2n+k, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == Nat.mod(LV.ev(t), 1n+mp) : Nat}, N.lt_zero_absurd(k, hb)) 257 258 def canon_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +t: List<&2, Nat>, +ht16: {FS.limbs16(one, 16n, t) == True{} : Bool}, +hv: {Nat.is_lt(LV.ev(t), C.shift(256n, one)) == True{} : Bool}, +htc: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.canon(c, t)) == Nat.mod(LV.ev(t), 1n+mp) : Nat}: 259 %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(t, c), 0n)))) : {LV.ev(L.select(_, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == Nat.mod(LV.ev(t), 1n+mp) : Nat} 260 canon_u(one, h1, mp, c, t, ht16, hv, htc, hcc, LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), {==}, u_hi(one, h1, c, t, hv, hcc)) 261 262 def canon_lb(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +t: List<&2, Nat>, +ht16: {FS.limbs16(one, 16n, t) == True{} : Bool}, b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.select(b, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == True{} : Bool}: 263 match b: 264 case 0n: 265 +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) 266 %Equal.sym(List<&2, Nat>, L.select(0n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), t, sel_zero(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {FS.limbs16(one, 16n, _) == True{} : Bool} 267 ht16 268 case 1n: 269 +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) 270 %Equal.sym(List<&2, Nat>, L.select(1n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), L.take(16n, L.carry(32n, L.add(t, c), 0n)), sel_one(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {FS.limbs16(one, 16n, _) == True{} : Bool} 271 hu16 272 case 2n+ +k: 273 Empty.absurd({FS.limbs16(one, 16n, L.select(2n+k, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == True{} : Bool}, N.lt_zero_absurd(k, hb)) 274 275 def canon_limbs(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +t: List<&2, Nat>, +ht16: {FS.limbs16(one, 16n, t) == True{} : Bool}, +hv: {Nat.is_lt(LV.ev(t), C.shift(256n, one)) == True{} : Bool}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.canon(c, t)) == True{} : Bool}: 276 %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(t, c), 0n)))) : {FS.limbs16(one, 16n, L.select(_, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == True{} : Bool} 277 canon_lb(one, h1, c, t, ht16, LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), u_hi(one, h1, c, t, hv, hcc)) 278 279 # ---- the fold rounds ---- 280 281 def round_v(+c: List<&2, Nat>, +xs: List<&2, Nat>) -> {LV.ev(L.carry(32n, L.fold(c, xs), 0n)) == LV.ev(L.fold(c, xs)) : Nat}: 282 LV.carry_v(32n, L.fold(c, xs), 0n) 283 284 def round_mod(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +xs: List<&2, Nat>) -> {Nat.mod(LV.ev(L.carry(32n, L.fold(c, xs), 0n)), 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 285 %Equal.sym(Nat, LV.ev(L.carry(32n, L.fold(c, xs), 0n)), LV.ev(L.fold(c, xs)), round_v(c, xs)) : {Nat.mod(_, 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 286 %Equal.sym(Nat, Nat.mod(LV.ev(L.fold(c, xs)), 1n+mp), Nat.mod(LV.ev(xs), 1n+mp), fold_mod(one, h1, mp, c, hm, xs)) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 287 {==} 288 289 def round_lo(+one: Nat, +h1: {one == 1n : Nat}, +ys: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.take(16n, L.carry(32n, ys, 0n))) == True{} : Bool}: 290 B.carry_limbs(one, h1, 32n, 16n, ys, 0n, {==}) 291 292 # below 2^256 H after a round, from below 2^256 H' before (H = 1 + H' c) 293 def round_lt1(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>, +hh: Nat, +hlo: {FS.limbs16(one, 16n, L.take(16n, xs)) == True{} : Bool}, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(hh, C.shift(256n, one))) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.carry(32n, L.fold(c, xs), 0n)), Nat.add(C.shift(256n, one), Nat.mul(hh, LV.ev(c)))) == True{} : Bool}: 294 %Equal.sym(Nat, LV.ev(L.carry(32n, L.fold(c, xs), 0n)), LV.ev(L.fold(c, xs)), round_v(c, xs)) : {Nat.is_lt(_, Nat.add(C.shift(256n, one), Nat.mul(hh, LV.ev(c)))) == True{} : Bool} 295 fold_lt1(one, h1, c, xs, hh, hlo, hx) 296 297 def take_small_h(+xs: List<&2, Nat>, hi: Nat, +tt: Nat, +h0: {Nat.is_lt(hi, 1n) == True{} : Bool}, +es: {LV.ev(xs) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(hi, tt)) : Nat}) -> {LV.ev(L.take(16n, xs)) == LV.ev(xs) : Nat}: 298 match hi: 299 case 0n: 300 %Equal.sym(Nat, LV.ev(xs), Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(0n, tt)), es) : {LV.ev(L.take(16n, xs)) == _ : Nat} 301 %Equal.sym(Nat, Nat.mul(0n, tt), 0n, SR.zero_mul(tt)) : {LV.ev(L.take(16n, xs)) == Nat.add(LV.ev(L.take(16n, xs)), _) : Nat} 302 %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, xs)), 0n), LV.ev(L.take(16n, xs)), NA.add_zero(LV.ev(L.take(16n, xs)))) : {LV.ev(L.take(16n, xs)) == _ : Nat} 303 {==} 304 case 1n+ +k: 305 Empty.absurd({LV.ev(L.take(16n, xs)) == LV.ev(xs) : Nat}, N.lt_zero_absurd(k, h0)) 306 307 # x below 2^256 (16 limbs fine): the first 16 limbs are all of it 308 def take_small(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.take(16n, xs)) == LV.ev(xs) : Nat}: 309 +tt = C.shift(256n, one) 310 +hx1 = I.lt_subst_r(LV.ev(xs), tt, Nat.mul(1n, tt), Equal.sym(Nat, Nat.mul(1n, tt), tt, SR.one_mul(tt)), hx) 311 +h0 = hi_lt(one, h1, xs, 1n, hx1) 312 take_small_h(xs, LV.ev(L.drop(16n, xs)), tt, h0, split256(one, h1, xs))