proofs/crypto/ed25519/bytes.bend
bend-collections-laws-crypto@1.0.0.0 · 149 lines · 18 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as SHA
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T512
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as HH
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend as S512
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
15
16
17
18
19
20def v(+x: U32) -> Nat:
21 U32.to_nat(x)
22
23
24
25def take_eq(+n: Nat, +xs: List<&2, U32>) -> {F.take(n, xs) == SE.first(n, xs) : List<&2, U32>}:
26 match n:
27 case 0n:
28 {==}
29 case 1n+ +m:
30 match xs:
31 case Nil{}:
32 {==}
33 case Con{+x, +xt}:
34 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, F.take(m, xt), SE.first(m, xt), take_eq(m, xt))
35
36def drop_eq(+n: Nat, +xs: List<&2, U32>) -> {F.drop(n, xs) == SE.rest(n, xs) : List<&2, U32>}:
37 match n:
38 case 0n:
39 {==}
40 case 1n+ +m:
41 match xs:
42 case Nil{}:
43 {==}
44 case Con{+x, +xt}:
45 drop_eq(m, xt)
46
47def cat_eq(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {E.cat(xs, ys) == SE.cat(xs, ys) : List<&2, U32>}:
48 match xs:
49 case Nil{}:
50 {==}
51 case Con{+x, +xt}:
52 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, E.cat(xt, ys), SE.cat(xt, ys), cat_eq(xt, ys))
53
54
55def pl(n: Nat, +m: Nat) -> Nat:
56 match n:
57 case 0n:
58 m
59 case 1n+k:
60 1n+pl(k, m)
61
62def take_okb(+n: Nat, +m: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(pl(n, m), xs, b) == True{} : Bool}) -> {LM.okb(n, F.take(n, xs), b) == True{} : Bool}:
63 match n:
64 case 0n:
65 {==}
66 case 1n+ +k:
67 match xs:
68 case Nil{}:
69 e
70 case Con{+x, +xt}:
71 L.and_intro(Nat.is_le(v(x), b), LM.okb(k, F.take(k, xt), b), L.and_left(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e), take_okb(k, m, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e)))
72
73def drop_okb(+n: Nat, +m: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(pl(n, m), xs, b) == True{} : Bool}) -> {LM.okb(m, F.drop(n, xs), b) == True{} : Bool}:
74 match n:
75 case 0n:
76 e
77 case 1n+ +k:
78 match xs:
79 case Nil{}:
80 Empty.absurd({LM.okb(m, Nil{}, b) == True{} : Bool}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
81 case Con{+x, +xt}:
82 drop_okb(k, m, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e))
83
84
85def e8(n: Nat) -> Nat:
86 match n:
87 case 0n:
88 0n
89 case 1n+k:
90 Nat.add(8n, e8(k))
91
92def bitlen_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {X.bitlen(xs) == e8(n) : Nat}:
93 match n xs:
94 case 0n Nil{}:
95 {==}
96 case 0n Con{x, xt}:
97 Empty.absurd({X.bitlen(Con{x, xt}) == 0n : Nat}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
98 case 1n+k Nil{}:
99 Empty.absurd({0n == e8(1n+k) : Nat}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
100 case 1n+ +k Con{+x, +xt}:
101 Equal.cong(Nat, Nat, z => Nat.add(8n, z), X.bitlen(xt), e8(k), bitlen_okb(k, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(k, xt, b), e)))
102
103def bitlen_256(+xs: List<&2, U32>, +e: {LM.okb(32n, xs, 255n) == True{} : Bool}) -> {X.bitlen(xs) == 256n : Nat}:
104 bitlen_okb(32n, xs, 255n, e)
105
106
107
108def sha_eq(+bytes: List<&2, U32>) -> {H.sha512(bytes) == SHA.sha512_bytes(bytes) : List<&2, U32>}:
109 S512.sha512_correct(bytes)
110
111def byte_and(+x: U32) -> {Nat.is_le(v(U32.and(x, 255)), 255n) == True{} : Bool}:
112 HH.and_le32(x, 255)
113
114def okb_con(+n: Nat, +x: U32, +t: List<&2, U32>, +hx: {Nat.is_le(v(x), 255n) == True{} : Bool}, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(1n+n, Con{x, t}, 255n) == True{} : Bool}:
115 L.and_intro(Nat.is_le(v(x), 255n), LM.okb(n, t, 255n), hx, ht)
116
117def octets_okb(+n: Nat, +x: U32, +t: List<&2, U32>, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(4n+n, C512.octets(x, t), 255n) == True{} : Bool}:
118 +b0 = U32.and(x, 255)
119 +b1 = U32.and(U32.shrn(x, 8n), 255)
120 +b2 = U32.and(U32.shrn(x, 16n), 255)
121 +b3 = U32.and(U32.shrn(x, 24n), 255)
122 +l0 = okb_con(n, b0, t, byte_and(x), ht)
123 +l1 = okb_con(1n+n, b1, Con{b0, t}, byte_and(U32.shrn(x, 8n)), l0)
124 +l2 = okb_con(2n+n, b2, Con{b1, Con{b0, t}}, byte_and(U32.shrn(x, 16n)), l1)
125 okb_con(3n+n, b3, Con{b2, Con{b1, Con{b0, t}}}, byte_and(U32.shrn(x, 24n)), l2)
126
127def lane_okb(+n: Nat, +l: T512.Lane, +t: List<&2, U32>, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(8n+n, C512.lane_octets(l, t), 255n) == True{} : Bool}:
128 match l:
129 case T512.W{+hi, +lo}:
130 octets_okb(4n+n, hi, C512.octets(lo, t), octets_okb(n, lo, t, ht))
131
132def digest_okb(+s: T512.State) -> {LM.okb(64n, C512.digest_bytes(s), 255n) == True{} : Bool}:
133 match s:
134 case T512.H{+a, +b, +c, +d, +e, +f, +g, +h}:
135 +th = C512.lane_octets(h, Nil{})
136 +tg = C512.lane_octets(g, th)
137 +tf = C512.lane_octets(f, tg)
138 +te = C512.lane_octets(e, tf)
139 +td = C512.lane_octets(d, te)
140 +tc = C512.lane_octets(c, td)
141 +tb = C512.lane_octets(b, tc)
142 lane_okb(56n, a, tb, lane_okb(48n, b, tc, lane_okb(40n, c, td, lane_okb(32n, d, te, lane_okb(24n, e, tf, lane_okb(16n, f, tg, lane_okb(8n, g, th, lane_okb(0n, h, Nil{}, {==}))))))))
143
144
145def sha_okb(+bytes: List<&2, U32>) -> {LM.okb(64n, H.sha512(bytes), 255n) == True{} : Bool}:
146 digest_okb(C512.blocks(C512.lanes(List.append(&2, U32, bytes, C512.suffix(List.length(&2, U32, bytes)))), 64n, C512.round_constants(), C512.initial()))
147
148def sha_lea(+bytes: List<&2, U32>) -> {LM.lea(H.sha512(bytes), 255n) == True{} : Bool}:
149 LM.okb_lea(64n, H.sha512(bytes), 255n, sha_okb(bytes))