proofs/crypto/secp256k1/reduce.bend source
proofs/crypto/secp256k1/reduce.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/reduce.src; edit the .srcimport Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../src/crypto/secp256k1/limbs.bend as Limport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Lgimport ../../lib/arith.bend as ARimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../math/natural/arith.bend as NRimport ../../math/typed/width.bend as WWimport ./semiring.bend as SRimport ./limbs.bend as LVimport ./ineq.bend as Iimport ./bounds.bend as B# The folding reduction modulo m = 2^256 - c (src/crypto/secp256k1/limbs.bend# fold / rounds / canon): with x = lo + 2^256 hi, x = (lo + c hi) + m hi, so# a fold keeps x mod m; bounds on the folds (the arguments of# libsecp256k1's secp256k1_fe_mul_inner and secp256k1_scalar_reduce_512)# bring a product below 2^256 in 3 folds for p and 4 for n; one conditional# subtraction then gives x mod m. The modulus is written 1 + mp, the shape# of the division lemmas (proofs/math/natural/arith.bend), and 2^256 is# C.shift(256n, one) with one == 1.# x = lo + hi 2^256 for lo, hi the first 16 limbs and the restdef 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}: %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} %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} %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} {==}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}: %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} %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} {==}# x = fold(x) + hi mdef 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}: %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} {==}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}: %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} %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} %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} {==}# ---- bounds ----# T a < T b gives a < bdef 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}: match c: case True{}: hc case False{}: +le = AR.mul_le(b, a, t, N.not_lt_le(a, b, hc)) 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)))# the high part of x < 2^256 H is below Hdef 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}: +t = C.shift(256n, one) +hi = LV.ev(L.drop(16n, xs)) +lo = LV.ev(L.take(16n, xs)) +le = I.le_add_l(lo, Nat.mul(hi, t)) +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) 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), {==})# a fold of x < 2^256 H (low 16 limbs fine) is below 2^256 + H cdef 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}: +lo = LV.ev(L.take(16n, xs)) +hi = LV.ev(L.drop(16n, xs)) +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)) +hl = AR.mul_le(hi, hh, LV.ev(c), N.lt_le(hi, hh, hi_lt(one, h1, xs, hh, hx))) 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))# lo + h t < d when lo + (1 + h) t < t + ddef 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}: %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} %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} hx# (the hi >= 1 case) lo + h t < d with d + c <= t: h = 0, and then lo + c < tdef 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}: match h: case 0n: +hl = I.lt_subst_l(Nat.add(lo, 0n), lo, d, NA.add_zero(lo), hs) +s1 = I.lt_le_add(lo, cv, d, cv, hl, N.le_refl(cv)) +s2 = N.lt_le_trans(Nat.add(lo, cv), Nat.add(d, cv), t, s1, hd) %Equal.sym(Nat, f, Nat.add(lo, Nat.mul(1n, cv)), ef) : {Nat.is_lt(_, t) == True{} : Bool} %Equal.sym(Nat, Nat.mul(1n, cv), cv, SR.one_mul(cv)) : {Nat.is_lt(Nat.add(lo, _), t) == True{} : Bool} s2 case 1n+ +g: +le1 = N.le_trans(d, Nat.add(d, cv), t, N.le_add_right(d, cv), hd) +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)))) 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))))# the hi = 0 case: the fold is lodef 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}: %Equal.sym(Nat, f, Nat.add(lo, Nat.mul(0n, cv)), ef) : {Nat.is_lt(_, t) == True{} : Bool} %Equal.sym(Nat, Nat.mul(0n, cv), 0n, SR.zero_mul(cv)) : {Nat.is_lt(Nat.add(lo, _), t) == True{} : Bool} %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {Nat.is_lt(_, t) == True{} : Bool} lldef 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}: match hi: case 0n: fold_lt2_z(t, lo, cv, f, ll, ef) case 1n+ +h: 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)# a fold of x < 2^256 + D (low 16 limbs fine), with D + c <= 2^256, is below 2^256def 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}: +t = C.shift(256n, one) +lo = LV.ev(L.take(16n, xs)) +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)) 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))# ---- selection ----def pick_one(+x: Nat, +y: Nat) -> {L.pick1(1n, x, y) == x : Nat}: %Equal.sym(Nat, Nat.mul(x, 1n), x, NA.mul_one(x)) : {Nat.add(_, Nat.mul(y, 0n)) == x : Nat} %Equal.sym(Nat, Nat.mul(y, 0n), 0n, NA.mul_zero(y)) : {Nat.add(x, _) == x : Nat} %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {_ == x : Nat} {==}def pick_zero(+x: Nat, +y: Nat) -> {L.pick1(0n, x, y) == y : Nat}: %Equal.sym(Nat, Nat.mul(x, 0n), 0n, NA.mul_zero(x)) : {Nat.add(_, Nat.mul(y, 1n)) == y : Nat} %Equal.sym(Nat, Nat.mul(y, 1n), y, NA.mul_one(y)) : {Nat.add(0n, _) == y : Nat} %Equal.sym(Nat, Nat.add(0n, y), y, SR.zero_add(y)) : {_ == y : Nat} {==}# select(1, xs, ys) == xs and select(0, xs, ys) == ys for lists of n limbsdef 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>}: match n xs ys: case 0n Nil{} _: {==} case 0n x <> xt _: Empty.absurd({L.select(1n, x <> xt, ys) == x <> xt : List<&2, Nat>}, Lg.false_true(hx)) case 1n+k Nil{} _: Empty.absurd({L.select(1n, [], ys) == [] : List<&2, Nat>}, Lg.false_true(hx)) case 1n+k x <> xt Nil{}: Empty.absurd({L.select(1n, x <> xt, []) == x <> xt : List<&2, Nat>}, Lg.false_true(hy)) case 1n+ +k +x <> +xt +y <> +yt: +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)) %Equal.sym(List<&2, Nat>, L.select(1n, xt, yt), xt, e1) : {L.pick1(1n, x, y) <> _ == x <> xt : List<&2, Nat>} %Equal.sym(Nat, L.pick1(1n, x, y), x, pick_one(x, y)) : {_ <> xt == x <> xt : List<&2, Nat>} {==}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>}: match n xs ys: case 0n Nil{} Nil{}: {==} case 0n Nil{} y <> yt: Empty.absurd({L.select(0n, [], y <> yt) == y <> yt : List<&2, Nat>}, Lg.false_true(hy)) case 0n x <> xt _: Empty.absurd({L.select(0n, x <> xt, ys) == ys : List<&2, Nat>}, Lg.false_true(hx)) case 1n+k Nil{} _: Empty.absurd({L.select(0n, [], ys) == ys : List<&2, Nat>}, Lg.false_true(hx)) case 1n+k x <> xt Nil{}: Empty.absurd({L.select(0n, x <> xt, []) == [] : List<&2, Nat>}, Lg.false_true(hy)) case 1n+ +k +x <> +xt +y <> +yt: +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)) %Equal.sym(List<&2, Nat>, L.select(0n, xt, yt), yt, e1) : {L.pick1(0n, x, y) <> _ == y <> yt : List<&2, Nat>} %Equal.sym(Nat, L.pick1(0n, x, y), y, pick_zero(x, y)) : {_ <> yt == y <> yt : List<&2, Nat>} {==}# ---- the conditional subtraction ----# v + cv = lo < t = m + cv: v < m, and v mod m = vdef 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}: +s1 = I.lt_subst_l(lo, Nat.add(v, cv), t, Equal.sym(Nat, Nat.add(v, cv), lo, eu), ll) +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) +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) Equal.sym(Nat, Nat.mod(v, 1n+mp), v, NR.mod_of(0n, mp, v, s3))# v + cv = lo + t with t = m + cv, v < t, cv + cv < t: v mod m = lodef 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}: +m = {1n+mp : Nat} # v = lo + m +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)))) +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)))) # lo < cv < m +s1 = I.lt_subst_l(v, Nat.add(lo, m), t, e2, hv) +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) +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) +s4 = I.lt_subst_r(Nat.add(cv, cv), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht), hcc) +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) +s6 = N.lt_trans(lo, cv, m, s3, s5) # v mod m = (lo + 1 m) mod m = lo %Equal.sym(Nat, v, Nat.add(lo, 1n+mp), e2) : {lo == Nat.mod(_, 1n+mp) : Nat} %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} %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} %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} %Equal.sym(Nat, Nat.mod(lo, 1n+mp), lo, NR.mod_of(0n, mp, lo, s6)) : {lo == _ : Nat} {==}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}: %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} %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} {==}# the carried sum t + c is below 2 2^256, so its part above 2^256 is 0 or 1def 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}: +tt = C.shift(256n, one) +u = L.carry(32n, L.add(t, c), 0n) +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) +s1 = I.lt_le_add(LV.ev(t), LV.ev(c), tt, tt, hv, N.lt_le(LV.ev(c), tt, hc)) +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) +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) hi_lt(one, h1, u, 2n, s3)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}: match b: case 0n: +u = L.carry(32n, L.add(t, c), 0n) +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) +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)) +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)), 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), 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)))))) %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} canon0_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, ll, es) case 1n: +u = L.carry(32n, L.add(t, c), 0n) +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) +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)), 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), 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)))))) %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} canon1_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, hv, hcc, es) case 2n+ +k: 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))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}: %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} 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))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}: match b: case 0n: +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) %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} ht16 case 1n: +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) %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} hu16 case 2n+ +k: 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))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}: %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} 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))# ---- the fold rounds ----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}: LV.carry_v(32n, L.fold(c, xs), 0n)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}: %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} %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} {==}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}: B.carry_limbs(one, h1, 32n, 16n, ys, 0n, {==})# below 2^256 H after a round, from below 2^256 H' before (H = 1 + H' c)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}: %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} fold_lt1(one, h1, c, xs, hh, hlo, hx)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}: match hi: case 0n: %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} %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} %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} {==} case 1n+ +k: Empty.absurd({LV.ev(L.take(16n, xs)) == LV.ev(xs) : Nat}, N.lt_zero_absurd(k, h0))# x below 2^256 (16 limbs fine): the first 16 limbs are all of itdef 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}: +tt = C.shift(256n, one) +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) +h0 = hi_lt(one, h1, xs, 1n, hx1) take_small_h(xs, LV.ev(L.drop(16n, xs)), tt, h0, split256(one, h1, xs))