~/bend-docscommunity

proofs/crypto/sha512/conformance.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend as Conformance

Generated by tools/generators/sha512_gen.py; do not edit by hand.

4 imports
import Base
import ../../../src/crypto/sha512/types.bend as T
import ../../../src/crypto/sha512/core.bend as C
import ../../../spec/crypto/sha512.bend as F

Laws

law step_correct provedsource · line 14 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.step(s, k, w) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.step(s, k, w) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law feedforward_correct provedsource · line 25 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.feedforward(x, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.feedforward(x, y) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law next_correct provedsource · line 35 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+e:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+i:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+j:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+m:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+n:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+rest:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.next(b, g, o, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.recurrence(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane}

law window_rounds_correct provedsource · line 60 · raw

@+q:Nat -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+e:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+i:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+j:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+m:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+n:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+rest:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.window_rounds(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.rounds(ks, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest), s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law block_rounds_correct provedsource · line 101 · raw

@+ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+q:Nat -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+e:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+i:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+j:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+m:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+n:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+rest:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.block_rounds(ws, q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.rounds(ks, List.append(&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane, ws, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)), s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law compress16_correct provedsource · line 138 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+e:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+i:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+j:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+m:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+n:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+q:Nat -> @+ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.compress(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.schedule(q, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]), ks, s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law blocks_correct provedsource · line 167 · raw

@+ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+q:Nat -> @+ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(ws, q, ks, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.blocks(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.schedules(ws, q), ks, s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law lanes_correct provedsource · line 213 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(bytes) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.words(bytes) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>}

law zeros_correct provedsource · line 240 · raw

@+r:Nat -> @+fits:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.zeros_if(r, fits) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.zero_count_if(r, fits) : Nat}

law suffix_correct provedsource · line 252 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.suffix(n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.padding_suffix(n) : List<&2, U32>}

law digest_correct provedsource · line 261 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.digest_bytes(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.digest_octets(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.digest(s)) : List<&2, U32>}

law digest_length provedsource · line 270 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.digest_bytes(s)) == 64n : Nat}

law constants_correct provedsource · line 279 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.constants : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>}

law initial_correct provedsource · line 285 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.initial == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.initial : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law sha512_correct provedsource · line 291 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.sha512(bytes) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.sha512_bytes(bytes) : List<&2, U32>}