proofs/containers/doubly_linked_list/grow.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/grow.bend as Grow

13 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ./state.bend as ST
import ./rel.bend as RL
import ./vals.bend as VA
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Definitions

def nth0_app source · line 19 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, xs, ys), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(xs, i) : U32}

def val_app source · line 28 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+ys:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, vl, ys), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vl, i) : Maybe<&2, T>}

def p2_c source · line 68 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(b)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {c == True{} : Bool}

2^a < 2^b: a < b

def p2_inv source · line 76 · raw

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

def shl_cap source · line 80 · raw

@+cap:U32 -> @+d:Nat -> @+hd:{Nat.is_lt(d, 29n) == True{} : Bool} -> @+hcap:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(cap)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d)) == True{} : Bool}

the doubled capacity

def gz_ext source · line 88 · raw

@+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+d:Nat -> @+pg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, gT) == True{} : Bool} -> @+fr:Nat -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) == fr : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)}), fr) == True{} : Bool}

Templates

template seg_ext source · line 39 · raw

@-T:Data -> @+pl:List<&2, U32> -> @+pz:List<&2, U32> -> @+nl:List<&2, U32> -> @+nz:List<&2, U32> -> @+sl:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, sl, fr, vl) == True{} : Bool} -> @+hp:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, pl)) == True{} : Bool} -> @+hn:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, nl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, pl, pz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, nl, nz), sl, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, sl, p, q) : Bool}

the links of a live list, after the blocks are extended

template slok_ext source · line 55 · raw

@-T:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+ys:List<&2, Maybe<&2, T>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, vl, ys)) == True{} : Bool}

live ids stay live when vacant slots are appended

template lvin_ext source · line 93 · raw

@-T:Data -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+d:Nat -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0n, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})}), 0n, sl) == True{} : Bool}