proofs/lib/array.bend checks

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

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 ../../spec/lib/common.bend as SC
import ./lemmas/proofs/nat_algebra.bend as NA

Types

type Tree source · line 17 · raw

@-T:Data -> Data

TLeaf
```
@-T:Data -> @value:T -> Tree<T>
```

TNode

@-T:Data -> @lo:Tree<T> -> @hi:Tree<T> -> Tree<T>

Definitions

def thaw source · line 21 · raw

@-T:Data -> @t:Tree<T> -> Array<T>

def freeze source · line 28 · raw

@-T:Data -> @a:Array<T> -> Tree<T>

def slots source · line 35 · raw

@-T:Data -> @t:Tree<T> -> List<&2, T>

def perfect source · line 42 · raw

@-T:Data -> @+d:Nat -> @t:Tree<T> -> Bool

def ndec source · line 56 · raw

@d:Nat -> @+j:Nat -> Bool

Mirror of an update at a Nat index (proof-level description of the new tree). left is this node's branch decision (see ndec); passing it as a parameter avoids matching on a computed value.

def tupd source · line 63 · raw

@-T:Data -> @d:Nat -> @t:Tree<T> -> @+j:Nat -> @+v:T -> @left:Bool -> Tree<T>

def upd source · line 76 · raw

@-T:Data -> @+d:Nat -> @t:Tree<T> -> @+j:Nat -> @+v:T -> Tree<T>

def trep source · line 79 · raw

@-T:Data -> @+d:Nat -> @+v:T -> Tree<T>

def freeze_thaw source · line 88 · raw

@-T:Data -> @+t:Tree<T> -> {freeze(T, thaw(T, t)) == t : Tree<T>}

def pf_left source · line 97 · raw

@-T:Data -> @+p:Nat -> @+l:Tree<T> -> @+r:Tree<T> -> @+pf:{perfect(T, 1n+p, TNode{l, r}) == True{} : Bool} -> {perfect(T, p, l) == True{} : Bool}

def pf_right source · line 100 · raw

@-T:Data -> @+p:Nat -> @+l:Tree<T> -> @+r:Tree<T> -> @+pf:{perfect(T, 1n+p, TNode{l, r}) == True{} : Bool} -> {perfect(T, p, r) == True{} : Bool}

def slots_length source · line 103 · raw

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

def trep_perfect source · line 117 · raw

@-T:Data -> @+d:Nat -> @+v:T -> {perfect(T, d, trep(T, d, v)) == True{} : Bool}

def trep_slots source · line 124 · raw

@-T:Data -> @+d:Nat -> @+v:T -> {slots(T, trep(T, d, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), v) : List<&2, T>}

def leaf_update source · line 135 · raw

@-T:Data -> @+x:T -> @+v:T -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n) == True{} : Bool} -> {[v] == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, [x], j, v) : List<&2, T>}

def leaf_value source · line 142 · raw

@-T:Data -> @+y:T -> @+j:Nat -> @+x:T -> @+hj:{Nat.is_lt(j, 1n) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, [y], j) == Some{x} : Maybe<&2, T>} -> {y == x : T}

def len_lt source · line 149 · raw

@-T:Data -> @+p:Nat -> @+l:Tree<T> -> @+j:Nat -> @+pl:{perfect(T, p, l) == True{} : Bool} -> @+h:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)) == True{} : Bool} -> {Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, slots(T, l))) == True{} : Bool}

def len_le source · line 153 · raw

@-T:Data -> @+p:Nat -> @+l:Tree<T> -> @+j:Nat -> @+pl:{perfect(T, p, l) == True{} : Bool} -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p), j) == True{} : Bool} -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, slots(T, l)), j) == True{} : Bool}

def upper_lt source · line 157 · raw

@+j:Nat -> @+p:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+p)) == True{} : Bool} -> @+le:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p), j) == True{} : Bool} -> {Nat.is_lt(Nat.sub(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)) == True{} : Bool}

def right_update source · line 160 · raw

@-T:Data -> @+p:Nat -> @+l:Tree<T> -> @+r:Tree<T> -> @+j:Nat -> @+v:T -> @+pl:{perfect(T, p, l) == True{} : Bool} -> @+le:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p), j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, slots(T, l), slots(T, r)), j, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, slots(T, l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, slots(T, r), Nat.sub(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)), v)) : List<&2, T>}

