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))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.