proofs/containers/doubly_linked_list/links.bend checks

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

7 imports

import Base
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ./state.bend as ST
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Definitions

def seg_c source · line 13 · raw

@+pl1:List<&2, U32> -> @+nl1:List<&2, U32> -> @+pl2:List<&2, U32> -> @+nl2:List<&2, U32> -> @+s:Nat -> @+t:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(pl1, s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(pl2, s) : U32} -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(nl1, s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(nl2, s) : U32} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl1, nl1, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl2, nl2, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), q) : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl1, nl1, s <> t, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl2, nl2, s <> t, p, q) : Bool}

def seg_fp source · line 20 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+y:Nat -> @+v:U32 -> @+xs:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, pl, y, v), nl, xs, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, xs, p, q) : Bool}

a write to the prev list off the segment leaves it

def seg_fn source · line 28 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+y:Nat -> @+v:U32 -> @+xs:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, nl, y, v), xs, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, xs, p, q) : Bool}

a write to the next list off the segment leaves it

def fll_fn source · line 36 · raw

@+nl:List<&2, U32> -> @+y:Nat -> @+v:U32 -> @+fl:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, fl) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, nl, y, v), fl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(nl, fl) : Bool}

a write to the next list off the free stack leaves it

def seg_app source · line 47 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), p, q) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, a, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, p), q)) : Bool}

a segment splits at an append

def segq source · line 61 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+t:List<&2, Nat> -> @+a:Nat -> @+p:U32 -> @+x:U32 -> @+y:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, a <> t, p, x) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(a <> t) == True{} : Bool} -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.lastn(t, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, nl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.lastn(t, a), y), a <> t, p, y) == True{} : Bool}

re-target the last id's next

def segp source · line 80 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+b:Nat -> @+t:List<&2, Nat> -> @+x:U32 -> @+q:U32 -> @+y:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, b <> t, x, q) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(b <> t) == True{} : Bool} -> @+hl:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, pl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, pl, b, y), nl, b <> t, y, q) == True{} : Bool}

re-target the first id's prev