proofs/lib/u32_tree.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as U32_tree

6 imports

import Base
import ./logic.bend as L
import ./array.bend as AR
import ../../spec/lib/common.bend as SC
import ./u32div.bend as UD
import ./words32.bend as W32

Definitions

def len_of source · line 11 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(T, d, t) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(T, t))) == True{} : Bool}

def uget source · line 14 · raw

@+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i))) : Pair(Array<U32>, U32)}

def uset_a source · line 17 · raw

@+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:U32 -> {Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t), i, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) : Array<U32>}

def uset_p source · line 20 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> @+i:Nat -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, t, i, x)) == True{} : Bool}

def uset_s source · line 23 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, t, i, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), i, x) : List<&2, U32>}