~/bend-docscommunity

proofs/crypto/secp256k1/listops.bend source

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

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/listops.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# Zero tests, equality, parity, comparison with m and small constants of# src/crypto/secp256k1/limbs.bend, against the values of the limbs.# ---- Bool facts ----def is_eq_add0(a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:  match a:    case 0n:      {==}    case 1n+k:      {==}def and_true(+b: Bool) -> {Bool.and(True{}, b) == b : Bool}:  {==}def and_assoc(a: Bool, +b: Bool, +c: Bool) -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}:  match a:    case True{}:      {==}    case False{}:      {==}# 2^16 y == 0 exactly when y == 0def sh_eq0(+y: Nat) -> {Nat.is_eq(C.shift(16n, y), 0n) == Nat.is_eq(y, 0n) : Bool}:  WW.shift_eq0(16n, y)# ---- is_zero ----def and_true_r(b: Bool) -> {Bool.and(b, True{}) == b : Bool}:  match b:    case True{}:      {==}    case False{}:      {==}def nonzero_v(xs: List<&2, Nat>, +acc: Nat) -> {Nat.is_eq(L.nonzero(xs, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), 0n)) : Bool}:  match xs:    case Nil{}:      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))    case +x <> +t:      %Equal.sym(Bool, Nat.is_eq(L.nonzero(t, Nat.add(acc, x)), 0n), Bool.and(Nat.is_eq(Nat.add(acc, x), 0n), Nat.is_eq(LV.ev(t), 0n)), nonzero_v(t, Nat.add(acc, x))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, x), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), is_eq_add0(acc, x)) : {Bool.and(_, Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(C.shift(16n, LV.ev(t)), 0n)), is_eq_add0(x, C.shift(16n, LV.ev(t)))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}      %Equal.sym(Bool, Nat.is_eq(C.shift(16n, LV.ev(t)), 0n), Nat.is_eq(LV.ev(t), 0n), sh_eq0(LV.ev(t))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), _)) : Bool}      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : Bool}      {==}def is_zero_v(+xs: List<&2, Nat>) -> {L.is_zero(xs) == Nat.is_eq(LV.ev(xs), 0n) : Bool}:  nonzero_v(xs, 0n)# ---- parity ----def parity_v(+xs: List<&2, Nat>) -> {Nat.mod(L.hd0(xs), 2n) == Nat.mod(LV.ev(xs), 2n) : Nat}:  match xs:    case Nil{}:      {==}    case +x <> +t:      Equal.sym(Nat, Nat.mod(Nat.add(x, C.shift(16n, LV.ev(t))), 2n), Nat.mod(x, 2n), WW.odd_limb(15n, x, LV.ev(t)))# ---- Bool from implications ----def iff_bool(p: Bool, q: Bool, f: {p == True{} : Bool} -> {q == True{} : Bool}, g: {q == True{} : Bool} -> {p == True{} : Bool}) -> {p == q : Bool}:  match p q:    case True{} True{}:      {==}    case False{} False{}:      {==}    case True{} False{}:      Empty.absurd({True{} == False{} : Bool}, Lg.false_true(f({==})))    case False{} True{}:      Empty.absurd({False{} == True{} : Bool}, Lg.false_true(g({==})))# ---- a limb and the rest are unique (x, y < 2^16) ----def w_succ(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+Nat.sub(C.shift(16n, one), 1n) == C.shift(16n, one) : Nat}:  N.sub_add(C.shift(16n, one), 1n, N.lt_succ_le_succ(0n, C.shift(16n, one), B.pos_pos(one, h1, 1n)))# x + 2^16 a = a W + x with W = 1 + wpdef digit_form(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +a: Nat) -> {Nat.add(x, C.shift(16n, a)) == Nat.add(Nat.mul(a, 1n+Nat.sub(C.shift(16n, one), 1n)), x) : Nat}:  %Equal.sym(Nat, 1n+Nat.sub(C.shift(16n, one), 1n), C.shift(16n, one), w_succ(one, h1)) : {Nat.add(x, C.shift(16n, a)) == Nat.add(Nat.mul(a, _), x) : Nat}  %Equal.sym(Nat, C.shift(16n, a), Nat.mul(a, C.shift(16n, one)), WW.shift_mul_one(16n, one, h1, a)) : {Nat.add(x, _) == Nat.add(Nat.mul(a, C.shift(16n, one)), x) : Nat}  %Equal.sym(Nat, Nat.add(x, Nat.mul(a, C.shift(16n, one))), Nat.add(Nat.mul(a, C.shift(16n, one)), x), NA.add_comm(x, Nat.mul(a, C.shift(16n, one)))) : {_ == Nat.add(Nat.mul(a, C.shift(16n, one)), x) : Nat}  {==}def lt_w(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(x, 1n+Nat.sub(C.shift(16n, one), 1n)) == True{} : Bool}:  %Equal.sym(Nat, 1n+Nat.sub(C.shift(16n, one), 1n), C.shift(16n, one), w_succ(one, h1)) : {Nat.is_lt(x, _) == True{} : Bool}  hxdef uniq_lo(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {x == y : Nat}:  +wp = Nat.sub(C.shift(16n, one), 1n)  +ex = Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), x, NR.mod_of(a, wp, x, lt_w(one, h1, x, hx)))  +ey = NR.mod_of(b, wp, y, lt_w(one, h1, y, hy))  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))  Equal.trans(Nat, x, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), y, ex, Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.mod(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), y, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))def uniq_hi(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {a == b : Nat}:  +wp = Nat.sub(C.shift(16n, one), 1n)  +ex = Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), a, NR.div_of(a, wp, x, lt_w(one, h1, x, hx)))  +ey = NR.div_of(b, wp, y, lt_w(one, h1, y, hy))  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))  Equal.trans(Nat, a, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), b, ex, Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.div(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), b, Equal.cong(Nat, Nat, z => Nat.div(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))def eq_digit_f(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +h: {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}) -> {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}:  +e = N.eq_from_is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), h)  +exy = uniq_lo(one, h1, x, y, a, b, hx, hy, e)  +eab = uniq_hi(one, h1, x, y, a, b, hx, hy, e)  Lg.and_intro(Nat.is_eq(x, y), Nat.is_eq(a, b), Lg.subst(Nat, z => {Nat.is_eq(x, z) == True{} : Bool}, x, y, exy, N.is_eq_refl(x)), Lg.subst(Nat, z => {Nat.is_eq(a, z) == True{} : Bool}, a, b, eab, N.is_eq_refl(a)))def eq_digit_g(+x: Nat, +y: Nat, +a: Nat, +b: Nat, +h: {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}) -> {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}:  +exy = N.eq_from_is_eq(x, y, Lg.and_left(Nat.is_eq(x, y), Nat.is_eq(a, b), h))  +eab = N.eq_from_is_eq(a, b, Lg.and_right(Nat.is_eq(x, y), Nat.is_eq(a, b), h))  %Equal.sym(Nat, x, y, exy) : {Nat.is_eq(Nat.add(_, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}  %Equal.sym(Nat, a, b, eab) : {Nat.is_eq(Nat.add(y, C.shift(16n, _)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}  N.is_eq_refl(Nat.add(y, C.shift(16n, b)))def eq_digit(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) : Bool}:  iff_bool(Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))), Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)), h => eq_digit_f(one, h1, x, y, a, b, hx, hy, h), h => eq_digit_g(x, y, a, b, h))# ---- eq ----# (x - y) + (y - x) == 0 exactly when x == ydef absdiff(x: Nat, y: Nat) -> {Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n) == Nat.is_eq(x, y) : Bool}:  match x y:    case 0n 0n:      {==}    case 0n 1n+q:      {==}    case 1n+p 0n:      {==}    case 1n+p 1n+q:      absdiff(p, q)def diff_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +acc: Nat, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, n, ys) == True{} : Bool}) -> {Nat.is_eq(L.diff(xs, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), LV.ev(ys))) : Bool}:  match n xs ys:    case 0n Nil{} Nil{}:      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))    case 0n Nil{} y <> yt:      Empty.absurd({Nat.is_eq(L.diff([], y <> yt, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev([]), LV.ev(y <> yt))) : Bool}, Lg.false_true(hy))    case 0n x <> xt _:      Empty.absurd({Nat.is_eq(L.diff(x <> xt, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(x <> xt), LV.ev(ys))) : Bool}, Lg.false_true(hx))    case 1n+k Nil{} _:      Empty.absurd({Nat.is_eq(L.diff([], ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev([]), LV.ev(ys))) : Bool}, Lg.false_true(hx))    case 1n+k x <> xt Nil{}:      Empty.absurd({Nat.is_eq(L.diff(x <> xt, [], acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(x <> xt), LV.ev([]))) : Bool}, Lg.false_true(hy))    case 1n+ +k +x <> +xt +y <> +yt:      +hx0 = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx)      +hy0 = Lg.and_left(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)      +hxt = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx)      +hyt = Lg.and_right(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)      %Equal.sym(Bool, Nat.is_eq(L.diff(xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))), 0n), Bool.and(Nat.is_eq(Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), 0n), Nat.is_eq(LV.ev(xt), LV.ev(yt))), diff_v(one, h1, k, xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), hxt, hyt)) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n)), is_eq_add0(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))) : {Bool.and(_, Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}      %Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n), Nat.is_eq(x, y), absdiff(x, y)) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), _), Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt)))), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt))), eq_digit(one, h1, x, y, LV.ev(xt), LV.ev(yt), hx0, hy0)) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, y)), Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, y)), Nat.is_eq(LV.ev(xt), LV.ev(yt))), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))) : Bool}      {==}def eq_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, 16n, ys) == True{} : Bool}) -> {L.eq(xs, ys) == Nat.is_eq(LV.ev(xs), LV.ev(ys)) : Bool}:  diff_v(one, h1, 16n, xs, ys, 0n, hx, hy)# ---- x < m through the carry out of x + c ----def hz(+lo: Nat, hi: Nat, +t: Nat, +hl: {Nat.is_lt(lo, t) == True{} : Bool}) -> {Nat.is_eq(hi, 0n) == Nat.is_lt(Nat.add(lo, Nat.mul(hi, t)), t) : Bool}:  match hi:    case 0n:      %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {True{} == Nat.is_lt(_, t) : Bool}      Equal.sym(Bool, Nat.is_lt(lo, t), True{}, hl)    case 1n+ +k:      Equal.sym(Bool, Nat.is_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t), False{}, N.le_not_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t, N.le_trans(t, Nat.add(t, Nat.mul(k, t)), Nat.add(lo, Nat.add(t, Nat.mul(k, t))), N.le_add_right(t, Nat.mul(k, t)), I.le_add_l(lo, Nat.add(t, Nat.mul(k, t))))))def ltm_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}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:  +u = L.carry(32n, L.add(x, c), 0n)  +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(x, 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))  %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_eq(_, 0n) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}  %Equal.sym(Bool, Nat.is_eq(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), 0n), Nat.is_lt(Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), C.shift(256n, one)), hz(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one), ll)) : {_ == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}  %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), LV.ev(L.carry(32n, L.add(x, c), 0n)), Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), R.split256(one, h1, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(x), LV.ev(c)), R.u_val(c, x)) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}  %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.is_lt(Nat.add(LV.ev(x), LV.ev(c)), _) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}  WW.lt_cancel_r(LV.ev(x), 1n+mp, LV.ev(c))def ltm_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}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:  ltm_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), x)# ---- small constants: norm16([k]) for k < 2^16 ----def small_ev(+k: Nat) -> {LV.ev([k]) == k : Nat}:  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(k, _) == k : Nat}  %Equal.sym(Nat, Nat.add(k, 0n), k, NA.add_zero(k)) : {_ == k : Nat}  {==}def small_v(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.norm16([k])) == k : Nat}:  +x = L.carry(32n, [k], 0n)  +ex = Equal.trans(Nat, LV.ev(x), LV.ev([k]), k, LV.carry_v(32n, [k], 0n), small_ev(k))  %Equal.sym(Nat, LV.ev(L.take(16n, L.carry(32n, [k], 0n))), LV.ev(L.carry(32n, [k], 0n)), R.take_small(one, h1, L.carry(32n, [k], 0n), I.lt_subst_l(k, LV.ev(x), C.shift(256n, one), Equal.sym(Nat, LV.ev(x), k, ex), hk))) : {_ == k : Nat}  %Equal.sym(Nat, LV.ev(L.carry(32n, [k], 0n)), k, ex) : {_ == k : Nat}  {==}def small_l(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {FS.limbs16(one, 16n, L.norm16([k])) == True{} : Bool}:  B.carry_limbs(one, h1, 32n, 16n, [k], 0n, {==})