def bytes_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:210

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/spec/crypto/curve25519/x25519.bend as S
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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
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

210# n tight bytes are the little-endian encoding of their value
211def bytes_le(+n: Nat, +ys: List<&2, U32>, +e: {LM.okb(n, ys, 255n) == True{} : Bool}) -> {S.le_bytes(n, FS.value(ys)) == ys : List<&2, U32>}:
212  match n ys:
213    case 0n Nil{}:
214      {==}
215    case 0n Con{y, yt}:
216      Empty.absurd({Nil{} == Con{y, yt} : List<&2, U32>}, L.false_true(e))
217    case 1n+m Nil{}:
218      Empty.absurd({S.le_bytes(1n+m, 0n) == Nil{} : List<&2, U32>}, L.false_true(e))
219    case 1n+ +m Con{+y, +yt}:
220      +V = FS.value(yt)
221      +hy = LM.okb_head(m, y, yt, 255n, e)
222      +hl = N.le_lt_succ(v(y), 255n, hy)
223      +x = Nat.add(v(y), C.shift(8n, V))
224      +ex = Equal.trans(Nat, x, Nat.add(C.shift(8n, V), v(y)), Nat.add(Nat.mul(V, 256n), v(y)), NA.add_comm(v(y), C.shift(8n, V)), M.cong_l(C.shift(8n, V), Nat.mul(V, 256n), v(y), Equal.sym(Nat, Nat.mul(V, 256n), C.shift(8n, V), LM.m256(V))))
225      +em = Equal.trans(Nat, Nat.mod(x, 256n), Nat.mod(Nat.add(Nat.mul(V, 256n), v(y)), 256n), v(y), M.cong_mod(256n, x, Nat.add(Nat.mul(V, 256n), v(y)), ex), NR.mod_of(V, 255n, v(y), hl))
226      +ed = Equal.trans(Nat, Nat.div(x, 256n), Nat.div(Nat.add(Nat.mul(V, 256n), v(y)), 256n), V, Equal.cong(Nat, Nat, z => Nat.div(z, 256n), x, Nat.add(Nat.mul(V, 256n), v(y)), ex), NR.div_of(V, 255n, v(y), hl))
227      +e1 = Equal.trans(U32, U32.from_nat(Nat.mod(x, 256n)), U32.from_nat(v(y)), y, Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.mod(x, 256n), v(y), em), byte_rt(y, hy))
228      +e2 = Equal.trans(List<&2, U32>, S.le_bytes(m, Nat.div(x, 256n)), S.le_bytes(m, V), yt, Equal.cong(Nat, List<&2, U32>, z => S.le_bytes(m, z), Nat.div(x, 256n), V, ed), bytes_le(m, yt, LM.okb_tail(m, y, yt, 255n, e)))
229      Equal.trans(List<&2, U32>, Con{U32.from_nat(Nat.mod(x, 256n)), S.le_bytes(m, Nat.div(x, 256n))}, Con{y, S.le_bytes(m, Nat.div(x, 256n))}, Con{y, yt}, Equal.cong(U32, List<&2, U32>, z => Con{z, S.le_bytes(m, Nat.div(x, 256n))}, U32.from_nat(Nat.mod(x, 256n)), y, e1), Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{y, z}, S.le_bytes(m, Nat.div(x, 256n)), yt, e2))