~/bend-docscommunity

proofs/crypto/sha/packed/packed_proof.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_proof.bend as Packed_proof

10 imports
import Base
import ../../../../src/crypto/sha/packed/core.bend as Runtime
import ./legacy_model.bend as Legacy
import ./packed_array_proof.bend as A
import ../../../../src/crypto/sha/packed/packed.bend as P
import ../../../../spec/crypto/sha/packed.bend as R
import ./core_model.bend as C
import ../../../../spec/crypto/sha.bend as F
import ../../../../src/crypto/sha/state.bend as S
import ./conformance.bend as Conformance

Laws

law compress_correct provedsource · line 12 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+extra:Nat -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/core.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, extra, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law read16_correct provedsource · line 36 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read16(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 0n, index, False{}, 0n, 0n, s, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read15_correct provedsource · line 62 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read15(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 1n, index, False{}, 0n, 0n, s, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read14_correct provedsource · line 87 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read14(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 2n, index, False{}, 0n, 0n, s, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read13_correct provedsource · line 111 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read13(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 3n, index, False{}, 0n, 0n, s, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read12_correct provedsource · line 134 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read12(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 4n, index, False{}, 0n, 0n, s, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read11_correct provedsource · line 156 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read11(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 5n, index, False{}, 0n, 0n, s, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read10_correct provedsource · line 177 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read10(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 6n, index, False{}, 0n, 0n, s, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read9_correct provedsource · line 197 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read9(extra, index, s, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 7n, index, False{}, 0n, 0n, s, [w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read8_correct provedsource · line 216 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read8(extra, index, s, w0, w1, w2, w3, w4, w5, w6, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 8n, index, False{}, 0n, 0n, s, [w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read7_correct provedsource · line 234 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read7(extra, index, s, w0, w1, w2, w3, w4, w5, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 9n, index, False{}, 0n, 0n, s, [w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read6_correct provedsource · line 251 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read6(extra, index, s, w0, w1, w2, w3, w4, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 10n, index, False{}, 0n, 0n, s, [w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read5_correct provedsource · line 267 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read5(extra, index, s, w0, w1, w2, w3, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 11n, index, False{}, 0n, 0n, s, [w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read4_correct provedsource · line 282 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read4(extra, index, s, w0, w1, w2, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 12n, index, False{}, 0n, 0n, s, [w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read3_correct provedsource · line 296 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read3(extra, index, s, w0, w1, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 13n, index, False{}, 0n, 0n, s, [w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read2_correct provedsource · line 309 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read2(extra, index, s, w0, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 14n, index, False{}, 0n, 0n, s, [w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law read1_correct provedsource · line 321 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.read1(extra, index, s, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 15n, index, False{}, 0n, 0n, s, [], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law partial_correct provedsource · line 332 · raw

@+w:U32 -> @+delta:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.partial(w, delta) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.partial(w, delta) : U32}

law pad_choose_correct provedsource · line 344 · raw

@+c:Cmp -> @+w:U32 -> @+delta:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_choose(c, w, delta) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.pad_choose(c, w, delta) : U32}

law pad_word_correct provedsource · line 355 · raw

@+w:U32 -> @+pos:Nat -> @+remain:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w, pos, remain) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.pad_word(w, pos, remain) : U32}

law tail_word_correct provedsource · line 363 · raw

@+short:Bool -> @+w:U32 -> @+pos:Nat -> @+remain:Nat -> @+length:U32 -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.length_word(short, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w, pos, remain), length) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.length_word(short, 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.pad_word(w, pos, remain), length) : U32}

law padded_words_correct provedsource · line 375 · raw

@+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+remain:Nat -> @+total:Nat -> {[0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w0, 0n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w1, 4n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w2, 8n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w3, 12n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w4, 16n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w5, 20n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w6, 24n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w7, 28n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w8, 32n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w9, 36n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w10, 40n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w11, 44n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w12, 48n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w13, 52n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.length_word(Nat.is_lt(remain, 56n), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w14, 56n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/core.len_hi(total)), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.length_word(Nat.is_lt(remain, 56n), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad_word(w15, 60n, remain), 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/core.len_lo(total))] == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.padded_words([w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15], 0n, remain, total) : List<&2, U32>}

law pad16_correct provedsource · line 431 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad16(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 0n, index, True{}, remain, total, s, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad15_correct provedsource · line 467 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad15(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 1n, index, True{}, remain, total, s, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad14_correct provedsource · line 494 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad14(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 2n, index, True{}, remain, total, s, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad13_correct provedsource · line 520 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad13(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 3n, index, True{}, remain, total, s, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad12_correct provedsource · line 545 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad12(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 4n, index, True{}, remain, total, s, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad11_correct provedsource · line 569 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad11(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 5n, index, True{}, remain, total, s, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad10_correct provedsource · line 592 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad10(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 6n, index, True{}, remain, total, s, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad9_correct provedsource · line 614 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad9(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 7n, index, True{}, remain, total, s, [w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad8_correct provedsource · line 635 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad8(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, w6, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 8n, index, True{}, remain, total, s, [w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad7_correct provedsource · line 655 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad7(extra, index, s, remain, total, w0, w1, w2, w3, w4, w5, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 9n, index, True{}, remain, total, s, [w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad6_correct provedsource · line 674 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad6(extra, index, s, remain, total, w0, w1, w2, w3, w4, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 10n, index, True{}, remain, total, s, [w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad5_correct provedsource · line 692 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad5(extra, index, s, remain, total, w0, w1, w2, w3, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 11n, index, True{}, remain, total, s, [w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad4_correct provedsource · line 709 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad4(extra, index, s, remain, total, w0, w1, w2, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 12n, index, True{}, remain, total, s, [w2, w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad3_correct provedsource · line 725 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad3(extra, index, s, remain, total, w0, w1, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 13n, index, True{}, remain, total, s, [w1, w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad2_correct provedsource · line 740 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad2(extra, index, s, remain, total, w0, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 14n, index, True{}, remain, total, s, [w0], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law pad1_correct provedsource · line 754 · raw

@+extra:Nat -> @+index:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.pad1(extra, index, s, remain, total, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.gather(extra, 15n, index, True{}, remain, total, s, [], pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law final_extra_correct provedsource · line 767 · raw

@+extra:Nat -> @+more:Bool -> @+total:Nat -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.final_extra(extra, more, total, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.final_extra(extra, more, total, pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law blocks_correct provedsource · line 783 · raw

@+extra:Nat -> @+n:Nat -> @+index:U32 -> @+remain:Nat -> @+total:Nat -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.blocks(extra, n, index, remain, total, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.blocks(extra, n, index, remain, total, pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law blocks_zero_reified provedsource · line 792 · raw

@+extra:Nat -> @+index:U32 -> @+remain:Nat -> @+total:Nat -> @-a:Array<U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @view:Sigma<&2, &1, 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_array_proof.Tree, t => {a == 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_array_proof.thaw(t) : Array<U32>}> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.blocks(extra, 0n, index, remain, total, (a, s)) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.blocks(extra, 0n, index, remain, total, (a, s)) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law blocks_step_reified provedsource · line 816 · raw

@+p:Nat -> @+extra:Nat -> @+index:U32 -> @+remain:Nat -> @+total:Nat -> @-a:Array<U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @view:Sigma<&2, &1, 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_array_proof.Tree, t => {a == 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_array_proof.thaw(t) : Array<U32>}> -> @recurse:(@pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.blocks(extra, p, U32.add(index, 16), remain, total, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.blocks(extra, p, U32.add(index, 16), remain, total, pair) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.blocks(extra, 1n+p, index, remain, total, (a, s)) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.blocks(extra, 1n+p, index, remain, total, (a, s)) : Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)}

law hash_unchecked_correct provedsource · line 850 · raw

@a:Array<U32> -> @+length:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.hash_unchecked(a, length) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.hash_unchecked(a, length) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law checked_correct provedsource · line 861 · raw

@+valid:Bool -> @a:Array<U32> -> @+length:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.checked(valid, a, length) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.checked(valid, a, length) : Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State>}

law sized_correct provedsource · line 874 · raw

@+length:Nat -> @pair:Pair(Array<U32>, U32) -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.sized(length, pair) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.sized(length, pair) : Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State>}

law hash_correct provedsource · line 883 · raw

@a:Array<U32> -> @+length:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.hash(a, length) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.hash(a, length) : Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State>}

law digest_result_correct provedsource · line 891 · raw

@+r:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/legacy_model.packed_digest(r) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.digest_result(r) : Maybe<&2, List<&2, U32>>}

law sha256_correct provedsource · line 902 · raw

@a:Array<U32> -> @+length:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/legacy_model.sha256_packed(a, length) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.sha256(a, length) : Maybe<&2, List<&2, U32>>}

law sha256_reified provedsource · line 907 · raw

@-a:Array<U32> -> @+length:Nat -> @view:Sigma<&2, &1, 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_array_proof.Tree, t => {a == 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/packed_array_proof.thaw(t) : Array<U32>}> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/legacy_model.sha256_packed(a, length) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha/packed.sha256(a, length) : Maybe<&2, List<&2, U32>>}