Data.SHA256Schedule

1module Data.SHA256Schedule
2
3import Data.SHA256
4import Model.Config
5import Std.Natural
6
7family SHA256WordReadResult : Type 0
8constructor SHA256WordReadSucceeded
9field unrestricted sha256WordReadValue : (family ModelWord32)
10field unrestricted sha256WordReadRemaining : Bytes
11constructor SHA256WordReadFailed
12field unrestricted sha256WordReadError : (family SHA256ErrorCode)
13
14end-family
15
16family SHA256BlockDecodeResult : Type 0
17constructor SHA256BlockDecodeSucceeded
18field unrestricted sha256BlockDecodedSchedule : (family SHA256Schedule)
19field unrestricted sha256BlockDecodedWordCount : Nat
20constructor SHA256BlockDecodeFailed
21field unrestricted sha256BlockDecodeError : (family SHA256ErrorCode)
22field unrestricted sha256BlockDecodeWordOrdinal : Nat
23
24end-family
25
26family SHA256ScheduleLookupResult : Type 0
27constructor SHA256ScheduleLookupSucceeded
28field unrestricted sha256ScheduleLookupWord : (family ModelWord32)
29constructor SHA256ScheduleLookupFailed
30field unrestricted sha256ScheduleLookupError : (family SHA256ErrorCode)
31field unrestricted sha256ScheduleLookupIndex : Nat
32
33end-family
34
35def sha256NaturalFour =
36  (byte-to-nat (byte 4))
37
38def sha256NaturalSixteen =
39  (byte-to-nat (byte 16))
40
41def sha256NaturalSixtyFour =
42  (byte-to-nat (byte 64))
43
44def sha256ReadWord =
45  (lambda unrestricted input : Bytes .
46    (nat-eliminate
47      (lambda unrestricted sufficient : Nat . (family SHA256WordReadResult))
48      (constructor
49        SHA256WordReadResult
50        SHA256WordReadFailed
51        (constructor SHA256ErrorCode SHA256BlockLengthInvalid))
52      (lambda unrestricted predecessor : Nat .
53        (lambda unrestricted induction : (family SHA256WordReadResult) .
54          (app
55            (lambda unrestricted tail1 : Bytes .
56              (app
57                (lambda unrestricted tail2 : Bytes .
58                  (app
59                    (lambda unrestricted tail3 : Bytes .
60                      (app
61                        (lambda unrestricted tail4 : Bytes .
62                          (constructor
63                            SHA256WordReadResult
64                            SHA256WordReadSucceeded
65                            (constructor
66                              ModelWord32
67                              ModelWord32Value
68                              (bytes-head tail3)
69                              (bytes-head tail2)
70                              (bytes-head tail1)
71                              (bytes-head input))
72                            tail4))
73                        (bytes-tail tail3)))
74                    (bytes-tail tail2)))
75                (bytes-tail tail1)))
76            (bytes-tail input))))
77      (naturalLessOrEqual sha256NaturalFour (bytes-length input))))
78
79def sha256DecodeBlockWordsWithFuel =
80  (lambda unrestricted fuel : Nat .
81    (nat-eliminate
82      (lambda unrestricted current : Nat .
83        (pi unrestricted input : Bytes .
84          (pi unrestricted ordinal : Nat . (family SHA256BlockDecodeResult))))
85      (lambda unrestricted input : Bytes .
86        (lambda unrestricted ordinal : Nat .
87          (nat-eliminate
88            (lambda unrestricted emptyFlag : Nat . (family SHA256BlockDecodeResult))
89            (constructor
90              SHA256BlockDecodeResult
91              SHA256BlockDecodeFailed
92              (constructor SHA256ErrorCode SHA256BlockLengthInvalid)
93              ordinal)
94            (lambda unrestricted predecessor : Nat .
95              (lambda unrestricted induction : (family SHA256BlockDecodeResult) .
96                (constructor
97                  SHA256BlockDecodeResult
98                  SHA256BlockDecodeSucceeded
99                  (constructor SHA256Schedule SHA256ScheduleEnd)
100                  ordinal)))
101            (naturalIsZero (bytes-length input)))))
102      (lambda unrestricted predecessor : Nat .
103        (lambda unrestricted induction : (pi unrestricted input : Bytes . (pi unrestricted ordinal : Nat . (family SHA256BlockDecodeResult))) .
104          (lambda unrestricted input : Bytes .
105            (lambda unrestricted ordinal : Nat .
106              (eliminate
107                SHA256WordReadResult
108                (lambda unrestricted current : (family SHA256WordReadResult) .
109                  (family SHA256BlockDecodeResult))
110                (sha256ReadWord input)
111                (branch
112                  SHA256WordReadSucceeded
113                  word
114                  remaining
115                  .
116                  (eliminate
117                    SHA256BlockDecodeResult
118                    (lambda unrestricted current : (family SHA256BlockDecodeResult) .
119                      (family SHA256BlockDecodeResult))
120                    (induction remaining (succ ordinal))
121                    (branch
122                      SHA256BlockDecodeSucceeded
123                      tailSchedule
124                      finalCount
125                      .
126                      (constructor
127                        SHA256BlockDecodeResult
128                        SHA256BlockDecodeSucceeded
129                        (constructor SHA256Schedule SHA256ScheduleNext word tailSchedule)
130                        finalCount))
131                    (branch
132                      SHA256BlockDecodeFailed
133                      error
134                      failedOrdinal
135                      .
136                      (constructor
137                        SHA256BlockDecodeResult
138                        SHA256BlockDecodeFailed
139                        error
140                        failedOrdinal))))
141                (branch
142                  SHA256WordReadFailed
143                  error
144                  .
145                  (constructor SHA256BlockDecodeResult SHA256BlockDecodeFailed error ordinal)))))))
146      fuel))
147
148def sha256DecodeBlockWords =
149  (lambda unrestricted block : Bytes .
150    (nat-eliminate
151      (lambda unrestricted validLength : Nat . (family SHA256BlockDecodeResult))
152      (constructor
153        SHA256BlockDecodeResult
154        SHA256BlockDecodeFailed
155        (constructor SHA256ErrorCode SHA256BlockLengthInvalid)
156        zero)
157      (lambda unrestricted predecessor : Nat .
158        (lambda unrestricted induction : (family SHA256BlockDecodeResult) .
159          (sha256DecodeBlockWordsWithFuel sha256NaturalSixteen block zero)))
160      (naturalEqual (bytes-length block) sha256NaturalSixtyFour)))
161
162-- Drop the first `index` nodes of a schedule, returning the suffix that begins
163-- at that index (or the empty schedule when the index runs past the end).
164--
165-- This is a FIRST-ORDER fold: the accumulator is a `SHA256Schedule` VALUE, not a
166-- function. At each step it destructures the current suffix and keeps the tail --
167-- a shared sub-structure of the original list, no copy -- so producing the
168-- index-th suffix costs O(index) constant-work steps. (The list-recursion
169-- hypothesis `nodeInduction` is deliberately unused, so it is never materialized.)
170def sha256ScheduleDrop =
171  (lambda unrestricted index : Nat .
172    (lambda unrestricted schedule : (family SHA256Schedule) .
173      (nat-eliminate
174        (lambda unrestricted current : Nat . (family SHA256Schedule))
175        schedule
176        (lambda unrestricted predecessor : Nat .
177          (lambda unrestricted induction : (family SHA256Schedule) .
178            (eliminate
179              SHA256Schedule
180              (lambda unrestricted current : (family SHA256Schedule) . (family SHA256Schedule))
181              induction
182              (branch SHA256ScheduleEnd . (constructor SHA256Schedule SHA256ScheduleEnd))
183              (branch SHA256ScheduleNext word tail nodeInduction . tail))))
184        index)))
185
186-- Linear O(index) message-schedule lookup.
187--
188-- The previous definition walked the linked list with a `nat-eliminate` over the
189-- FULL index at every node, and its successor step re-invoked the list-recursion
190-- hypothesis (`(app induction predecessor)`) at every intermediate fold level.
191-- Because the VM evaluates a fold's induction eagerly, one lookup at index k
192-- forced a fresh lookup of the tail at 0,1,...,k-1 -- an exponential re-walk that
193-- made schedule expansion run in ~O(N^4) (~3.2 billion evals for a single 4-byte
194-- hash). A HIGHER-ORDER rewrite (function-valued accumulator) removes the
195-- re-invocation but still pays O(k^2) per lookup, because the VM symbolically
196-- unrolls the function accumulator into a term of size O(k) at every step.
197--
198-- This version is FIRST-ORDER: `sha256ScheduleDrop` folds the SCHEDULE VALUE
199-- itself to the suffix at `index` (O(index), shared sub-structures, no term
200-- building), then reads that suffix's head word. Result values are byte-for-byte
201-- identical to the original (index i still yields W[i]); only the cost changed,
202-- so the SHA-256 digest is preserved exactly.
203def sha256ScheduleLookup =
204  (lambda unrestricted schedule : (family SHA256Schedule) .
205    (lambda unrestricted index : Nat .
206      (eliminate
207        SHA256Schedule
208        (lambda unrestricted current : (family SHA256Schedule) .
209          (family SHA256ScheduleLookupResult))
210        (sha256ScheduleDrop index schedule)
211        (branch
212          SHA256ScheduleEnd
213          .
214          (constructor
215            SHA256ScheduleLookupResult
216            SHA256ScheduleLookupFailed
217            (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid)
218            index))
219        (branch
220          SHA256ScheduleNext
221          word
222          tail
223          nodeInduction
224          .
225          (constructor SHA256ScheduleLookupResult SHA256ScheduleLookupSucceeded word)))))
226
227def sha256ScheduleAppend =
228  (lambda unrestricted schedule : (family SHA256Schedule) .
229    (lambda unrestricted word : (family ModelWord32) .
230      (eliminate
231        SHA256Schedule
232        (lambda unrestricted current : (family SHA256Schedule) . (family SHA256Schedule))
233        schedule
234        (branch
235          SHA256ScheduleEnd
236          .
237          (constructor
238            SHA256Schedule
239            SHA256ScheduleNext
240            word
241            (constructor SHA256Schedule SHA256ScheduleEnd)))
242        (branch
243          SHA256ScheduleNext
244          head
245          tail
246          induction
247          .
248          (constructor SHA256Schedule SHA256ScheduleNext head induction)))))
249
250def sha256ScheduleLength =
251  (lambda unrestricted schedule : (family SHA256Schedule) .
252    (eliminate
253      SHA256Schedule
254      (lambda unrestricted current : (family SHA256Schedule) . Nat)
255      schedule
256      (branch SHA256ScheduleEnd . zero)
257      (branch SHA256ScheduleNext word tail induction . (succ induction))))