def fin_okb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fold.bend:106

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL

106def fin_okb(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat, +a: List<&2, U32>, +c: U32, +ha: {LM.okb(1n+m, a, 255n) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {LM.okb(1n+m, F.add0(a, U32.mul(38, c)), WD.sc(28n, one)) == True{} : Bool}:
107  match a:
108    case Nil{}:
109      Empty.absurd({LM.okb(1n+m, Nil{}, WD.sc(28n, one)) == True{} : Bool}, L.false_true(ha))
110    case Con{+x, +xt}:
111      +em = m38_v(one, h1, c, hc)
112      +hh = head_le(one, h1, v(x), v(c), LM.okb_head(m, x, xt, 255n, ha), hc)
113      +hb = N.le_lt_trans(Nat.add(v(x), v(U32.mul(38, c))), WD.sc(28n, one), WD.sc(32n, one), L.subst(Nat, z => {Nat.is_le(Nat.add(v(x), z), WD.sc(28n, one)) == True{} : Bool}, Nat.mul(38n, v(c)), v(U32.mul(38, c)), Equal.sym(Nat, v(U32.mul(38, c)), Nat.mul(38n, v(c)), em), hh), LM.sc_lt(3n, 28n, one, h1))
114      +ev = LM.add_v(one, h1, x, U32.mul(38, c), hb)
115      +hd = L.subst(Nat, z => {Nat.is_le(z, WD.sc(28n, one)) == True{} : Bool}, Nat.add(v(x), Nat.mul(38n, v(c))), v(U32.add(x, U32.mul(38, c))), Equal.trans(Nat, Nat.add(v(x), Nat.mul(38n, v(c))), Nat.add(v(x), v(U32.mul(38, c))), v(U32.add(x, U32.mul(38, c))), M.cong_r(v(x), Nat.mul(38n, v(c)), v(U32.mul(38, c)), Equal.sym(Nat, v(U32.mul(38, c)), Nat.mul(38n, v(c)), em)), Equal.sym(Nat, v(U32.add(x, U32.mul(38, c))), Nat.add(v(x), v(U32.mul(38, c))), ev)), hh)
116      L.and_intro(Nat.is_le(v(U32.add(x, U32.mul(38, c))), WD.sc(28n, one)), LM.okb(m, xt, WD.sc(28n, one)), hd, PL.okb_mono(m, xt, 255n, WD.sc(28n, one), le255(one, h1, 20n), LM.okb_tail(m, x, xt, 255n, ha)))