def right_nth source · line 164 · raw

@-T:Data -> @+p:Nat -> @+l:Tree<T> -> @+r:Tree<T> -> @+j:Nat -> @+pl:{perfect(T, p, l) == True{} : Bool} -> @+le:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p), j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, slots(T, l), slots(T, r)), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, slots(T, r), Nat.sub(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p))) : Maybe<&2, T>}

def tupd_perfect source · line 170 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+j:Nat -> @+v:T -> @+b:Bool -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {perfect(T, d, tupd(T, d, t, j, v, b)) == True{} : Bool}

def tupd_slots source · line 183 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+j:Nat -> @+v:T -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+b:Bool -> @+eb:{ndec(d, j) == b : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {slots(T, tupd(T, d, t, j, v, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, slots(T, t), j, v) : List<&2, T>}

def upd_perfect source · line 202 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+j:Nat -> @+v:T -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {perfect(T, d, upd(T, d, t, j, v)) == True{} : Bool}

def upd_slots source · line 205 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+j:Nat -> @+v:T -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {slots(T, upd(T, d, t, j, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, slots(T, t), j, v) : List<&2, T>}

def lt_bridge source · line 210 · raw

@+i:U32 -> @+p:Nat -> @+hp:{Nat.is_lt(p, 32n) == True{} : Bool} -> @+b:Bool -> @+eb:{U32.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(p)) == b : Bool} -> {Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)) == b : Bool}

def sub_bridge source · line 215 · raw

@+i:U32 -> @+p:Nat -> @+hp:{Nat.is_lt(p, 32n) == True{} : Bool} -> @+le:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p), U32.to_nat(i)) == True{} : Bool} -> {U32.to_nat(U32.sub(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(p))) == Nat.sub(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)) : Nat}

def size_thaw source · line 222 · raw

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

def get_go source · line 236 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+x:T -> @+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(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+b:Bool -> @+eb:{U32.is_lt(i, U32.shr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d))) == b : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.get.go(T, thaw(T, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d), i, b) == (thaw(T, t), x) : Pair(Array<T>, T)}

Base 2.0.32 passes each descent step its branch decision z; eb names it as U32.is_lt(i, U32.shr(2^d)), the value Base computes, so callers pass {==}.

def swap_go source · line 264 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+v:T -> @+x:T -> @+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(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+b:Bool -> @+eb:{U32.is_lt(i, U32.shr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d))) == b : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.swap.go(T, thaw(T, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d), i, v, b) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Pair(Array<T>, T)}

def get source · line 302 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+x:T -> @+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(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.get(T, thaw(T, t), i) == (thaw(T, t), x) : Pair(Array<T>, T)}

Public Base entry points. Premises: the tree is perfect of depth d < 32 and the index is below 2^d; x is the value currently stored at that index.

def swap source · line 307 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+v:T -> @+x:T -> @+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(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.swap(T, thaw(T, t), i, v) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Pair(Array<T>, T)}

def set source · line 312 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+v:T -> @+x:T -> @+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(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.set(T, thaw(T, t), i, v) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array<T>}

def new source · line 316 · raw

@-T:Data -> @+d:Nat -> @+v:T -> {Array.new(T, d, v) == thaw(T, trep(T, d, v)) : Array<T>}

def clone source · line 324 · raw

@-T:Data -> @+t:Tree<T> -> {Array.clone(T, thaw(T, t)) == (thaw(T, t), thaw(T, t)) : Pair(Array<T>, Array<T>)}

def get_set_same source · line 335 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+v:T -> @+x:T -> @+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(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.get(T, Array.set(T, thaw(T, t), i, v), i) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), v) : Pair(Array<T>, T)}

def get_set_other source · line 342 · raw

@-T:Data -> @+d:Nat -> @+t:Tree<T> -> @+i:U32 -> @+j:U32 -> @+v:T -> @+x:T -> @+y:T -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hj:{Nat.is_lt(U32.to_nat(j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ne:{Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == False{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, slots(T, t), U32.to_nat(j)) == Some{y} : Maybe<&2, T>} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {Array.get(T, Array.set(T, thaw(T, t), i, v), j) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), y) : Pair(Array<T>, T)}