def kbit_val

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

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/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

48# X.kbit(bs, t) is bit t of the value of the bytes
49def kbit_val(+bs: List<&2, U32>, +t: Nat, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {v(X.kbit(bs, t)) == S.kbit(FS.value(bs), t) : Nat}:
50  match bs t:
51    case Nil{} _:
52      Equal.cong(Nat, Nat, z => C.bit(z), 0n, C.high(t, 0n), Equal.sym(Nat, C.high(t, 0n), 0n, high_zero(t)))
53    case Con{+b, +bt} 0n:
54      low_bit(0n, b, C.shift(7n, FS.value(bt)))
55    case Con{+b, +bt} 1n:
56      low_bit(1n, b, C.shift(6n, FS.value(bt)))
57    case Con{+b, +bt} 2n:
58      low_bit(2n, b, C.shift(5n, FS.value(bt)))
59    case Con{+b, +bt} 3n:
60      low_bit(3n, b, C.shift(4n, FS.value(bt)))
61    case Con{+b, +bt} 4n:
62      low_bit(4n, b, C.shift(3n, FS.value(bt)))
63    case Con{+b, +bt} 5n:
64      low_bit(5n, b, C.shift(2n, FS.value(bt)))
65    case Con{+b, +bt} 6n:
66      low_bit(6n, b, C.shift(1n, FS.value(bt)))
67    case Con{+b, +bt} 7n:
68      low_bit(7n, b, FS.value(bt))
69    case Con{+b, +bt} 8n+ +q:
70      +V = FS.value(bt)
71      +hbl = N.le_lt_succ(v(b), 255n, LM.lea_head(b, bt, 255n, hb))
72      +e1 = WI.high_comp(q, 8n, Nat.add(v(b), C.shift(8n, V)))
73      +e2 = Equal.cong(Nat, Nat, z => C.high(q, z), C.high(8n, Nat.add(v(b), C.shift(8n, V))), V, WI.high_uniq(8n, v(b), V, hbl))
74      +e3 = Equal.cong(Nat, Nat, z => C.bit(z), C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V))), C.high(q, V), Equal.trans(Nat, C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V))), C.high(q, C.high(8n, Nat.add(v(b), C.shift(8n, V)))), C.high(q, V), e1, e2))
75      Equal.trans(Nat, v(X.kbit(bt, q)), C.bit(C.high(q, V)), C.bit(C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V)))), kbit_val(bt, q, LM.lea_tail(b, bt, 255n, hb)), Equal.sym(Nat, C.bit(C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V)))), C.bit(C.high(q, V)), e3))