proofs/crypto/curve25519/poly.bend source

proofs/crypto/curve25519/poly.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/curve25519/field.bend as FSimport ../../../src/crypto/curve25519/field.bend as Fimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/word.bend as WDimport ../../lib/arith.bend as ARimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ./num.bend as Mimport ./limbs.bend as LM# The limb-list polynomial operations of src/crypto/curve25519/field.bend:# addl (limbwise sum), scal (times a limb), conv (the schoolbook product),# take/drop (the split at 2^256) and wide (the fold of the product's high# half). Each keeps its value exactly (Nat, no wrap) under limb bounds whose# sums and products stay below 2^32.def v(+x: U32) -> Nat:  U32.to_nat(x)# ---- lengths ----def len_le(n: Nat, xs: List<&2, U32>) -> Bool:  match n:    case 0n:      match xs:        case Nil{}:          True{}        case Con{x, xt}:          False{}    case 1n+m:      match xs:        case Nil{}:          True{}        case Con{x, xt}:          len_le(m, xt)def len_ge(n: Nat, xs: List<&2, U32>) -> Bool:  match n:    case 0n:      True{}    case 1n+m:      match xs:        case Nil{}:          False{}        case Con{x, xt}:          len_ge(m, xt)def len_le_nil(+n: Nat) -> {len_le(n, Nil{}) == True{} : Bool}:  match n:    case 0n:      {==}    case 1n+m:      {==}def len_le_mono(+k: Nat, +d: Nat, +xs: List<&2, U32>, +e: {len_le(k, xs) == True{} : Bool}) -> {len_le(Nat.add(k, d), xs) == True{} : Bool}:  match k xs:    case 0n Nil{}:      len_le_nil(d)    case 0n Con{y, yt}:      Empty.absurd({len_le(d, Con{y, yt}) == True{} : Bool}, L.false_true(e))    case 1n+m Nil{}:      {==}    case 1n+ +m Con{y, +yt}:      len_le_mono(m, d, yt, e)def okb_len_le(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {len_le(n, xs) == True{} : Bool}:  match n xs:    case 0n Nil{}:      {==}    case 0n Con{y, yt}:      Empty.absurd({len_le(0n, Con{y, yt}) == True{} : Bool}, L.false_true(e))    case 1n+m Nil{}:      {==}    case 1n+ +m Con{+y, +yt}:      okb_len_le(m, yt, b, LM.okb_tail(m, y, yt, b, e))def okb_len_ge(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {len_ge(n, xs) == True{} : Bool}:  match n xs:    case 0n Nil{}:      {==}    case 0n Con{y, yt}:      {==}    case 1n+m Nil{}:      Empty.absurd({len_ge(1n+m, Nil{}) == True{} : Bool}, L.false_true(e))    case 1n+ +m Con{+y, +yt}:      okb_len_ge(m, yt, b, LM.okb_tail(m, y, yt, b, e))def okb_mono(+n: Nat, +xs: List<&2, U32>, +b: Nat, +c: Nat, +hb: {Nat.is_le(b, c) == True{} : Bool}, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {LM.okb(n, xs, c) == True{} : Bool}:  match n xs:    case 0n Nil{}:      {==}    case 0n Con{y, yt}:      Empty.absurd({LM.okb(0n, Con{y, yt}, c) == True{} : Bool}, L.false_true(e))    case 1n+m Nil{}:      Empty.absurd({LM.okb(1n+m, Nil{}, c) == True{} : Bool}, L.false_true(e))    case 1n+ +m Con{+y, +yt}:      L.and_intro(Nat.is_le(v(y), c), LM.okb(m, yt, c), N.le_trans(v(y), b, c, LM.okb_head(m, y, yt, b, e), hb), okb_mono(m, yt, b, c, hb, LM.okb_tail(m, y, yt, b, e)))def le_add_l(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}:  %NA.add_comm(b, a) : {Nat.is_le(b, _) == True{} : Bool}  N.le_add_right(b, a)# ---- addl ----def addl_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {Nat.is_le(v(y), b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:  LM.add_v(one, h1, x, y, N.le_lt_trans(Nat.add(v(x), v(y)), Nat.add(a, b), WD.sc(32n, one), M.le_add2(v(x), v(y), a, b, hx, hy), hab))def addl_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.addl(xs, ys)) == Nat.add(FS.value(xs), FS.value(ys)) : Nat}:  match xs ys:    case Nil{} _:      {==}    case Con{+x, +xt} Nil{}:      Equal.sym(Nat, Nat.add(FS.value(Con{x, xt}), 0n), FS.value(Con{x, xt}), N.add_zero(FS.value(Con{x, xt})))    case Con{+x, +xt} Con{+y, +yt}:      +ev = addl_v(one, h1, x, y, a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy), hab)      +ih = addl_val(one, h1, xt, yt, a, b, LM.lea_tail(x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hab)      +X = FS.value(xt)      +Y = FS.value(yt)      +e1 = M.cong_add(v(U32.add(x, y)), Nat.add(v(x), v(y)), C.shift(8n, FS.value(F.addl(xt, yt))), C.shift(8n, Nat.add(X, Y)), ev, M.cong_sc(8n, FS.value(F.addl(xt, yt)), Nat.add(X, Y), ih))      +e2 = M.cong_r(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y)), Nat.add(C.shift(8n, X), C.shift(8n, Y)), Equal.sym(Nat, Nat.add(C.shift(8n, X), C.shift(8n, Y)), C.shift(8n, Nat.add(X, Y)), M.sc_add(8n, X, Y)))      Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(8n, FS.value(F.addl(xt, yt)))), Nat.add(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(y), C.shift(8n, Y))), e1,        Equal.trans(Nat, Nat.add(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(v(x), v(y)), Nat.add(C.shift(8n, X), C.shift(8n, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(y), C.shift(8n, Y))), e2, M.add4(v(x), v(y), C.shift(8n, X), C.shift(8n, Y))))def addl_lea(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.addl(xs, ys), Nat.add(a, b)) == True{} : Bool}:  match xs ys:    case Nil{} _:      LM.lea_mono(ys, b, Nat.add(a, b), le_add_l(a, b), hy)    case Con{+x, +xt} Nil{}:      LM.lea_mono(Con{x, xt}, a, Nat.add(a, b), N.le_add_right(a, b), hx)    case Con{+x, +xt} Con{+y, +yt}:      +ev = addl_v(one, h1, x, y, a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy), hab)      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.add(a, b)) == True{} : Bool}, Nat.add(v(x), v(y)), v(U32.add(x, y)), Equal.sym(Nat, v(U32.add(x, y)), Nat.add(v(x), v(y)), ev), M.le_add2(v(x), v(y), a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy)))      L.and_intro(Nat.is_le(v(U32.add(x, y)), Nat.add(a, b)), LM.lea(F.addl(xt, yt), Nat.add(a, b)), hd, addl_lea(one, h1, xt, yt, a, b, LM.lea_tail(x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hab))# n limbs and at most n limbs give n limbsdef addl_okb(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.okb(n, xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hl: {len_le(n, ys) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.okb(n, F.addl(xs, ys), Nat.add(a, b)) == True{} : Bool}:  match n xs ys:    case 0n Nil{} Nil{}:      {==}    case 0n Nil{} Con{y, yt}:      Empty.absurd({LM.okb(0n, Con{y, yt}, Nat.add(a, b)) == True{} : Bool}, L.false_true(hl))    case 0n Con{x, xt} _:      Empty.absurd({LM.okb(0n, F.addl(Con{x, xt}, ys), Nat.add(a, b)) == True{} : Bool}, L.false_true(hx))    case 1n+m Nil{} _:      Empty.absurd({LM.okb(1n+m, ys, Nat.add(a, b)) == True{} : Bool}, L.false_true(hx))    case 1n+ +m Con{+x, +xt} Nil{}:      okb_mono(1n+m, Con{x, xt}, a, Nat.add(a, b), N.le_add_right(a, b), hx)    case 1n+ +m Con{+x, +xt} Con{+y, +yt}:      +hxh = LM.okb_head(m, x, xt, a, hx)      +hyh = LM.lea_head(y, yt, b, hy)      +ev = addl_v(one, h1, x, y, a, b, hxh, hyh, hab)      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.add(a, b)) == True{} : Bool}, Nat.add(v(x), v(y)), v(U32.add(x, y)), Equal.sym(Nat, v(U32.add(x, y)), Nat.add(v(x), v(y)), ev), M.le_add2(v(x), v(y), a, b, hxh, hyh))      L.and_intro(Nat.is_le(v(U32.add(x, y)), Nat.add(a, b)), LM.okb(m, F.addl(xt, yt), Nat.add(a, b)), hd, addl_okb(one, h1, m, xt, yt, a, b, LM.okb_tail(m, x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hl, hab))def addl_len_ge(+n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +e: {len_ge(n, xs) == True{} : Bool}) -> {len_ge(n, F.addl(xs, ys)) == True{} : Bool}:  match n xs ys:    case 0n _ _:      {==}    case 1n+m Nil{} _:      Empty.absurd({len_ge(1n+m, ys) == True{} : Bool}, L.false_true(e))    case 1n+m Con{x, xt} Nil{}:      e    case 1n+ +m Con{x, +xt} Con{y, +yt}:      addl_len_ge(m, xt, yt, e)def addl_len_le(+n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +ex: {len_le(n, xs) == True{} : Bool}, +ey: {len_le(n, ys) == True{} : Bool}) -> {len_le(n, F.addl(xs, ys)) == True{} : Bool}:  match n xs ys:    case 0n Nil{} _:      ey    case 0n Con{x, xt} _:      Empty.absurd({len_le(0n, F.addl(Con{x, xt}, ys)) == True{} : Bool}, L.false_true(ex))    case 1n+m Nil{} _:      ey    case 1n+m Con{x, xt} Nil{}:      ex    case 1n+ +m Con{x, +xt} Con{y, +yt}:      addl_len_le(m, xt, yt, ex, ey)# ---- scal ----def sc_mul_l(+k: Nat, +a: Nat, +x: Nat) -> {WD.sc(k, Nat.mul(a, x)) == Nat.mul(a, WD.sc(k, x)) : Nat}:  +e1 = M.cong_sc(k, Nat.mul(a, x), Nat.mul(x, a), NA.mul_comm(a, x))  +e2 = AR.sc_mul(k, x, a)  +e3 = NA.mul_comm(WD.sc(k, x), a)  Equal.trans(Nat, WD.sc(k, Nat.mul(a, x)), WD.sc(k, Nat.mul(x, a)), Nat.mul(a, WD.sc(k, x)), e1, Equal.trans(Nat, WD.sc(k, Nat.mul(x, a)), Nat.mul(WD.sc(k, x), a), Nat.mul(a, WD.sc(k, x)), e2, e3))def scal_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {Nat.is_le(v(y), b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}:  LM.mul_v(one, h1, x, y, N.le_lt_trans(Nat.mul(v(x), v(y)), Nat.mul(a, b), WD.sc(32n, one), M.le_mul2(v(x), v(y), a, b, hx, hy), hab))def scal_val(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.scal(x, ys)) == Nat.mul(v(x), FS.value(ys)) : Nat}:  match ys:    case Nil{}:      Equal.sym(Nat, Nat.mul(v(x), 0n), 0n, NA.mul_zero(v(x)))    case Con{+y, +yt}:      +ev = scal_v(one, h1, x, y, a, b, hx, LM.lea_head(y, yt, b, hy), hab)      +ih = scal_val(one, h1, x, yt, a, b, hx, LM.lea_tail(y, yt, b, hy), hab)      +Y = FS.value(yt)      +e1 = M.cong_add(v(U32.mul(x, y)), Nat.mul(v(x), v(y)), C.shift(8n, FS.value(F.scal(x, yt))), C.shift(8n, Nat.mul(v(x), Y)), ev, M.cong_sc(8n, FS.value(F.scal(x, yt)), Nat.mul(v(x), Y), ih))      +e2 = M.cong_r(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y)), Nat.mul(v(x), C.shift(8n, Y)), sc_mul_l(8n, v(x), Y))      +e3 = Equal.sym(Nat, Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), Nat.add(Nat.mul(v(x), v(y)), Nat.mul(v(x), C.shift(8n, Y))), NA.mul_add_left(v(x), v(y), C.shift(8n, Y)))      Equal.trans(Nat, Nat.add(v(U32.mul(x, y)), C.shift(8n, FS.value(F.scal(x, yt)))), Nat.add(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y))), Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), e1,        Equal.trans(Nat, Nat.add(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y))), Nat.add(Nat.mul(v(x), v(y)), Nat.mul(v(x), C.shift(8n, Y))), Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), e2, e3))def scal_lea(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}:  match ys:    case Nil{}:      {==}    case Con{+y, +yt}:      +hyh = LM.lea_head(y, yt, b, hy)      +ev = scal_v(one, h1, x, y, a, b, hx, hyh, hab)      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(v(x), v(y)), v(U32.mul(x, y)), Equal.sym(Nat, v(U32.mul(x, y)), Nat.mul(v(x), v(y)), ev), M.le_mul2(v(x), v(y), a, b, hx, hyh))      L.and_intro(Nat.is_le(v(U32.mul(x, y)), Nat.mul(a, b)), LM.lea(F.scal(x, yt), Nat.mul(a, b)), hd, scal_lea(one, h1, x, yt, a, b, hx, LM.lea_tail(y, yt, b, hy), hab))def scal_okb(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.okb(n, ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.okb(n, F.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}:  match n ys:    case 0n Nil{}:      {==}    case 0n Con{y, yt}:      Empty.absurd({LM.okb(0n, F.scal(x, Con{y, yt}), Nat.mul(a, b)) == True{} : Bool}, L.false_true(hy))    case 1n+m Nil{}:      Empty.absurd({LM.okb(1n+m, Nil{}, Nat.mul(a, b)) == True{} : Bool}, L.false_true(hy))    case 1n+ +m Con{+y, +yt}:      +hyh = LM.okb_head(m, y, yt, b, hy)      +ev = scal_v(one, h1, x, y, a, b, hx, hyh, hab)      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(v(x), v(y)), v(U32.mul(x, y)), Equal.sym(Nat, v(U32.mul(x, y)), Nat.mul(v(x), v(y)), ev), M.le_mul2(v(x), v(y), a, b, hx, hyh))      L.and_intro(Nat.is_le(v(U32.mul(x, y)), Nat.mul(a, b)), LM.okb(m, F.scal(x, yt), Nat.mul(a, b)), hd, scal_okb(one, h1, m, x, yt, a, b, hx, LM.okb_tail(m, y, yt, b, hy), hab))def scal_len_ge(+n: Nat, +x: U32, +ys: List<&2, U32>, +e: {len_ge(n, ys) == True{} : Bool}) -> {len_ge(n, F.scal(x, ys)) == True{} : Bool}:  match n ys:    case 0n _:      {==}    case 1n+m Nil{}:      Empty.absurd({len_ge(1n+m, Nil{}) == True{} : Bool}, L.false_true(e))    case 1n+ +m Con{y, +yt}:      scal_len_ge(m, x, yt, e)def scal_len_le(+n: Nat, +x: U32, +ys: List<&2, U32>, +e: {len_le(n, ys) == True{} : Bool}) -> {len_le(n, F.scal(x, ys)) == True{} : Bool}:  match n ys:    case 0n Nil{}:      {==}    case 0n Con{y, yt}:      Empty.absurd({len_le(0n, F.scal(x, Con{y, yt})) == True{} : Bool}, L.false_true(e))    case 1n+m Nil{}:      {==}    case 1n+ +m Con{y, +yt}:      scal_len_le(m, x, yt, e)# ---- conv ----# len(xs) * kdef cb(xs: List<&2, U32>, +k: Nat) -> Nat:  match xs:    case Nil{}:      0n    case Con{x, xt}:      Nat.add(k, cb(xt, k))def cbn(n: Nat, +k: Nat) -> Nat:  match n:    case 0n:      0n    case 1n+m:      Nat.add(k, cbn(m, k))def conv_lea(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hc: {Nat.is_lt(cb(xs, Nat.mul(a, b)), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.conv(xs, ys), cb(xs, Nat.mul(a, b))) == True{} : Bool}:  match xs:    case Nil{}:      {==}    case Con{+x, +xt}:      +ab = Nat.mul(a, b)      +k = cb(xt, ab)      +hab = N.le_lt_trans(ab, Nat.add(ab, k), WD.sc(32n, one), N.le_add_right(ab, k), hc)      +hk = N.le_lt_trans(k, Nat.add(ab, k), WD.sc(32n, one), le_add_l(ab, k), hc)      +hs = scal_lea(one, h1, x, ys, a, b, LM.lea_head(x, xt, a, hx), hy, hab)      +hz = L.and_intro(Nat.is_le(0n, k), LM.lea(F.conv(xt, ys), k), N.zero_le(k), conv_lea(one, h1, xt, ys, a, b, LM.lea_tail(x, xt, a, hx), hy, hk))      addl_lea(one, h1, F.scal(x, ys), Con{0, F.conv(xt, ys)}, ab, k, hs, hz, hc)def conv_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hc: {Nat.is_lt(cb(xs, Nat.mul(a, b)), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.conv(xs, ys)) == Nat.mul(FS.value(xs), FS.value(ys)) : Nat}:  match xs:    case Nil{}:      {==}    case Con{+x, +xt}:      +ab = Nat.mul(a, b)      +k = cb(xt, ab)      +Y = FS.value(ys)      +X = FS.value(xt)      +hab = N.le_lt_trans(ab, Nat.add(ab, k), WD.sc(32n, one), N.le_add_right(ab, k), hc)      +hk = N.le_lt_trans(k, Nat.add(ab, k), WD.sc(32n, one), le_add_l(ab, k), hc)      +hxh = LM.lea_head(x, xt, a, hx)      +hxt = LM.lea_tail(x, xt, a, hx)      +hs = scal_lea(one, h1, x, ys, a, b, hxh, hy, hab)      +hz = L.and_intro(Nat.is_le(0n, k), LM.lea(F.conv(xt, ys), k), N.zero_le(k), conv_lea(one, h1, xt, ys, a, b, hxt, hy, hk))      +e1 = addl_val(one, h1, F.scal(x, ys), Con{0, F.conv(xt, ys)}, ab, k, hs, hz, hc)      +e2 = M.cong_add(FS.value(F.scal(x, ys)), Nat.mul(v(x), Y), FS.value(Con{0, F.conv(xt, ys)}), C.shift(8n, Nat.mul(X, Y)), scal_val(one, h1, x, ys, a, b, hxh, hy, hab), M.cong_sc(8n, FS.value(F.conv(xt, ys)), Nat.mul(X, Y), conv_val(one, h1, xt, ys, a, b, hxt, hy, hk)))      +e3 = M.cong_r(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y)), Nat.mul(C.shift(8n, X), Y), AR.sc_mul(8n, X, Y))      +e4 = Equal.sym(Nat, Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), Nat.add(Nat.mul(v(x), Y), Nat.mul(C.shift(8n, X), Y)), NA.mul_add_right(v(x), C.shift(8n, X), Y))      Equal.trans(Nat, FS.value(F.conv(Con{x, xt}, ys)), Nat.add(FS.value(F.scal(x, ys)), FS.value(Con{0, F.conv(xt, ys)})), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e1,        Equal.trans(Nat, Nat.add(FS.value(F.scal(x, ys)), FS.value(Con{0, F.conv(xt, ys)})), Nat.add(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y))), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e2,          Equal.trans(Nat, Nat.add(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y))), Nat.add(Nat.mul(v(x), Y), Nat.mul(C.shift(8n, X), Y)), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e3, e4)))def conv_len_ge(+n: Nat, +x: U32, +xt: List<&2, U32>, +ys: List<&2, U32>, +e: {len_ge(n, ys) == True{} : Bool}) -> {len_ge(n, F.conv(Con{x, xt}, ys)) == True{} : Bool}:  addl_len_ge(n, F.scal(x, ys), Con{0, F.conv(xt, ys)}, scal_len_ge(n, x, ys, e))# len(conv(xs, ys)) <= j + k when len(xs) <= j and len(ys) <= kdef conv_len_le(+j: Nat, +k: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +ex: {len_le(j, xs) == True{} : Bool}, +ey: {len_le(k, ys) == True{} : Bool}) -> {len_le(Nat.add(j, k), F.conv(xs, ys)) == True{} : Bool}:  match j xs:    case 0n Nil{}:      len_le_nil(k)    case 0n Con{x, xt}:      Empty.absurd({len_le(k, F.conv(Con{x, xt}, ys)) == True{} : Bool}, L.false_true(ex))    case 1n+m Nil{}:      {==}    case 1n+ +m Con{+x, +xt}:      +hs0 = len_le_mono(k, 1n+m, F.scal(x, ys), scal_len_le(k, x, ys, ey))      +hs = L.subst(Nat, z => {len_le(z, F.scal(x, ys)) == True{} : Bool}, Nat.add(k, 1n+m), Nat.add(1n+m, k), NA.add_comm(k, 1n+m), hs0)      +hz = conv_len_le(m, k, xt, ys, ex, ey)      addl_len_le(Nat.add(1n+m, k), F.scal(x, ys), Con{0, F.conv(xt, ys)}, hs, hz)# ---- take and drop ----def take_drop_val(+n: Nat, +xs: List<&2, U32>) -> {FS.value(xs) == Nat.add(FS.value(F.take(n, xs)), LM.sh(F.take(n, xs), FS.value(F.drop(n, xs)))) : Nat}:  match n xs:    case 0n _:      {==}    case 1n+m Nil{}:      {==}    case 1n+ +m Con{+x, +xt}:      +T = FS.value(F.take(m, xt))      +D = LM.sh(F.take(m, xt), FS.value(F.drop(m, xt)))      +ih = take_drop_val(m, xt)      +e1 = M.cong_r(v(x), C.shift(8n, FS.value(xt)), C.shift(8n, Nat.add(T, D)), M.cong_sc(8n, FS.value(xt), Nat.add(T, D), ih))      +e2 = M.cong_r(v(x), C.shift(8n, Nat.add(T, D)), Nat.add(C.shift(8n, T), C.shift(8n, D)), Equal.sym(Nat, Nat.add(C.shift(8n, T), C.shift(8n, D)), C.shift(8n, Nat.add(T, D)), M.sc_add(8n, T, D)))      +e3 = Equal.sym(Nat, Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), Nat.add(v(x), Nat.add(C.shift(8n, T), C.shift(8n, D))), NA.add_assoc(v(x), C.shift(8n, T), C.shift(8n, D)))      Equal.trans(Nat, Nat.add(v(x), C.shift(8n, FS.value(xt))), Nat.add(v(x), C.shift(8n, Nat.add(T, D))), Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), e1,        Equal.trans(Nat, Nat.add(v(x), C.shift(8n, Nat.add(T, D))), Nat.add(v(x), Nat.add(C.shift(8n, T), C.shift(8n, D))), Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), e2, e3))def take_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +hl: {len_ge(n, xs) == True{} : Bool}, +hx: {LM.lea(xs, b) == True{} : Bool}) -> {LM.okb(n, F.take(n, xs), b) == True{} : Bool}:  match n xs:    case 0n _:      {==}    case 1n+m Nil{}:      Empty.absurd({LM.okb(1n+m, Nil{}, b) == True{} : Bool}, L.false_true(hl))    case 1n+ +m Con{+x, +xt}:      L.and_intro(Nat.is_le(v(x), b), LM.okb(m, F.take(m, xt), b), LM.lea_head(x, xt, b, hx), take_okb(m, xt, b, hl, LM.lea_tail(x, xt, b, hx)))def drop_lea(+n: Nat, +xs: List<&2, U32>, +b: Nat, +hx: {LM.lea(xs, b) == True{} : Bool}) -> {LM.lea(F.drop(n, xs), b) == True{} : Bool}:  match n xs:    case 0n _:      hx    case 1n+m Nil{}:      {==}    case 1n+ +m Con{+x, +xt}:      drop_lea(m, xt, b, LM.lea_tail(x, xt, b, hx))def drop_len_le(+n: Nat, +k: Nat, +xs: List<&2, U32>, +hl: {len_le(Nat.add(n, k), xs) == True{} : Bool}) -> {len_le(k, F.drop(n, xs)) == True{} : Bool}:  match n xs:    case 0n _:      hl    case 1n+m Nil{}:      len_le_nil(k)    case 1n+ +m Con{x, +xt}:      drop_len_le(m, k, xt, hl)