proofs/crypto/sha/packed/legacy_model.bend

bend-collections@1.0.0.0 · 60 lines · 8 definitions

1# PROOF-ONLY historical list model. Not imported by the production API.
2import Base
3import bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend as Runtime
4import bend-collections@1.0.0.0/src/crypto/sha/state.bend as State
5import bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as Core
6import bend-collections@1.0.0.0/src/crypto/sha/packed/packed.bend as Packed
7import bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend as Proof
8
9# The core refinement theorem quantifies over every constant table.
10# Instantiate the verified core with the FIPS 180-4 constants.
11def constants() -> List<&2, U32>:
12  [1116352408, 1899447441, 3049323471, 3921009573,
13   961987163, 1508970993, 2453635748, 2870763221,
14   3624381080, 310598401, 607225278, 1426881987,
15   1925078388, 2162078206, 2614888103, 3248222580,
16   3835390401, 4022224774, 264347078, 604807628,
17   770255983, 1249150122, 1555081692, 1996064986,
18   2554220882, 2821834349, 2952996808, 3210313671,
19   3336571891, 3584528711, 113926993, 338241895,
20   666307205, 773529912, 1294757372, 1396182291,
21   1695183700, 1986661051, 2177026350, 2456956037,
22   2730485921, 2820302411, 3259730800, 3345764771,
23   3516065817, 3600352804, 4094571909, 275423344,
24   430227734, 506948616, 659060556, 883997877,
25   958139571, 1322822218, 1537002063, 1747873779,
26   1955562222, 2024104815, 2227730452, 2361852424,
27   2428436474, 2756734187, 3204031479, 3329325298]
28
29def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
30  Core.sha256(bytes)
31
32def ascii(s: String) -> List<&2, U32>:
33  Core.ascii(s)
34
35def hex(ws: List<&2, U32>) -> String:
36  Core.hex(ws)
37
38# Big-endian octets, represented as U32 values in 0..255.
39def digest_bytes(ws: List<&2, U32>) -> List<&2, U32>:
40  match ws:
41    case Nil{}:
42      Nil{}
43    case +w <> tail:
44      U32.and(U32.shrn(w, 24n), 255) <>
45      U32.and(U32.shrn(w, 16n), 255) <>
46      U32.and(U32.shrn(w, 8n), 255) <>
47      U32.and(w, 255) <> digest_bytes(tail)
48
49def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
50  digest_bytes(sha256(bytes))
51
52def packed_digest(r: Maybe<&2,State.State>) -> Maybe<&2,List<&2,U32>>:
53  match r:
54    case None{}: None{}
55    case Some{s}: Some{Core.digest(s)}
56
57# Four bytes per U32, big-endian word order. Returns None for an oversized length.
58# This consumes the array; existing list APIs above retain their original behavior.
59def sha256_packed(words: Array<U32>, byte_length: Nat) -> Maybe<&2,List<&2,U32>>:
60  packed_digest(Packed.hash(words,byte_length))