proofs/lib/array2.bend checks

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

7 imports

import Base
import ./logic.bend as L
import ./nat.bend as N
import ./u32.bend as U
import ./list.bend as LL
import ./array.bend as AR
import ../../spec/lib/common.bend as SC

Definitions

def thaw2 source · line 23 · raw

@t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> Array<Array<U32>>

def size_thaw2 source · line 30 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t) == True{} : Bool} -> {Array.size(Array<U32>, thaw2(t)) == (thaw2(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d)) : Pair(Array<Array<U32>>, U32)}

def swap_go2 source · line 42 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> @+i:U32 -> @+vt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+xt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, t), U32.to_nat(i)) == Some{xt} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>>} -> @+b:Bool -> @+eb:{U32.is_lt(i, U32.shr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d))) == b : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t) == True{} : Bool} -> {Array.swap.go(Array<U32>, thaw2(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, vt), b) == (thaw2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t, U32.to_nat(i), vt)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, xt)) : Pair(Array<Array<U32>>, Array<U32>)}

def swap2 source · line 79 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> @+i:U32 -> @+vt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+xt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, t), U32.to_nat(i)) == Some{xt} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>>} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t) == True{} : Bool} -> {Array.swap(Array<U32>, thaw2(t), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, vt)) == (thaw2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t, U32.to_nat(i), vt)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, xt)) : Pair(Array<Array<U32>>, Array<U32>)}

Public Base entry points at the nested element type.

def set2 source · line 84 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> @+i:U32 -> @+vt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+xt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, t), U32.to_nat(i)) == Some{xt} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>>} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t) == True{} : Bool} -> {Array.set(Array<U32>, thaw2(t), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, vt)) == thaw2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>, d, t, U32.to_nat(i), vt)) : Array<Array<U32>>}

def node_lo source · line 89 · raw

@+lt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> @+rt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>> -> {ANode{thaw2(lt), thaw2(rt)} == thaw2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{lt, rt}) : Array<Array<U32>>}

Doubling on either side, as the vertex table grows.