proofs/crypto/sha512/conformance.bend source
proofs/crypto/sha512/conformance.bend on the hub · documented module
# Generated by tools/generators/sha512_gen.py; do not edit by hand.import Baseimport ../../../src/crypto/sha512/types.bend as Timport ../../../src/crypto/sha512/core.bend as Cimport ../../../spec/crypto/sha512.bend as F# src/crypto/sha512/core.bend refines spec/crypto/sha512.bend, the structure# of proofs/crypto/sha/conformance.bend (SHA-256) at 64-bit words: one round# and the feedforward are equal after opening every word into its halves;# the rolling window computes the spec's recurrence over the reverse history;# a block's rounds, the blocks, the parsing and the padding follow by# induction, each short tail by enumeration.law step_correct: for +s: T.State for +k: T.Lane for +w: T.Lane {C.step(s, k, w) == F.step(s, k, w) : T.State}def step_correct(s, k, w): match s k w: case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.W{kh, kl} T.W{wh, wl}: {==}law feedforward_correct: for +x: T.State for +y: T.State {C.feedforward(x, y) == F.feedforward(x, y) : T.State}def feedforward_correct(x, y): match x y: case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.H{T.W{ih, il}, T.W{jh, jl}, T.W{kh, kl}, T.W{lh, ll}, T.W{mh, ml}, T.W{nh, nl}, T.W{oh, ol}, T.W{ph, pl}}: {==}law next_correct: for +a: T.Lane for +b: T.Lane for +c: T.Lane for +d: T.Lane for +e: T.Lane for +f: T.Lane for +g: T.Lane for +h: T.Lane for +i: T.Lane for +j: T.Lane for +k: T.Lane for +l: T.Lane for +m: T.Lane for +n: T.Lane for +o: T.Lane for +p: T.Lane for +rest: List<&2, T.Lane> {C.next(b, g, o, p) == F.recurrence(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest) : T.Lane}def next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest): match b g o p: case T.W{bh, bl} T.W{gh, gl} T.W{oh, ol} T.W{ph, pl}: {==}law window_rounds_correct: for +q: Nat for +a: T.Lane for +b: T.Lane for +c: T.Lane for +d: T.Lane for +e: T.Lane for +f: T.Lane for +g: T.Lane for +h: T.Lane for +i: T.Lane for +j: T.Lane for +k: T.Lane for +l: T.Lane for +m: T.Lane for +n: T.Lane for +o: T.Lane for +p: T.Lane for +rest: List<&2, T.Lane> for +ks: List<&2, T.Lane> for +s: T.State {C.window_rounds(q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(s) : T.State}def window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s): match q ks: case 0n Nil{}: {==} case 0n x <> xt: {==} case 1n+r Nil{}: {==} case 1n+r x <> xt: %next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest) : {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) == F.rounds(xt, F.extension(r, _ <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(F.step(s, x, _)) : T.State} %step_correct(s, x, C.next(b, g, o, p)) : {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) == F.rounds(xt, F.extension(r, C.next(b, g, o, p) <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(_) : T.State} window_rounds_correct(r, C.next(b, g, o, p), a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p <> rest, xt, C.step(s, x, C.next(b, g, o, p)))law block_rounds_correct: for +ws: List<&2, T.Lane> for +q: Nat for +a: T.Lane for +b: T.Lane for +c: T.Lane for +d: T.Lane for +e: T.Lane for +f: T.Lane for +g: T.Lane for +h: T.Lane for +i: T.Lane for +j: T.Lane for +k: T.Lane for +l: T.Lane for +m: T.Lane for +n: T.Lane for +o: T.Lane for +p: T.Lane for +rest: List<&2, T.Lane> for +ks: List<&2, T.Lane> for +s: T.State {C.block_rounds(ws, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, List.append(&2, T.Lane, ws, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(s) : T.State}def block_rounds_correct(ws, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s): match ws ks: case Nil{} _: window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s) case w <> wt Nil{}: {==} case w <> wt x <> xt: %step_correct(s, x, w) : {C.block_rounds(w <> wt, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) == F.rounds(xt, List.append(&2, T.Lane, wt, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(_) : T.State} block_rounds_correct(wt, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, xt, C.step(s, x, w))law compress16_correct: for +a: T.Lane for +b: T.Lane for +c: T.Lane for +d: T.Lane for +e: T.Lane for +f: T.Lane for +g: T.Lane for +h: T.Lane for +i: T.Lane for +j: T.Lane for +k: T.Lane for +l: T.Lane for +m: T.Lane for +n: T.Lane for +o: T.Lane for +p: T.Lane for +q: Nat for +ks: List<&2, T.Lane> for +s: T.State {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == F.compress(F.schedule(q, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]), ks, s) : T.State}def compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s): +r = F.rounds(ks, List.append(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], F.extension(q, List.reverse(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]))))(s) %feedforward_correct(s, r) : {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == _ : T.State} Equal.cong(T.State, T.State, t => C.feedforward(s, t), C.block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, C.Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s), r, block_rounds_correct([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a, Nil{}, ks, s))law blocks_correct: for +ws: List<&2, T.Lane> for +q: Nat for +ks: List<&2, T.Lane> for +s: T.State {C.blocks(ws, q, ks, s) == F.blocks(F.schedules(ws, q), ks)(s) : T.State}def blocks_correct(ws, q, ks, s): match ws: case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest: %compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) : {C.blocks(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, q, ks, s) == F.blocks(F.schedules(rest, q), ks)(_) : T.State} blocks_correct(rest, q, ks, C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s)) case Nil{}: {==} case a <> Nil{}: {==} case a <> b <> Nil{}: {==} case a <> b <> c <> Nil{}: {==} case a <> b <> c <> d <> Nil{}: {==} case a <> b <> c <> d <> e <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> Nil{}: {==} case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> Nil{}: {==}law lanes_correct: for +bytes: List<&2, U32> {C.lanes(bytes) == F.words(bytes) : List<&2, T.Lane>}def lanes_correct(bytes): match bytes: case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest: %lanes_correct(rest) : {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.decode(b0, b1, b2, b3), F.decode(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>} {==} case Nil{}: {==} case b0 <> Nil{}: {==} case b0 <> b1 <> Nil{}: {==} case b0 <> b1 <> b2 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}: {==}law zeros_correct: for +r: Nat for +fits: Bool {C.zeros_if(r, fits) == F.zero_count_if(r, fits) : Nat}def zeros_correct(r, fits): match fits: case True{}: {==} case False{}: {==}law suffix_correct: for +n: Nat {C.suffix(n) == F.padding_suffix(n) : List<&2, U32>}def suffix_correct(n): %zeros_correct(Nat.mod(n, 128n), Nat.is_le(Nat.mod(n, 128n), 111n)) : {C.suffix(n) == 128 <> List.append(&2, U32, List.replicate(U32, _, 0), F.length_field(n)) : List<&2, U32>} {==}law digest_correct: for +s: T.State {C.digest_bytes(s) == F.digest_octets(F.digest(s)) : List<&2, U32>}def digest_correct(s): match s: case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}: {==}law digest_length: for +s: T.State {List.length(&2, U32, C.digest_bytes(s)) == 64n : Nat}def digest_length(s): match s: case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}: {==}law constants_correct: {C.round_constants() == F.constants() : List<&2, T.Lane>}def constants_correct(): {==}law initial_correct: {C.initial() == F.initial() : T.State}def initial_correct(): {==}law sha512_correct: for +bytes: List<&2, U32> {C.sha512(bytes) == F.sha512_bytes(bytes) : List<&2, U32>}def sha512_correct(bytes): +n = List.length(&2, U32, bytes) %suffix_correct(n) : {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(F.words( List.append(&2, U32, bytes, _)), 64n), F.constants())(F.initial()))) : List<&2, U32>} +padded = List.append(&2, U32, bytes, C.suffix(n)) %lanes_correct(padded) : {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(_, 64n), F.constants())(F.initial()))) : List<&2, U32>} %Equal.sym(List<&2, T.Lane>, C.round_constants(), F.constants(), constants_correct()) : {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), _)(F.initial()))) : List<&2, U32>} %Equal.sym(T.State, C.initial(), F.initial(), initial_correct()) : {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), C.round_constants())(_))) : List<&2, U32>} %blocks_correct(C.lanes(padded), 64n, C.round_constants(), C.initial()) : {C.sha512(bytes) == F.digest_octets(F.digest(_)) : List<&2, U32>} digest_correct(C.blocks(C.lanes(padded), 64n, C.round_constants(), C.initial()))