proofs/crypto/blake/blake3/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 126 lines · 9 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
4import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/array.bend as A
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/compress.bend as P
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as LP
9
10# BLAKE3 public API theorem: for every packed input array and every
11# byte_length, the implementation's blake3 equals the specification's
12# (spec/crypto/blake/blake3.bend), including the rejection of lengths
13# past 4 * capacity. No axioms, no holes.
14#
15# The chain: compress.bend (the unrolled compression function is the list
16# specification's), read.bend (block reads and the final-block mask),
17# chunk.bend (chunk loops), tree.bend (the subtree stack computes the
18# specification's tree), loop.bend (the chunk loop runs the stack over the
19# specification's chunk list), and here the root, the digest and the API.
20
21law root_correct:
22  for +o: T.Out
23  {K.root_cv(o) == S.root(o) : T.CV}
24
25def root_correct(o):
26  match o:
27    case T.Out{+c,+b,+t,+len,+flags}: P.compress_correct(c,b,t,len,U32.or(flags,8))
28
29law unchecked_view:
30  for -a: Array<U32>
31  for +length: Nat
32  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
33  {K.unchecked(a,length) == S.hash(a,length) : T.CV}
34
35def unchecked_view(a,length,view):
36  match view:
37    case Tuple{+tree,pf}:
38      +n = Nat.div(Nat.sub(length,1n),1024n)
39      +last = Nat.sub(length,Nat.mul(n,1024n))
40      +cs = S.chunks(n,0,0,last,S.chunk_at(n,0,0,last,A.thaw(tree)))
41      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.unchecked(_,length) == S.hash(_,length) : T.CV}
42      Equal.trans(T.CV,
43        K.root_cv(K.chunks(n,0,0,last,(A.thaw(tree),K.StkNil{}))),
44        K.root_cv(LP.run(K.StkNil{},cs)),
45        S.root(S.tree(SC.length(T.Out,cs),cs)),
46        Equal.cong(T.Out,T.CV,o => K.root_cv(o),K.chunks(n,0,0,last,(A.thaw(tree),K.StkNil{})),LP.run(K.StkNil{},cs),LP.fuse(n,0,0,last,A.thaw(tree),K.StkNil{})),
47        Equal.trans(T.CV,
48          K.root_cv(LP.run(K.StkNil{},cs)),
49          K.root_cv(S.tree(SC.length(T.Out,cs),cs)),
50          S.root(S.tree(SC.length(T.Out,cs),cs)),
51          Equal.cong(T.Out,T.CV,o => K.root_cv(o),LP.run(K.StkNil{},cs),S.tree(SC.length(T.Out,cs),cs),LP.run_chunks(n,0,0,last,S.chunk_at(n,0,0,last,A.thaw(tree)))),
52          root_correct(S.tree(SC.length(T.Out,cs),cs))))
53
54law digest_correct:
55  for +c: T.CV
56  {K.digest(c) == S.digest(c) : Array<U32>}
57
58def digest_correct(c):
59  match c:
60    case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: {==}
61
62law checked_view:
63  for -a: Array<U32>
64  for +length: Nat
65  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
66  {K.checked(True{},a,length) == S.checked(True{},a,length) : Maybe<&1,Array<U32>>}
67
68def checked_view(a,length,view):
69  match view:
70    case Tuple{+tree,pf}:
71      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.checked(True{},_,length) == S.checked(True{},_,length) : Maybe<&1,Array<U32>>}
72      Equal.trans(Maybe<&1,Array<U32>>,
73        Some{K.digest(K.unchecked(A.thaw(tree),length))},
74        Some{K.digest(S.hash(A.thaw(tree),length))},
75        Some{S.digest(S.hash(A.thaw(tree),length))},
76        Equal.cong(T.CV,Maybe<&1,Array<U32>>,c => Some{K.digest(c)},K.unchecked(A.thaw(tree),length),S.hash(A.thaw(tree),length),unchecked_view(A.thaw(tree),length,A.reify(A.thaw(tree)))),
77        Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,d => Some{d},K.digest(S.hash(A.thaw(tree),length)),S.digest(S.hash(A.thaw(tree),length)),digest_correct(S.hash(A.thaw(tree),length))))
78
79law checked_correct:
80  for +valid: Bool
81  for a: Array<U32>
82  for +length: Nat
83  {K.checked(valid,a,length) == S.checked(valid,a,length) : Maybe<&1,Array<U32>>}
84
85def checked_correct(valid,a,length):
86  match valid:
87    case False{}: {==}
88    case True{}: checked_view(a,length,A.reify(a))
89
90law sized_correct:
91  for +length: Nat
92  for pair: Array<U32> & U32
93  {K.sized(length,pair) == S.sized(length,pair) : Maybe<&1,Array<U32>>}
94
95def sized_correct(length,pair):
96  (a,capacity) = pair
97  checked_correct(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
98
99# The public API: for every packed word array and every byte length.
100law blake3_correct:
101  for words: Array<U32>
102  for +byte_length: Nat
103  {K.blake3(words,byte_length) == S.blake3(words,byte_length) : Maybe<&1,Array<U32>>}
104
105def blake3_correct(words,byte_length):
106  sized_correct(byte_length,Array.size(U32,words))
107
108# Rejection: a length past 4 * capacity gives None.
109law blake3_rejects:
110  for a: Array<U32>
111  for +n: Nat
112  for +capacity: U32
113  for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}
114  {K.sized(n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}
115
116def blake3_rejects(a,n,capacity,invalid):
117  Equal.cong(Bool,Maybe<&1,Array<U32>>,b => K.checked(b,a,n),Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))),False{},invalid)
118
119# The digest is eight words.
120law digest_size:
121  for +c: T.CV
122  {Pair.snd(Array<U32>,U32,Array.size(U32,K.digest(c))) == 8 : U32}
123
124def digest_size(c):
125  match c:
126    case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: {==}