def byte_fits

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar2.bend:55

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/src/crypto/curve25519/x25519.bend as X
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/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

55# a byte string's value fits its bit count
56def byte_fits(+bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {C.high(X.bitlen(bs), FS.value(bs)) == 0n : Nat}:
57  match bs:
58    case Nil{}:
59      {==}
60    case Con{+b, +bt}:
61      +V = FS.value(bt)
62      +hbl = N.le_lt_succ(v(b), 255n, LM.lea_head(b, bt, 255n, hb))
63      +e1 = WI.high_comp(X.bitlen(bt), 8n, Nat.add(v(b), C.shift(8n, V)))
64      +e2 = Equal.cong(Nat, Nat, z => C.high(X.bitlen(bt), z), C.high(8n, Nat.add(v(b), C.shift(8n, V))), V, WI.high_uniq(8n, v(b), V, hbl))
65      Equal.trans(Nat, C.high(Nat.add(8n, X.bitlen(bt)), Nat.add(v(b), C.shift(8n, V))), C.high(X.bitlen(bt), V), 0n, Equal.trans(Nat, C.high(Nat.add(8n, X.bitlen(bt)), Nat.add(v(b), C.shift(8n, V))), C.high(X.bitlen(bt), C.high(8n, Nat.add(v(b), C.shift(8n, V)))), C.high(X.bitlen(bt), V), e1, e2), byte_fits(bt, LM.lea_tail(b, bt, 255n, hb)))