def valo_digits

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/adc.bend:92

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/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/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K

92def valo_digits(+one: Nat, +xs: List<&2, U32>, +ds: List<&2, Nat>, +h: {digs_eq(xs, ds) == True{} : Bool}) -> {K.valo(one, xs) == FS.digits(one, ds) : Nat}:
93  match xs ds:
94    case Nil{} Nil{}:
95      {==}
96    case Con{+x, +xt} Con{+d, +dt}:
97      +e1 = N.eq_from_is_eq(v(x), d, L.and_left(Nat.is_eq(v(x), d), digs_eq(xt, dt), h))
98      +e2 = valo_digits(one, xt, dt, L.and_right(Nat.is_eq(v(x), d), digs_eq(xt, dt), h))
99      M.cong_add(Nat.mul(one, v(x)), Nat.mul(one, d), C.shift(8n, K.valo(one, xt)), C.shift(8n, FS.digits(one, dt)), Equal.cong(Nat, Nat, z => Nat.mul(one, z), v(x), d, e1), M.cong_sc(8n, K.valo(one, xt), FS.digits(one, dt), e2))
100    case Nil{} Con{d, dt}:
101      Empty.absurd({0n == FS.digits(one, Con{d, dt}) : Nat}, L.false_true(h))
102    case Con{x, xt} Nil{}:
103      Empty.absurd({K.valo(one, Con{x, xt}) == 0n : Nat}, L.false_true(h))