proofs/crypto/secp256k1/limbs.bend source
proofs/crypto/secp256k1/limbs.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/limbs.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/lemmas/proofs/nat_algebra.bend as NAimport ../../math/natural/arith.bend as NRimport ../../math/typed/width.bend as WWimport ./semiring.bend as SR# The limb lists of src/crypto/secp256k1/limbs.bend and their values: every# operation is exact on natural numbers (Fiat-Crypto's unsaturated limbs,# Erbsen et al. 2019: the value of the limb list is the number; with Nat# limbs there is no overflow to rule out in the value, and the run-time# bound 2^48 is a separate statement). ev is the value without `one`;# ev_value relates it to spec/crypto/secp256k1/field.bend's value.def ev(xs: List<&2, Nat>) -> Nat: match xs: case Nil{}: 0n case x <> t: Nat.add(x, C.shift(16n, ev(t)))# y at limb position n: y 2^(16 n)def pos(n: Nat, +y: Nat) -> Nat: match n: case 0n: y case 1n+k: C.shift(16n, pos(k, y))# 256 as a shift of one (the checker expands 2^8 in 256 steps, well# within its depth)def b8(+one: Nat, +h1: {one == 1n : Nat}) -> {C.shift(8n, one) == 256n : Nat}: %Equal.sym(Nat, one, 1n, h1) : {C.shift(8n, _) == 256n : Nat} {==}def m256(+y: Nat) -> {Nat.mul(y, 256n) == C.shift(8n, y) : Nat}: %Equal.sym(Nat, C.shift(8n, y), Nat.mul(y, C.shift(8n, 1n)), WW.shift_mul(8n, y)) : {Nat.mul(y, 256n) == _ : Nat} {==}def mul_one_l(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(one, x) == x : Nat}: %Equal.sym(Nat, one, 1n, h1) : {Nat.mul(_, x) == x : Nat} SR.one_mul(x)def ev_value(+one: Nat, +h1: {one == 1n : Nat}, xs: List<&2, Nat>) -> {FS.value(one, xs) == ev(xs) : Nat}: match xs: case Nil{}: {==} case +x <> +t: %Equal.sym(Nat, Nat.mul(one, x), x, mul_one_l(one, h1, x)) : {Nat.add(_, C.shift(16n, FS.digits(one, t))) == Nat.add(x, C.shift(16n, ev(t))) : Nat} %Equal.sym(Nat, FS.digits(one, t), ev(t), ev_value(one, h1, t)) : {Nat.add(x, C.shift(16n, _)) == Nat.add(x, C.shift(16n, ev(t))) : Nat} {==}# ---- sums, scalings, products ----def add_v(xs: List<&2, Nat>, ys: List<&2, Nat>) -> {ev(L.add(xs, ys)) == Nat.add(ev(xs), ev(ys)) : Nat}: match xs ys: case Nil{} Nil{}: {==} case Nil{} y <> yt: {==} case +x <> +xt Nil{}: Equal.sym(Nat, Nat.add(ev(x <> xt), 0n), ev(x <> xt), NA.add_zero(ev(x <> xt))) case +x <> +xt +y <> +yt: %Equal.sym(Nat, ev(L.add(xt, yt)), Nat.add(ev(xt), ev(yt)), add_v(xt, yt)) : {Nat.add(Nat.add(x, y), C.shift(16n, _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, C.shift(16n, Nat.add(ev(xt), ev(yt))), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))), WW.shift_add(16n, ev(xt), ev(yt))) : {Nat.add(Nat.add(x, y), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(x, y), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(x, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))), NA.add_assoc(x, y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(C.shift(16n, ev(xt)), Nat.add(y, C.shift(16n, ev(yt)))), NA.add_swap(y, C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))) : {Nat.add(x, _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(x, Nat.add(C.shift(16n, ev(xt)), _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_swap(x, C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(_, Nat.add(y, C.shift(16n, ev(yt)))) : Nat} %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(Nat.add(C.shift(16n, ev(xt)), x), _) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(xt)), x), Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_assoc(C.shift(16n, ev(xt)), x, Nat.add(C.shift(16n, ev(yt)), y))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == _ : Nat} %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(C.shift(16n, ev(xt)), _) : Nat} {==}def scal_v(+a: Nat, ys: List<&2, Nat>) -> {ev(L.scal(a, ys)) == Nat.mul(ev(ys), a) : Nat}: match ys: case Nil{}: {==} case +y <> +yt: %Equal.sym(Nat, ev(L.scal(a, yt)), Nat.mul(ev(yt), a), scal_v(a, yt)) : {Nat.add(Nat.mul(y, a), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat} %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(_, C.shift(16n, Nat.mul(ev(yt), a))) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat} %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(Nat.mul(a, y), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat} %Equal.sym(Nat, Nat.add(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt)))), Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)), NA.add_comm(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt))))) : {_ == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat} %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.mul(_, a) : Nat} %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(yt)), y), a), Nat.add(Nat.mul(C.shift(16n, ev(yt)), a), Nat.mul(y, a)), NA.mul_add_right(C.shift(16n, ev(yt)), y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == _ : Nat} %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(yt)), a), C.shift(16n, Nat.mul(ev(yt), a)), WW.shift_mul_l(16n, ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(_, Nat.mul(y, a)) : Nat} %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, _), Nat.mul(y, a)) : Nat} %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), _) : Nat} {==}def conv_v(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> {ev(L.conv(xs, ys)) == Nat.mul(ev(xs), ev(ys)) : Nat}: match xs: case Nil{}: {==} case +x <> +xt: %Equal.sym(Nat, ev(L.add(L.scal(x, ys), 0n <> L.conv(xt, ys))), Nat.add(ev(L.scal(x, ys)), ev(0n <> L.conv(xt, ys))), add_v(L.scal(x, ys), 0n <> L.conv(xt, ys))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat} %Equal.sym(Nat, ev(L.scal(x, ys)), Nat.mul(ev(ys), x), scal_v(x, ys)) : {Nat.add(_, ev(0n <> L.conv(xt, ys))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat} %Equal.sym(Nat, ev(L.conv(xt, ys)), Nat.mul(ev(xt), ev(ys)), conv_v(xt, ys)) : {Nat.add(Nat.mul(ev(ys), x), Nat.add(0n, C.shift(16n, _))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat} %Equal.sym(Nat, Nat.add(0n, C.shift(16n, Nat.mul(ev(xt), ev(ys)))), C.shift(16n, Nat.mul(ev(xt), ev(ys))), SR.zero_add(C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {Nat.add(Nat.mul(ev(ys), x), _) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat} %Equal.sym(Nat, Nat.add(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys)))), Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)), NA.add_comm(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.mul(_, ev(ys)) : Nat} %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(xt)), x), ev(ys)), Nat.add(Nat.mul(C.shift(16n, ev(xt)), ev(ys)), Nat.mul(x, ev(ys))), NA.mul_add_right(C.shift(16n, ev(xt)), x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == _ : Nat} %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(xt)), ev(ys)), C.shift(16n, Nat.mul(ev(xt), ev(ys))), WW.shift_mul_l(16n, ev(xt), ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(_, Nat.mul(x, ev(ys))) : Nat} %Equal.sym(Nat, Nat.mul(x, ev(ys)), Nat.mul(ev(ys), x), NA.mul_comm(x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), _) : Nat} {==}# ---- positions ----def pos_add(n: Nat, +x: Nat, +y: Nat) -> {pos(n, Nat.add(x, y)) == Nat.add(pos(n, x), pos(n, y)) : Nat}: match n: case 0n: {==} case 1n+ +k: %Equal.sym(Nat, pos(k, Nat.add(x, y)), Nat.add(pos(k, x), pos(k, y)), pos_add(k, x, y)) : {C.shift(16n, _) == Nat.add(C.shift(16n, pos(k, x)), C.shift(16n, pos(k, y))) : Nat} %Equal.sym(Nat, C.shift(16n, Nat.add(pos(k, x), pos(k, y))), Nat.add(C.shift(16n, pos(k, x)), C.shift(16n, pos(k, y))), WW.shift_add(16n, pos(k, x), pos(k, y))) : {_ == Nat.add(C.shift(16n, pos(k, x)), C.shift(16n, pos(k, y))) : Nat} {==}def pos_zero(n: Nat) -> {pos(n, 0n) == 0n : Nat}: match n: case 0n: {==} case 1n+ +k: %Equal.sym(Nat, pos(k, 0n), 0n, pos_zero(k)) : {C.shift(16n, _) == 0n : Nat} %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {_ == 0n : Nat} {==}def pos_mul(n: Nat, +x: Nat, +y: Nat) -> {pos(n, Nat.mul(x, y)) == Nat.mul(pos(n, x), y) : Nat}: match n: case 0n: {==} case 1n+ +k: %Equal.sym(Nat, pos(k, Nat.mul(x, y)), Nat.mul(pos(k, x), y), pos_mul(k, x, y)) : {C.shift(16n, _) == Nat.mul(C.shift(16n, pos(k, x)), y) : Nat} %Equal.sym(Nat, Nat.mul(C.shift(16n, pos(k, x)), y), C.shift(16n, Nat.mul(pos(k, x), y)), WW.shift_mul_l(16n, pos(k, x), y)) : {C.shift(16n, Nat.mul(pos(k, x), y)) == _ : Nat} {==}# ev(xs) = ev(take n xs) + 2^(16 n) ev(drop n xs)def take_drop_v(n: Nat, xs: List<&2, Nat>) -> {ev(xs) == Nat.add(ev(L.take(n, xs)), pos(n, ev(L.drop(n, xs)))) : Nat}: match n xs: case 0n Nil{}: {==} case 0n x <> t: {==} case 1n+ +k Nil{}: %Equal.sym(Nat, pos(k, 0n), 0n, pos_zero(k)) : {0n == Nat.add(0n, C.shift(16n, _)) : Nat} %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {0n == Nat.add(0n, _) : Nat} %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {0n == _ : Nat} {==} case 1n+ +k +x <> +t: %Equal.sym(Nat, ev(t), Nat.add(ev(L.take(k, t)), pos(k, ev(L.drop(k, t)))), take_drop_v(k, t)) : {Nat.add(x, C.shift(16n, _)) == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat} %Equal.sym(Nat, C.shift(16n, Nat.add(ev(L.take(k, t)), pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, ev(L.take(k, t))), C.shift(16n, pos(k, ev(L.drop(k, t))))), WW.shift_add(16n, ev(L.take(k, t)), pos(k, ev(L.drop(k, t))))) : {Nat.add(x, _) == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat} %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(L.take(k, t))), C.shift(16n, pos(k, ev(L.drop(k, t)))))), Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))), NA.add_swap(x, C.shift(16n, ev(L.take(k, t))), C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x), NA.add_comm(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), _) == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(L.take(k, t)))), Nat.add(C.shift(16n, ev(L.take(k, t))), x), NA.add_comm(x, C.shift(16n, ev(L.take(k, t))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x)) == Nat.add(_, C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(L.take(k, t))), x), C.shift(16n, pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))), NA.add_assoc(C.shift(16n, ev(L.take(k, t))), x, C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x)) == _ : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x), NA.add_comm(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x)) == Nat.add(C.shift(16n, ev(L.take(k, t))), _) : Nat} {==}def hd_tl_v(xs: List<&2, Nat>) -> {ev(xs) == Nat.add(L.hd0(xs), C.shift(16n, ev(L.tl(xs)))) : Nat}: match xs: case Nil{}: {==} case x <> t: {==}# ---- 16-bit limbs from bytes ----def lohi(+s: Nat) -> {Nat.add(L.lo16(s), C.shift(16n, L.hi16(s))) == s : Nat}: %Equal.sym(Nat, s, Nat.add(Nat.mul(Nat.div(s, 256n), 256n), Nat.mod(s, 256n)), NR.dm_eq(255n, s)) : {Nat.add(Nat.add(Nat.mod(s, 256n), Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == _ : Nat} %Equal.sym(Nat, Nat.div(s, 256n), Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)), NR.dm_eq(255n, Nat.div(s, 256n))) : {Nat.add(Nat.add(Nat.mod(s, 256n), Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(Nat.mul(_, 256n), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), m256(Nat.mod(Nat.div(s, 256n), 256n))) : {Nat.add(Nat.add(Nat.mod(s, 256n), _), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)), 256n), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)), 256n), C.shift(8n, Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n))), m256(Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)))) : {Nat.add(Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(_, Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), m256(Nat.div(Nat.div(s, 256n), 256n))) : {Nat.add(Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(C.shift(8n, Nat.add(_, Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n)), NA.add_comm(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)))) : {Nat.add(_, C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.add(Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)))), NA.add_assoc(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)))) : {_ == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.add(Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n)), NA.add_comm(Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)))) : {Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), _) == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))), NA.add_swap(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) : {_ == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.add(C.shift(8n, C.shift(8n, Nat.div(Nat.div(s, 256n), 256n))), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), WW.shift_add(8n, C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))) : {Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) == Nat.add(_, Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, C.shift(8n, C.shift(8n, Nat.div(Nat.div(s, 256n), 256n))), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), SR.shift_shift(8n, 8n, Nat.div(Nat.div(s, 256n), 256n))) : {Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) == Nat.add(Nat.add(_, C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))), NA.add_assoc(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) : {Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) == _ : Nat} {==}def horner_v(xs: List<&2, Nat>) -> {L.horner(xs) == ev(xs) : Nat}: match xs: case Nil{}: {==} case +x <> +t: %Equal.sym(Nat, L.horner(t), ev(t), horner_v(t)) : {Nat.add(Nat.mul(Nat.mul(_, 256n), 256n), x) == Nat.add(x, C.shift(16n, ev(t))) : Nat} %Equal.sym(Nat, Nat.mul(ev(t), 256n), C.shift(8n, ev(t)), m256(ev(t))) : {Nat.add(Nat.mul(_, 256n), x) == Nat.add(x, C.shift(16n, ev(t))) : Nat} %Equal.sym(Nat, Nat.mul(C.shift(8n, ev(t)), 256n), C.shift(8n, C.shift(8n, ev(t))), m256(C.shift(8n, ev(t)))) : {Nat.add(_, x) == Nat.add(x, C.shift(16n, ev(t))) : Nat} %Equal.sym(Nat, C.shift(8n, C.shift(8n, ev(t))), C.shift(16n, ev(t)), SR.shift_shift(8n, 8n, ev(t))) : {Nat.add(_, x) == Nat.add(x, C.shift(16n, ev(t))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), x) == _ : Nat} {==}# a carry pass keeps the value: the carry in plus the limbsdef carry_v(n: Nat, xs: List<&2, Nat>, +u: Nat) -> {ev(L.carry(n, xs, u)) == Nat.add(u, ev(xs)) : Nat}: match n xs: case 0n Nil{}: %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(u, _) == Nat.add(u, 0n) : Nat} %Equal.sym(Nat, Nat.add(u, 0n), u, NA.add_zero(u)) : {_ == Nat.add(u, 0n) : Nat} %Equal.sym(Nat, Nat.add(u, 0n), u, NA.add_zero(u)) : {u == _ : Nat} {==} case 0n +x <> +t: %Equal.sym(Nat, L.horner(x <> t), ev(x <> t), horner_v(x <> t)) : {Nat.add(Nat.add(u, _), C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(Nat.add(u, _), C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(_, C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), 0n), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_zero(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == Nat.add(u, _) : Nat} %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == _ : Nat} {==} case 1n+ +k Nil{}: %Equal.sym(Nat, ev(L.carry(k, [], L.hi16(Nat.add(u, 0n)))), Nat.add(L.hi16(Nat.add(u, 0n)), ev([])), carry_v(k, [], L.hi16(Nat.add(u, 0n)))) : {Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, _)) == Nat.add(u, 0n) : Nat} %Equal.sym(Nat, Nat.add(L.hi16(Nat.add(u, 0n)), 0n), L.hi16(Nat.add(u, 0n)), NA.add_zero(L.hi16(Nat.add(u, 0n)))) : {Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, _)) == Nat.add(u, 0n) : Nat} %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, L.hi16(Nat.add(u, 0n)))), Nat.add(u, 0n), lohi(Nat.add(u, 0n))) : {_ == Nat.add(u, 0n) : Nat} {==} case 1n+ +k +x <> +t: %Equal.sym(Nat, ev(L.carry(k, t, L.hi16(Nat.add(u, x)))), Nat.add(L.hi16(Nat.add(u, x)), ev(t)), carry_v(k, t, L.hi16(Nat.add(u, x)))) : {Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, _)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, C.shift(16n, Nat.add(L.hi16(Nat.add(u, x)), ev(t))), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t))), WW.shift_add(16n, L.hi16(Nat.add(u, x)), ev(t))) : {Nat.add(L.lo16(Nat.add(u, x)), _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, x)), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t)))), Nat.add(Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), C.shift(16n, ev(t))), Equal.sym(Nat, Nat.add(Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), C.shift(16n, ev(t))), Nat.add(L.lo16(Nat.add(u, x)), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t)))), NA.add_assoc(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t))))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), Nat.add(u, x), lohi(Nat.add(u, x))) : {Nat.add(_, C.shift(16n, ev(t))) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(Nat.add(u, x), C.shift(16n, ev(t))), Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))), NA.add_assoc(u, x, C.shift(16n, ev(t)))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(u, _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat} %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == Nat.add(u, _) : Nat} %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == _ : Nat} {==}