def valo_value

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/consts.bend:31

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

31def valo_value(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>) -> {valo(one, xs) == FS.value(xs) : Nat}:
32  match xs:
33    case Nil{}:
34      {==}
35    case Con{+h, +t}:
36      +e0 = L.subst(Nat, o => {Nat.mul(o, v(h)) == v(h) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), AR.one_mul(v(h)))
37      M.cong_add(Nat.mul(one, v(h)), v(h), C.shift(8n, valo(one, t)), C.shift(8n, FS.value(t)), e0, M.cong_sc(8n, valo(one, t), FS.value(t), valo_value(one, h1, t)))