~/bend-docscommunity

proofs/api.bend checks

raw source on the hub · import 0x48cee57f42dae6ba4c727fbf982cdd4d/proofs/api.bend as Api

3 imports
import Base
import ../src/keccak.bend as K
import ../src/types.bend as T

Laws

law rejected provedsource · line 5 · raw

@a:Array<U32> -> @n:Nat -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.checked(24n, False{}, a, n) == None{} : Maybe<&1, Array<U32>>}

law digest_size provedsource · line 13 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.size(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s))) == 8 : U32}

law digest_word0 provedsource · line 25 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 0)) == word0(s) : U32}

law digest_word1 provedsource · line 37 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 1)) == word1(s) : U32}

law digest_word2 provedsource · line 49 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 2)) == word2(s) : U32}

law digest_word3 provedsource · line 61 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 3)) == word3(s) : U32}

law digest_word4 provedsource · line 73 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 4)) == word4(s) : U32}

law digest_word5 provedsource · line 85 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 5)) == word5(s) : U32}

law digest_word6 provedsource · line 97 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 6)) == word6(s) : U32}

law digest_word7 provedsource · line 109 · raw

@+s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> {Pair.snd(Array<U32>, U32, Array.get(U32, 0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.digest(s), 7)) == word7(s) : U32}

law capacity_gate provedsource · line 117 · raw

@a:Array<U32> -> @+n:Nat -> @+capacity:U32 -> @invalid:{Nat.is_le(n, Nat.mul(4n, U32.to_nat(capacity))) == False{} : Bool} -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.sized(24n, n, (a, capacity)) == None{} : Maybe<&1, Array<U32>>}

law suffix0 provedsource · line 128 · raw

@w:U32 -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.partial(w, 0n) == 1 : U32}

law suffix1 provedsource · line 134 · raw

@+w:U32 -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.partial(w, 1n) == U32.or(U32.and(w, 255), 256) : U32}

law suffix2 provedsource · line 140 · raw

@+w:U32 -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.partial(w, 2n) == U32.or(U32.and(w, 65535), 65536) : U32}

law suffix3 provedsource · line 146 · raw

@+w:U32 -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.partial(w, 3n) == U32.or(U32.and(w, 16777215), 16777216) : U32}

law whole_word provedsource · line 152 · raw

@+w:U32 -> @n:Nat -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.partial(w, 4n+n) == w : U32}

law empty_suffix provedsource · line 159 · raw

@w:U32 -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.pad_word(w, 0n, 0n) == 1 : U32}

law empty_last_word provedsource · line 165 · raw

@w:U32 -> {U32.or(0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.pad_word(w, 132n, 0n), 2147483648) == 2147483648 : U32}

law combined_padding provedsource · line 171 · raw

@+w:U32 -> {U32.or(0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.pad_word(w, 132n, 135n), 2147483648) == U32.or(U32.or(U32.and(w, 16777215), 16777216), 2147483648) : U32}

Definitions

def word0 source · line 21 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word1 source · line 33 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word2 source · line 45 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word3 source · line 57 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word4 source · line 69 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word5 source · line 81 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word6 source · line 93 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32

def word7 source · line 105 · raw

@s:0x48cee57f42dae6ba4c727fbf982cdd4d/src/types.State -> U32