~/bend-docscommunity

proofs/containers/dynamic_array/growth.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/growth.bend as Growth

10 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/dynamic_array.bend as S
import ../../../src/containers/dynamic_array.bend as DA
import ./layout.bend as LY
import ./state.bend as ST
import ../../lib/list.bend as LL

Definitions

def grow_good source · line 16 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hdl:{Nat.is_lt(d, l) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, 1n+d, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})}}) == True{} : Bool}

The grown shadow (depth + 1, old tree as left half) is good when d < l.

def grow_model source · line 21 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t)) : List<&2, T>}

def sgstep source · line 25 · raw

@-T:Data -> @+k:Nat -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T>

def sgrow source · line 30 · raw

@-T:Data -> @f:Nat -> @+k:Nat -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T>

def fits_nat source · line 39 · raw

@+k:Nat -> @+d:Nat -> @+b:Bool -> @+e:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pow2(d)) == b : Bool} -> {Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool}

The source's own pow2 (still used for the 2^limit feasibility test, which is not cached) is the spec's.

def gstep_case source · line 42 · raw

@-T:Data -> @+k:Nat -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+b:Bool -> @+eb:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grow_step(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sgstep(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

def grow_until_real source · line 54 · raw

@-T:Data -> @+f:Nat -> @+k:Nat -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grow_until(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sgrow(T, f, k, sh)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

def fit_fits source · line 64 · raw

@+f:Nat -> @+d:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.fit(f, d, k) == d : Nat}

def sgrow_fits source · line 72 · raw

@-T:Data -> @+f:Nat -> @+k:Nat -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+h:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {sgrow(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T>}

def room_left source · line 80 · raw

@+d:Nat -> @+g:Nat -> @+l:Nat -> @+h:{Nat.is_le(Nat.add(d, 1n+g), l) == True{} : Bool} -> {Nat.is_lt(d, l) == True{} : Bool}

def fuel_shift source · line 83 · raw

@+d:Nat -> @+g:Nat -> @+l:Nat -> @+h:{Nat.is_le(Nat.add(d, 1n+g), l) == True{} : Bool} -> {Nat.is_le(Nat.add(1n+d, g), l) == True{} : Bool}

def sgrow_props source · line 86 · raw

@-T:Data -> @+f:Nat -> @+k:Nat -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hf:{Nat.is_le(Nat.add(d, f), l) == True{} : Bool} -> @+b:Bool -> @+eb:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(T, sgrow(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.fit(f, d, k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sgrow(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) == True{} : Bool})

def fe_case source · line 102 · raw

@+f1:Nat -> @+f2:Nat -> @+d:Nat -> @+k:Nat -> @+h1:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(Nat.add(d, f1))) == True{} : Bool} -> @+h2:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(Nat.add(d, f2))) == True{} : Bool} -> @+b:Bool -> @+eb:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.fit(f1, d, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.fit(f2, d, k) : Nat}

def pow2_gt source · line 114 · raw

@+k:Nat -> {Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool}