proofs/lib/words32.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/words32.bend as Words32

10 imports

import Base
import ./logic.bend as L
import ./u32alg.bend as A
import ./u32.bend as UW
import ./word.bend as WD
import ./u32div.bend as UD
import ./nat.bend as N
import ../../spec/lib/common.bend as SC
import ../../src/containers/hash_table.bend as H
import ./arith.bend as AT

Definitions

def eq_sym_c source · line 16 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{U32.is_eq(a, b) == c : Bool} -> @+d:Bool -> @+hd:{U32.is_eq(b, a) == d : Bool} -> {c == d : Bool}

def eq_sym_u32 source · line 27 · raw

@+a:U32 -> @+b:U32 -> {U32.is_eq(a, b) == U32.is_eq(b, a) : Bool}

def inc_val source · line 30 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+i:U32 -> @+h:{Nat.is_lt(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(i), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.inc(i)) == 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(i) : Nat}

def link_val source · line 36 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+hs:{Nat.is_lt(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(0xa7e654f9780078ca65bf9e187da99d3e/src/containers/hash_table.link(s)) == 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(s) : Nat}

def link_nz_c source · line 39 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+hs:{Nat.is_lt(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/containers/hash_table.link(s), 0) == c : Bool} -> {c == False{} : Bool}

def link_nz source · line 47 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+hs:{Nat.is_lt(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {U32.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/containers/hash_table.link(s), 0) == False{} : Bool}

def nth0 source · line 50 · raw

@tb:List<&2, U32> -> @+i:Nat -> U32

def nth_some source · line 59 · raw

@+tb:List<&2, U32> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, tb)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(U32, tb, i) == Some{nth0(tb, i)} : Maybe<&2, U32>}

def nth0_upd_same source · line 68 · raw

@+xs:List<&2, U32> -> @+i:Nat -> @+v:U32 -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {nth0(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(U32, xs, i, v), i) == v : U32}

def nth0_upd_other source · line 77 · raw

@+xs:List<&2, U32> -> @+i:Nat -> @+j:Nat -> @+v:U32 -> @+h:{Nat.is_eq(i, j) == False{} : Bool} -> {nth0(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(U32, xs, i, v), j) == nth0(xs, j) : U32}

def pow_one source · line 90 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(d, one) : Nat}

def pow_le32 source · line 93 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def bound32 source · line 98 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(1n+d, 32n) == True{} : Bool} -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(1n+x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}