~/bend-docscommunity

proofs/crypto/secp256k1/negate.bend source

proofs/crypto/secp256k1/negate.bend on the hub · documented module

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/negate.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/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 Bimport ./reduce.bend as R# Complements and the borrow-free negation of src/crypto/secp256k1/limbs.bend:# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16, and# negraw(c, b) + b = 2 m for m = 2^256 - c (so a + negraw(c, b) is congruent# to a - b), with 256 written as the symbolic 2^8 = C.shift(8n, one).def e255(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.sub(C.shift(8n, one), 1n) == 255n : Nat}:  %Equal.sym(Nat, one, 1n, h1) : {Nat.sub(C.shift(8n, _), 1n) == 255n : Nat}  {==}def bb_sq(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.mul(C.shift(8n, one), C.shift(8n, one)) == C.shift(16n, one) : Nat}:  %Equal.sym(Nat, Nat.mul(C.shift(8n, one), C.shift(8n, one)), C.shift(8n, Nat.mul(one, C.shift(8n, one))), WW.shift_mul_l(8n, one, C.shift(8n, one))) : {_ == C.shift(16n, one) : Nat}  %Equal.sym(Nat, Nat.mul(one, C.shift(8n, one)), C.shift(8n, one), LV.mul_one_l(one, h1, C.shift(8n, one))) : {C.shift(8n, _) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, C.shift(8n, C.shift(8n, one)), C.shift(16n, one), SR.shift_shift(8n, 8n, one)) : {_ == C.shift(16n, one) : Nat}  {==}def bb_pos(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(1n, C.shift(8n, one)) == True{} : Bool}:  %Equal.sym(Nat, one, 1n, h1) : {Nat.is_le(1n, C.shift(8n, _)) == True{} : Bool}  {==}# (B - 1) + 1 = Bdef pred_succ(+b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.add(Nat.sub(b, 1n), 1n) == b : Nat}:  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), Nat.add(1n, Nat.sub(b, 1n)), NA.add_comm(Nat.sub(b, 1n), 1n)) : {_ == b : Nat}  N.sub_add(b, 1n, h)# (B - 1) + (B - 1) B + 1 = B Bdef digit_max(+b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n) == Nat.mul(b, b) : Nat}:  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n), Nat.add(Nat.sub(b, 1n), Nat.add(Nat.mul(Nat.sub(b, 1n), b), 1n)), NA.add_assoc(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b), 1n)) : {_ == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.add(Nat.mul(Nat.sub(b, 1n), b), 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b)), NA.add_comm(Nat.mul(Nat.sub(b, 1n), b), 1n)) : {Nat.add(Nat.sub(b, 1n), _) == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b))), Nat.add(Nat.add(Nat.sub(b, 1n), 1n), Nat.mul(Nat.sub(b, 1n), b)), Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(b, 1n), 1n), Nat.mul(Nat.sub(b, 1n), b)), Nat.add(Nat.sub(b, 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b))), NA.add_assoc(Nat.sub(b, 1n), 1n, Nat.mul(Nat.sub(b, 1n), b)))) : {_ == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), b, pred_succ(b, h)) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, b, Nat.mul(b, 1n), Equal.sym(Nat, Nat.mul(b, 1n), b, NA.mul_one(b))) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.mul(b, 1n), Nat.mul(1n, b), NA.mul_comm(b, 1n)) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.add(Nat.mul(1n, b), Nat.mul(Nat.sub(b, 1n), b)), Nat.mul(Nat.add(1n, Nat.sub(b, 1n)), b), Equal.sym(Nat, Nat.mul(Nat.add(1n, Nat.sub(b, 1n)), b), Nat.add(Nat.mul(1n, b), Nat.mul(Nat.sub(b, 1n), b)), NA.mul_add_right(1n, Nat.sub(b, 1n), b))) : {_ == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.add(1n, Nat.sub(b, 1n)), Nat.add(Nat.sub(b, 1n), 1n), NA.add_comm(1n, Nat.sub(b, 1n))) : {Nat.mul(_, b) == Nat.mul(b, b) : Nat}  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), b, pred_succ(b, h)) : {Nat.mul(_, b) == Nat.mul(b, b) : Nat}  {==}# x < 2^16: x div 256 < 256def hi_byte_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(x, 256n), 256n) == True{} : Bool}:  +bq = C.shift(8n, one)  +hi = Nat.div(x, 256n)  +le = I.le_subst_r(Nat.mul(hi, 256n), Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), x, Equal.sym(Nat, x, Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)), N.le_add_right(Nat.mul(hi, 256n), Nat.mod(x, 256n)))  +le2 = I.le_subst_l(Nat.mul(hi, 256n), Nat.mul(hi, bq), x, Equal.cong(Nat, Nat, z => Nat.mul(hi, z), 256n, bq, Equal.sym(Nat, bq, 256n, LV.b8(one, h1))), le)  +s1 = N.le_lt_trans(Nat.mul(hi, bq), x, C.shift(16n, one), le2, hx)  +s2 = I.lt_subst_r(Nat.mul(hi, bq), C.shift(16n, one), Nat.mul(bq, bq), Equal.sym(Nat, Nat.mul(bq, bq), C.shift(16n, one), bb_sq(one, h1)), s1)  +s3 = R.mul_lt_cancel(bq, hi, bq, s2, Nat.is_lt(hi, bq), {==})  I.lt_subst_r(hi, bq, 256n, LV.b8(one, h1), s3)# (l + h B) + (h' B + l') = (l' + l) + (h' + h) Bdef combine(+l: Nat, +h: Nat, +h2: Nat, +l2: Nat, +b: Nat) -> {Nat.add(Nat.add(l, Nat.mul(h, b)), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}:  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.add(l, _), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}  %Equal.sym(Nat, Nat.add(l, Nat.mul(b, h)), Nat.add(Nat.mul(b, h), l), NA.add_comm(l, Nat.mul(b, h))) : {Nat.add(_, Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(_, l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_assoc(Nat.mul(b, h), l, Nat.add(Nat.mul(b, h2), l2))) : {_ == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), _) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}  %Equal.sym(Nat, Nat.add(l2, l), Nat.add(l, l2), NA.add_comm(l2, l)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(_, Nat.mul(Nat.add(h2, h), b)) : Nat}  %Equal.sym(Nat, Nat.add(h2, h), Nat.add(h, h2), NA.add_comm(h2, h)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.mul(_, b)) : Nat}  %Equal.sym(Nat, Nat.mul(Nat.add(h, h2), b), Nat.add(Nat.mul(h, b), Nat.mul(h2, b)), NA.mul_add_right(h, h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), _) : Nat}  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(_, Nat.mul(h2, b))) : Nat}  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), _)) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(l, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))), NA.add_assoc(l, l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}  %Equal.sym(Nat, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(Nat.mul(b, h), Nat.add(l2, Nat.mul(b, h2))), NA.add_swap(l2, Nat.mul(b, h), Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, _) : Nat}  %Equal.sym(Nat, Nat.add(l2, Nat.mul(b, h2)), Nat.add(Nat.mul(b, h2), l2), NA.add_comm(l2, Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, Nat.add(Nat.mul(b, h), _)) : Nat}  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_swap(l, Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.mul(b, h), _) : Nat}  {==}# comp1(x) + x + 1 = 2^16 for x < 2^16def comp1_v(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), 1n) == C.shift(16n, one) : Nat}:  +lo = Nat.mod(x, 256n)  +hi = Nat.div(x, 256n)  +hl = N.lt_succ_le(lo, 255n, NR.dm_lt(255n, x))  +hh = N.lt_succ_le(hi, 255n, hi_byte_lt(one, h1, x, hx))  %Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)) : {Nat.add(Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), _), 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n))), Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 256n)), combine(Nat.sub(255n, Nat.mod(x, 256n)), Nat.sub(255n, Nat.div(x, 256n)), Nat.div(x, 256n), Nat.mod(x, 256n), 256n)) : {Nat.add(_, 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, 256n, C.shift(8n, one), Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1))) : {Nat.add(Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), _)), 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), 255n, N.sub_add(255n, Nat.mod(x, 256n), hl)) : {Nat.add(Nat.add(_, Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 255n, N.sub_add(255n, Nat.div(x, 256n), hh)) : {Nat.add(Nat.add(255n, Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(_, Nat.mul(255n, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(Nat.sub(C.shift(8n, one), 1n), C.shift(8n, one))), 1n), Nat.mul(C.shift(8n, one), C.shift(8n, one)), digit_max(C.shift(8n, one), bb_pos(one, h1))) : {_ == C.shift(16n, one) : Nat}  bb_sq(one, h1)def comp1_o(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), one) == C.shift(16n, one) : Nat}:  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(L.comp1(x), x), _) == C.shift(16n, one) : Nat}  comp1_v(one, h1, x, hx)# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16def comp_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {Nat.add(Nat.add(LV.ev(L.comp(xs)), LV.ev(xs)), one) == LV.pos(n, one) : Nat}:  match n xs:    case 0n Nil{}:      {==}    case 0n x <> t:      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp(x <> t)), LV.ev(x <> t)), one) == LV.pos(0n, one) : Nat}, Lg.false_true(h))    case 1n+k Nil{}:      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp([])), LV.ev([])), one) == LV.pos(1n+k, one) : Nat}, Lg.false_true(h))    case 1n+ +k +x <> +t:      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)      %Equal.sym(Nat, LV.pos(k, one), Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), LV.pos(k, one), comp_v(one, h1, k, t, ht))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(x, C.shift(16n, LV.ev(t)))), one) == C.shift(16n, _) : Nat}      %Equal.sym(Nat, Nat.add(x, C.shift(16n, LV.ev(t))), Nat.add(C.shift(16n, LV.ev(t)), x), NA.add_comm(x, C.shift(16n, LV.ev(t)))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), _), one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(C.shift(16n, LV.ev(t)), x)), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), NA.add_assoc(L.comp1(x), C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))) : {Nat.add(_, one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), one), Nat.add(L.comp1(x), Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)), NA.add_assoc(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)) : {_ == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one)), NA.add_assoc(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x), one)) : {Nat.add(L.comp1(x), _) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(x, one)), NA.add_assoc(C.shift(16n, LV.ev(t)), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), _)) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _))) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}      %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one)), NA.add_assoc(LV.ev(L.comp(t)), LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == C.shift(16n, _) : Nat}      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))), Nat.add(C.shift(16n, LV.ev(L.comp(t))), C.shift(16n, Nat.add(LV.ev(t), one))), WW.shift_add(16n, LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(t), one)), Nat.add(C.shift(16n, LV.ev(t)), C.shift(16n, one)), WW.shift_add(16n, LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}      %Equal.sym(Nat, C.shift(16n, one), Nat.add(Nat.add(L.comp1(x), x), one), Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), C.shift(16n, one), comp1_o(one, h1, x, hx))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), Nat.add(L.comp1(x), Nat.add(x, one)), NA.add_assoc(L.comp1(x), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), _))) : Nat}      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), Nat.add(one, x))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x))), NA.add_swap(C.shift(16n, LV.ev(t)), L.comp1(x), Nat.add(one, x))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), NA.add_swap(C.shift(16n, LV.ev(L.comp(t))), L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}      {==}# ---- neg_raw(c, b) + b = m ----# b + c as 16 limbs, when b + c < 2^256def bc_limbs(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.norm16(L.add(b, c))) == True{} : Bool}:  B.carry_limbs(one, h1, 32n, 16n, L.add(b, c), 0n, {==})def bc_v(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>, +hbc: {Nat.is_lt(Nat.add(LV.ev(b), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.norm16(L.add(b, c))) == Nat.add(LV.ev(b), LV.ev(c)) : Nat}:  +x = L.carry(32n, L.add(b, c), 0n)  +ex = Equal.trans(Nat, LV.ev(x), LV.ev(L.add(b, c)), Nat.add(LV.ev(b), LV.ev(c)), LV.carry_v(32n, L.add(b, c), 0n), LV.add_v(b, c))  +hx = I.lt_subst_l(Nat.add(LV.ev(b), LV.ev(c)), LV.ev(x), C.shift(256n, one), Equal.sym(Nat, LV.ev(x), Nat.add(LV.ev(b), LV.ev(c)), ex), hbc)  %Equal.sym(Nat, LV.ev(L.take(16n, L.carry(32n, L.add(b, c), 0n))), LV.ev(L.carry(32n, L.add(b, c), 0n)), R.take_small(one, h1, L.carry(32n, L.add(b, c), 0n), hx)) : {_ == Nat.add(LV.ev(b), LV.ev(c)) : Nat}  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(b, c), 0n)), Nat.add(LV.ev(b), LV.ev(c)), ex) : {_ == Nat.add(LV.ev(b), LV.ev(c)) : Nat}  {==}# neg_raw(c, b) + b + c = 2^256def neg_t(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>, +hbc: {Nat.is_lt(Nat.add(LV.ev(b), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), Nat.add(LV.ev(b), LV.ev(c))) == C.shift(256n, one) : Nat}:  %Equal.sym(Nat, LV.ev(L.add(L.comp(L.norm16(L.add(b, c))), [1n])), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.add_v(L.comp(L.norm16(L.add(b, c))), [1n])) : {Nat.add(_, Nat.add(LV.ev(b), LV.ev(c))) == C.shift(256n, one) : Nat}  %Equal.sym(Nat, Nat.add(LV.ev(b), LV.ev(c)), LV.ev(L.norm16(L.add(b, c))), Equal.sym(Nat, LV.ev(L.norm16(L.add(b, c))), Nat.add(LV.ev(b), LV.ev(c)), bc_v(one, h1, c, b, hbc))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), _) == C.shift(256n, one) : Nat}  %Equal.sym(Nat, C.shift(256n, one), LV.pos(16n, one), Equal.sym(Nat, LV.pos(16n, one), C.shift(256n, one), B.pos16(one))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == _ : Nat}  %Equal.sym(Nat, LV.pos(16n, one), Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), one), LV.pos(16n, one), comp_v(one, h1, 16n, L.norm16(L.add(b, c)), bc_limbs(one, h1, c, b)))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == _ : Nat}  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), _) : Nat}  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(1n, _)), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}  %Equal.sym(Nat, Nat.add(1n, 0n), 1n, {==}) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), _), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), 1n), LV.ev(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(1n, LV.ev(L.norm16(L.add(b, c))))), NA.add_assoc(LV.ev(L.comp(L.norm16(L.add(b, c)))), 1n, LV.ev(L.norm16(L.add(b, c))))) : {_ == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}  %Equal.sym(Nat, Nat.add(1n, LV.ev(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n), NA.add_comm(1n, LV.ev(L.norm16(L.add(b, c))))) : {Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), _) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n)), NA.add_assoc(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c))), 1n)) : {Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n)) == _ : Nat}  {==}# neg_raw(c, b) + b = m, for b < m = 2^256 - cdef neg_v(+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}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:  +nb = LV.ev(L.neg_raw(c, b))  +bv = LV.ev(b)  +cv = LV.ev(c)  +hbc = I.lt_subst_r(Nat.add(bv, cv), Nat.add(1n+mp, cv), C.shift(256n, one), hm, N.lt_add_r2(bv, 1n+mp, cv, hb))  +e1 = Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(nb, Nat.add(bv, cv)), Nat.add(1n+mp, cv), NA.add_assoc(nb, bv, cv), Equal.trans(Nat, Nat.add(nb, Nat.add(bv, cv)), C.shift(256n, one), Nat.add(1n+mp, cv), neg_t(one, h1, c, b, hbc), Equal.sym(Nat, Nat.add(1n+mp, cv), C.shift(256n, one), hm)))  NR.add_cancel(cv, Nat.add(nb, bv), 1n+mp, Equal.trans(Nat, Nat.add(cv, Nat.add(nb, bv)), Nat.add(Nat.add(nb, bv), cv), Nat.add(cv, 1n+mp), NA.add_comm(cv, Nat.add(nb, bv)), Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(1n+mp, cv), Nat.add(cv, 1n+mp), e1, NA.add_comm(1n+mp, cv))))def neg_vv(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, FS.value(one, c)) == C.shift(256n, one) : Nat}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:  neg_v(one, h1, mp, c, Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), LV.ev_value(one, h1, c), hm), b, hb)# a + (m - b) = (a + m) - b, for b < mdef sub_mod(+mp: Nat, +a: Nat, +b: Nat, +nb: Nat, +hlt: {Nat.is_lt(b, 1n+mp) == True{} : Bool}, +hn: {Nat.add(nb, b) == 1n+mp : Nat}) -> {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), Nat.mod(b, 1n+mp)), 1n+mp) : Nat}:  %Equal.sym(Nat, Nat.mod(b, 1n+mp), b, NR.mod_of(0n, mp, b, hlt)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), _), 1n+mp) : Nat}  %Equal.sym(Nat, 1n+mp, Nat.add(nb, b), Equal.sym(Nat, Nat.add(nb, b), 1n+mp, hn)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, _), b), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.add(a, Nat.add(nb, b)), Nat.add(Nat.add(a, nb), b), Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(a, Nat.add(nb, b)), NA.add_assoc(a, nb, b))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(b, Nat.add(a, nb)), NA.add_comm(Nat.add(a, nb), b)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.sub(Nat.add(b, Nat.add(a, nb)), b), Nat.add(a, nb), N.add_sub_cancel(b, Nat.add(a, nb))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}  {==}