~/bend-docscommunity

proofs/crypto/hash/incremental.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend as Incremental

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

12 imports
import Base
import ../../../src/crypto/sha/state.bend as S256
import ../../../src/crypto/sha/core.bend as C256
import ../../../src/crypto/sha/sha256.bend as SHA256
import ../../../src/crypto/sha512/types.bend as T512
import ../../../src/crypto/sha512/core.bend as C512
import ../../../src/crypto/keccak/types.bend as TK
import ../../../src/crypto/keccak/permutation.bend as P
import ../../../src/crypto/sha3/core.bend as C3
import ../../../src/crypto/hash.bend as H
import ../sha/conformance.bend as SC
import ./lists.bend as L

Laws

law absorb256_inv provedsource · line 39 · raw

@+fuel:Nat -> @+bytes:List<&2, U32> -> @+q:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/state.State -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, bytes, z), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, s) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, buf256(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.absorb256(fuel, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.read256_0(bytes), bytes, q, s)), z), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, st256(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.absorb256(fuel, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.read256_0(bytes), bytes, q, s))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/state.State}

law step256_inv provedsource · line 187 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> @+xs:List<&2, U32> -> @+q:Nat -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, List.append(&2, U32, buf256(st), xs), z), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, st256(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, buf256(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.step256(st, xs, q)), z), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, st256(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.step256(st, xs, q))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/state.State}

law fold256_inv provedsource · line 207 · raw

@+cs:List<&2, List<&2, U32>> -> @+q:Nat -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, List.append(&2, U32, buf256(st), List.concat(&2, U32, cs)), z), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, st256(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, buf256(fold256(cs, q, st)), z), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, st256(fold256(cs, q, st))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/state.State}

law state256 provedsource · line 240 · raw

@+cs:List<&2, List<&2, U32>> -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.fold(cs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256H{st, len}) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256H{fold256(cs, 48n, st), Nat.add(len, List.length(&2, U32, List.concat(&2, U32, cs)))} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Hasher}

law finish256_eta provedsource · line 257 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> @+len:Nat -> @+q:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.finish256(st, len, q) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, buf256(st), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.suffix(len)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, st256(st)))) : List<&2, U32>}

law incremental256 provedsource · line 269 · raw

@+cs:List<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha256, cs)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, List.concat(&2, U32, cs), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.suffix(List.length(&2, U32, List.concat(&2, U32, cs)))), 48n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.initial))) : List<&2, U32>}

digest(update_all(new, chunks)) is the padded block loop over concat(chunks).

law absorb512_inv provedsource · line 298 · raw

@+fuel:Nat -> @+bytes:List<&2, U32> -> @+q:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, bytes, z)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, s) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, buf512(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.absorb512(fuel, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.read512_0(bytes), bytes, q, s)), z)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, st512(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.absorb512(fuel, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.read512_0(bytes), bytes, q, s))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law step512_inv provedsource · line 571 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> @+xs:List<&2, U32> -> @+q:Nat -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, List.append(&2, U32, buf512(st), xs), z)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, st512(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, buf512(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.step512(st, xs, q)), z)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, st512(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.step512(st, xs, q))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law fold512_inv provedsource · line 591 · raw

@+cs:List<&2, List<&2, U32>> -> @+q:Nat -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, List.append(&2, U32, buf512(st), List.concat(&2, U32, cs)), z)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, st512(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, buf512(fold512(cs, q, st)), z)), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, st512(fold512(cs, q, st))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State}

law state512 provedsource · line 624 · raw

@+cs:List<&2, List<&2, U32>> -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.fold(cs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512H{st, len}) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512H{fold512(cs, 64n, st), Nat.add(len, List.length(&2, U32, List.concat(&2, U32, cs)))} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Hasher}

law finish512_eta provedsource · line 641 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> @+len:Nat -> @+q:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.finish512(st, len, q) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, buf512(st), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.suffix(len))), q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, st512(st))) : List<&2, U32>}

law incremental512 provedsource · line 653 · raw

@+cs:List<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha512, cs)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.blocks(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lanes(List.append(&2, U32, List.concat(&2, U32, cs), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.suffix(List.length(&2, U32, List.concat(&2, U32, cs))))), 64n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.round_constants, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.initial)) : List<&2, U32>}

digest(update_all(new, chunks)) is the padded block loop over concat(chunks).

law absorb3_inv provedsource · line 682 · raw

@+fuel:Nat -> @+bytes:List<&2, U32> -> @+q:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, bytes, z)), q, s) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, buf3(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.absorb3(fuel, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.read3_0(bytes), bytes, q, s)), z)), q, st3(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.absorb3(fuel, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.read3_0(bytes), bytes, q, s))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law step3_inv provedsource · line 971 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> @+xs:List<&2, U32> -> @+q:Nat -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, List.append(&2, U32, buf3(st), xs), z)), q, st3(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, buf3(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.step3(st, xs, q)), z)), q, st3(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.step3(st, xs, q))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law fold3_inv provedsource · line 991 · raw

@+cs:List<&2, List<&2, U32>> -> @+q:Nat -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> @+z:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, List.append(&2, U32, buf3(st), List.concat(&2, U32, cs)), z)), q, st3(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, buf3(fold3(cs, q, st)), z)), q, st3(fold3(cs, q, st))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law state3 provedsource · line 1024 · raw

@+cs:List<&2, List<&2, U32>> -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.fold(cs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3H{st, len}) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3H{fold3(cs, 24n, st), Nat.add(len, List.length(&2, U32, List.concat(&2, U32, cs)))} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Hasher}

law finish3_eta provedsource · line 1041 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> @+len:Nat -> @+q:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.finish3(st, len, q) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, buf3(st), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.suffix(len))), q, st3(st))) : List<&2, U32>}

law incremental3 provedsource · line 1053 · raw

@+cs:List<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha3_256, cs)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(List.append(&2, U32, List.concat(&2, U32, cs), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.suffix(List.length(&2, U32, List.concat(&2, U32, cs))))), 24n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.zero)) : List<&2, U32>}

digest(update_all(new, chunks)) is the padded block loop over concat(chunks).

Definitions

def st256 source · line 29 · raw

@st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/state.State

def buf256 source · line 34 · raw

@st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> List<&2, U32>

def fold256 source · line 200 · raw

@cs:List<&2, List<&2, U32>> -> @+q:Nat -> @st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha256State

The state after each chunk in turn.

def st512 source · line 288 · raw

@st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

def buf512 source · line 293 · raw

@st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> List<&2, U32>

def fold512 source · line 584 · raw

@cs:List<&2, List<&2, U32>> -> @+q:Nat -> @st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha512State

The state after each chunk in turn.

def st3 source · line 672 · raw

@st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State

def buf3 source · line 677 · raw

@st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> List<&2, U32>

def fold3 source · line 984 · raw

@cs:List<&2, List<&2, U32>> -> @+q:Nat -> @st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.Sha3State

The state after each chunk in turn.