def fin_val

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
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

97def fin_val(+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}) -> {FS.value(F.add0(a, U32.mul(38, c))) == Nat.add(FS.value(a), Nat.mul(38n, v(c))) : Nat}:
98  match a:
99    case Nil{}:
100      Empty.absurd({0n == Nat.add(0n, Nat.mul(38n, v(c))) : Nat}, L.false_true(ha))
101    case Con{+x, +xt}:
102      +em = m38_v(one, h1, c, hc)
103      +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), head_le(one, h1, v(x), v(c), LM.okb_head(m, x, xt, 255n, ha), hc)), LM.sc_lt(3n, 28n, one, h1))
104      Equal.trans(Nat, FS.value(F.add0(Con{x, xt}, U32.mul(38, c))), Nat.add(FS.value(Con{x, xt}), v(U32.mul(38, c))), Nat.add(FS.value(Con{x, xt}), Nat.mul(38n, v(c))), add0_val(one, h1, x, xt, U32.mul(38, c), hb), M.cong_r(FS.value(Con{x, xt}), v(U32.mul(38, c)), Nat.mul(38n, v(c)), em))