proofs/crypto/curve25519/xbits.bend

bend-collections-laws-crypto@1.0.0.0 · 255 lines · 22 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as SN
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
15import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
16import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
17import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as SR
18import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as HH
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as CN
22
23# The byte-level pieces of X25519 (src/crypto/curve25519/x25519.bend against
24# spec/crypto/curve25519/x25519.bend): scalar bits, clamping, the bit
25# count, the swap bit, and the 32-byte encoding.
26
27def v(+x: U32) -> Nat:
28  U32.to_nat(x)
29
30# ---- bits of the scalar ----
31
32def high_zero(+t: Nat) -> {C.high(t, 0n) == 0n : Nat}:
33  match t:
34    case 0n:
35      {==}
36    case 1n+ +q:
37      high_zero(q)
38
39# bit t (t < 8) of b + 2^8 V is bit t of b
40def low_bit(+t: Nat, +b: U32, +w: Nat) -> {v(U32.and(U32.shrn(b, t), 1)) == C.bit(C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w))))) : Nat}:
41  +e1 = CN.and1(1n, {==}, U32.shrn(b, t))
42  +e2 = Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), v(U32.shrn(b, t)), C.high(t, v(b)), SR.shrn_high(b, t))
43  +e3 = Equal.sym(Nat, C.bit(C.high(t, v(b))), Nat.mod(C.high(t, v(b)), 2n), WI.bit_mod(C.high(t, v(b))))
44  +e4 = Equal.cong(Nat, Nat, z => C.bit(z), C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w)))), Nat.add(C.high(t, v(b)), Nat.double(w)), WI.high_add_shift(t, v(b), Nat.double(w)))
45  +e5 = WI.bit_dbl(C.high(t, v(b)), w)
46  Equal.trans(Nat, v(U32.and(U32.shrn(b, t), 1)), Nat.mod(v(U32.shrn(b, t)), 2n), C.bit(C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w))))), e1, Equal.trans(Nat, Nat.mod(v(U32.shrn(b, t)), 2n), Nat.mod(C.high(t, v(b)), 2n), C.bit(C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w))))), e2, Equal.trans(Nat, Nat.mod(C.high(t, v(b)), 2n), C.bit(C.high(t, v(b))), C.bit(C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w))))), e3, Equal.sym(Nat, C.bit(C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w))))), C.bit(C.high(t, v(b))), Equal.trans(Nat, C.bit(C.high(t, Nat.add(v(b), C.shift(t, Nat.double(w))))), C.bit(Nat.add(C.high(t, v(b)), Nat.double(w))), C.bit(C.high(t, v(b))), e4, e5)))))
47
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))
76
77def kbit_le(+bs: List<&2, U32>, +t: Nat, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {Nat.is_le(S.kbit(FS.value(bs), t), 1n) == True{} : Bool}:
78  WI.bit_le1(C.high(t, FS.value(bs)))
79
80# ---- clamping, the bit count ----
81
82def clamp_top_eq(+xs: List<&2, U32>) -> {X.clamp_top(xs) == S.clamp_last(xs) : List<&2, U32>}:
83  match xs:
84    case Nil{}:
85      {==}
86    case Con{+x, +xt}:
87      match xt:
88        case Nil{}:
89          {==}
90        case Con{+y, +yt}:
91          Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, X.clamp_top(Con{y, yt}), S.clamp_last(Con{y, yt}), clamp_top_eq(Con{y, yt}))
92
93def clamp_eq(+bs: List<&2, U32>) -> {X.clamp(bs) == S.clamp(bs) : List<&2, U32>}:
94  match bs:
95    case Nil{}:
96      {==}
97    case Con{+b, +bt}:
98      clamp_top_eq(Con{U32.and(b, 248), bt})
99
100def len_eq(+bs: List<&2, U32>) -> {X.len(bs) == C.length(U32, bs) : Nat}:
101  match bs:
102    case Nil{}:
103      {==}
104    case Con{+b, +bt}:
105      Equal.cong(Nat, Nat, z => 1n+z, X.len(bt), C.length(U32, bt), len_eq(bt))
106
107def nbits_eq(+k: List<&2, U32>) -> {X.nbits(k) == S.bits(k) : Nat}:
108  Equal.cong(Nat, Nat, z => Nat.sub(Nat.mul(8n, z), 1n), X.len(k), C.length(U32, k), len_eq(k))
109
110# or never exceeds the sum
111def bit_or_le(+a: Bool, +b: Bool) -> {Nat.is_le(SN.bit_value(Bool.or(a, b)), Nat.add(SN.bit_value(a), SN.bit_value(b))) == True{} : Bool}:
112  match a b:
113    case True{} True{}:
114      {==}
115    case True{} False{}:
116      {==}
117    case False{} True{}:
118      {==}
119    case False{} False{}:
120      {==}
121
122def or_le(+n: Nat, +x: Word(n), +m: Word(n)) -> {Nat.is_le(WD.uw(n, Word.or(n, x, m)), Nat.add(WD.uw(n, x), WD.uw(n, m))) == True{} : Bool}:
123  match n x m:
124    case 0n WNil{} WNil{}:
125      {==}
126    case 1n+ +p WCon{+a, +t1} WCon{+b, +t2}:
127      +u1 = WD.uw(p, t1)
128      +u2 = WD.uw(p, t2)
129      +d1 = N.double_le(WD.uw(p, Word.or(p, t1, t2)), Nat.add(u1, u2), or_le(p, t1, t2))
130      +d2 = L.subst(Nat, z => {Nat.is_le(Nat.double(WD.uw(p, Word.or(p, t1, t2))), z) == True{} : Bool}, Nat.double(Nat.add(u1, u2)), Nat.add(Nat.double(u1), Nat.double(u2)), NA.double_add(u1, u2), d1)
131      +s = M.le_add2(SN.bit_value(Bool.or(a, b)), Nat.double(WD.uw(p, Word.or(p, t1, t2))), Nat.add(SN.bit_value(a), SN.bit_value(b)), Nat.add(Nat.double(u1), Nat.double(u2)), bit_or_le(a, b), d2)
132      L.subst(Nat, z => {Nat.is_le(Nat.add(SN.bit_value(Bool.or(a, b)), Nat.double(WD.uw(p, Word.or(p, t1, t2)))), z) == True{} : Bool}, Nat.add(Nat.add(SN.bit_value(a), SN.bit_value(b)), Nat.add(Nat.double(u1), Nat.double(u2))), Nat.add(Nat.add(SN.bit_value(a), Nat.double(u1)), Nat.add(SN.bit_value(b), Nat.double(u2))), M.add4(SN.bit_value(a), SN.bit_value(b), Nat.double(u1), Nat.double(u2)), s)
133
134def or_le32(+x: U32, +m: U32) -> {Nat.is_le(v(U32.or(x, m)), Nat.add(v(x), v(m))) == True{} : Bool}:
135  match x m:
136    case U32{+a} U32{+b}:
137      %Equal.sym(Nat, UD.v(U32{Word.or(32n, a, b)}), WD.uw(32n, Word.or(32n, a, b)), UD.vw(Word.or(32n, a, b))) : {Nat.is_le(_, Nat.add(v(U32{a}), v(U32{b}))) == True{} : Bool}
138      %Equal.sym(Nat, UD.v(U32{a}), WD.uw(32n, a), UD.vw(a)) : {Nat.is_le(WD.uw(32n, Word.or(32n, a, b)), Nat.add(_, v(U32{b}))) == True{} : Bool}
139      %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.is_le(WD.uw(32n, Word.or(32n, a, b)), Nat.add(WD.uw(32n, a), _)) == True{} : Bool}
140      or_le(32n, a, b)
141
142def clamp_top_okb(+n: Nat, +xs: List<&2, U32>, +e: {LM.okb(1n+n, xs, 255n) == True{} : Bool}) -> {LM.okb(1n+n, X.clamp_top(xs), 255n) == True{} : Bool}:
143  match n xs:
144    case _ Nil{}:
145      Empty.absurd({LM.okb(1n+n, Nil{}, 255n) == True{} : Bool}, L.false_true(e))
146    case 0n Con{+x, Nil{}}:
147      +a = HH.and_le32(x, 127)
148      +o = or_le32(U32.and(x, 127), 64)
149      +b = N.le_trans(v(U32.or(U32.and(x, 127), 64)), Nat.add(v(U32.and(x, 127)), 64n), 255n, o, N.le_trans(Nat.add(v(U32.and(x, 127)), 64n), Nat.add(127n, 64n), 255n, M.le_add_r(v(U32.and(x, 127)), 127n, 64n, a), {==}))
150      L.and_intro(Nat.is_le(v(U32.or(U32.and(x, 127), 64)), 255n), True{}, b, {==})
151    case 0n Con{x, Con{y, yt}}:
152      Empty.absurd({LM.okb(1n, X.clamp_top(Con{x, Con{y, yt}}), 255n) == True{} : Bool}, L.false_true(LM.okb_tail(0n, x, Con{y, yt}, 255n, e)))
153    case 1n+m Con{x, Nil{}}:
154      Empty.absurd({LM.okb(2n+m, X.clamp_top(Con{x, Nil{}}), 255n) == True{} : Bool}, L.false_true(LM.okb_tail(1n+m, x, Nil{}, 255n, e)))
155    case 1n+ +m Con{+x, Con{+y, +yt}}:
156      L.and_intro(Nat.is_le(v(x), 255n), LM.okb(1n+m, X.clamp_top(Con{y, yt}), 255n), LM.okb_head(1n+m, x, Con{y, yt}, 255n, e), clamp_top_okb(m, Con{y, yt}, LM.okb_tail(1n+m, x, Con{y, yt}, 255n, e)))
157
158def clamp_okb(+k: List<&2, U32>, +e: {LM.okb(32n, k, 255n) == True{} : Bool}) -> {LM.okb(32n, X.clamp(k), 255n) == True{} : Bool}:
159  match k:
160    case Nil{}:
161      Empty.absurd({LM.okb(32n, Nil{}, 255n) == True{} : Bool}, L.false_true(e))
162    case Con{+b, +bt}:
163      +ha = N.le_trans(v(U32.and(b, 248)), 248n, 255n, HH.and_le32(b, 248), {==})
164      clamp_top_okb(31n, Con{U32.and(b, 248), bt}, L.and_intro(Nat.is_le(v(U32.and(b, 248)), 255n), LM.okb(31n, bt, 255n), ha, LM.okb_tail(31n, b, bt, 255n, e)))
165
166# ---- the swap bit ----
167
168def u0(+a: U32, +e: {v(a) == 0n : Nat}) -> {a == 0 : U32}:
169  U.injective(a, 0, e)
170
171def u1(+a: U32, +e: {v(a) == 1n : Nat}) -> {a == 1 : U32}:
172  U.injective(a, 1, e)
173
174# swap ^= k_t on bits
175def xor_bits(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ea: {v(a) == na : Nat}, +eb: {v(b) == nb : Nat}, +ha: {Nat.is_le(na, 1n) == True{} : Bool}, +hb: {Nat.is_le(nb, 1n) == True{} : Bool}) -> {v(U32.xor(a, b)) == S.bxor(na, nb) : Nat}:
176  match na nb:
177    case 0n 0n:
178      %Equal.sym(U32, a, 0, u0(a, ea)) : {v(U32.xor(_, b)) == 0n : Nat}
179      %Equal.sym(U32, b, 0, u0(b, eb)) : {v(U32.xor(0, _)) == 0n : Nat}
180      {==}
181    case 0n 1n:
182      %Equal.sym(U32, a, 0, u0(a, ea)) : {v(U32.xor(_, b)) == 1n : Nat}
183      %Equal.sym(U32, b, 1, u1(b, eb)) : {v(U32.xor(0, _)) == 1n : Nat}
184      {==}
185    case 1n 0n:
186      %Equal.sym(U32, a, 1, u1(a, ea)) : {v(U32.xor(_, b)) == 1n : Nat}
187      %Equal.sym(U32, b, 0, u0(b, eb)) : {v(U32.xor(1, _)) == 1n : Nat}
188      {==}
189    case 1n 1n:
190      %Equal.sym(U32, a, 1, u1(a, ea)) : {v(U32.xor(_, b)) == 0n : Nat}
191      %Equal.sym(U32, b, 1, u1(b, eb)) : {v(U32.xor(1, _)) == 0n : Nat}
192      {==}
193    case 2n+q _:
194      Empty.absurd({v(U32.xor(a, b)) == S.bxor(2n+q, nb) : Nat}, L.false_true(ha))
195    case _ 2n+q:
196      Empty.absurd({v(U32.xor(a, b)) == S.bxor(na, 2n+q) : Nat}, L.false_true(hb))
197
198def bxor_le(+a: Nat, +b: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {Nat.is_le(S.bxor(a, b), 1n) == True{} : Bool}:
199  match a:
200    case 0n:
201      hb
202    case 1n+q:
203      AR.sub_le2(1n, b)
204
205# ---- the encoding ----
206
207def byte_rt(+y: U32, +hy: {Nat.is_le(v(y), 255n) == True{} : Bool}) -> {U32.from_nat(v(y)) == y : U32}:
208  U.injective(U32.from_nat(v(y)), y, U.to_nat_from_nat(v(y), 8n, {==}, N.le_lt_succ(v(y), 255n, hy)))
209
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))
230
231# ---- decodeUCoordinate ----
232
233def mask_eq(+xs: List<&2, U32>) -> {F.mask_top(xs) == S.mask_last(xs) : List<&2, U32>}:
234  match xs:
235    case Nil{}:
236      {==}
237    case Con{+x, +xt}:
238      match xt:
239        case Nil{}:
240          {==}
241        case Con{+y, +yt}:
242          Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, F.mask_top(Con{y, yt}), S.mask_last(Con{y, yt}), mask_eq(Con{y, yt}))
243
244def mask_okb(+n: Nat, +xs: List<&2, U32>, +e: {LM.okb(1n+n, xs, 255n) == True{} : Bool}) -> {LM.okb(1n+n, F.mask_top(xs), 255n) == True{} : Bool}:
245  match n xs:
246    case _ Nil{}:
247      Empty.absurd({LM.okb(1n+n, Nil{}, 255n) == True{} : Bool}, L.false_true(e))
248    case 0n Con{+x, Nil{}}:
249      L.and_intro(Nat.is_le(v(U32.and(x, 127)), 255n), True{}, N.le_trans(v(U32.and(x, 127)), 127n, 255n, HH.and_le32(x, 127), {==}), {==})
250    case 0n Con{x, Con{y, yt}}:
251      Empty.absurd({LM.okb(1n, F.mask_top(Con{x, Con{y, yt}}), 255n) == True{} : Bool}, L.false_true(LM.okb_tail(0n, x, Con{y, yt}, 255n, e)))
252    case 1n+m Con{x, Nil{}}:
253      Empty.absurd({LM.okb(2n+m, F.mask_top(Con{x, Nil{}}), 255n) == True{} : Bool}, L.false_true(LM.okb_tail(1n+m, x, Nil{}, 255n, e)))
254    case 1n+ +m Con{+x, Con{+y, +yt}}:
255      L.and_intro(Nat.is_le(v(x), 255n), LM.okb(1n+m, F.mask_top(Con{y, yt}), 255n), LM.okb_head(1n+m, x, Con{y, yt}, 255n, e), mask_okb(m, Con{y, yt}, LM.okb_tail(1n+m, x, Con{y, yt}, 255n, e)))