proofs/containers/doubly_linked_list/lv.bend
bend-collections-laws-containers@1.0.0.0 · 113 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rel.bend as RL
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as VA
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
10
11# Liveness of ids after writes to the value list, and the live and vacant
12# id lists under them.
13
14
15def live_other(-T: Data, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +v: Maybe<&2, T>, +y: Nat, +ne: {Nat.is_eq(n, y) == False{} : Bool}) -> {ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), y) == ST.live(T, vl, y) : Bool}:
16 Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, SC.update(Maybe<&2, T>, vl, n, v), y), S.val_of(T, vl, y), VA.val_upd_other(T, vl, n, y, v, ne))
17
18def live_same(-T: Data, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +v: Maybe<&2, T>, +hl: {Nat.is_lt(n, SC.length(Maybe<&2, T>, vl)) == True{} : Bool}) -> {ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), n) == ST.some_b(T, v) : Bool}:
19 Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, SC.update(Maybe<&2, T>, vl, n, v), n), v, VA.val_upd_same(T, vl, n, v, hl))
20
21def live_c(-T: Data, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +v: Maybe<&2, T>, +y: Nat, +hl: {Nat.is_lt(n, SC.length(Maybe<&2, T>, vl)) == True{} : Bool}, +hv: {ST.some_b(T, v) == True{} : Bool}, +h: {ST.live(T, vl, y) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(n, y) == c : Bool}) -> {ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), y) == True{} : Bool}:
22 match c:
23 case True{}:
24 L.subst(Nat, z => {ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), z) == True{} : Bool}, n, y, N.eq_from_is_eq(n, y, hc), RL.by_eq(ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), n), ST.some_b(T, v), live_same(T, vl, n, v, hl), hv))
25 case False{}:
26 RL.by_eq(ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), y), ST.live(T, vl, y), live_other(T, vl, n, v, y, hc), h)
27
28# a live value written anywhere keeps the live ids live
29def slok_upd(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +v: Maybe<&2, T>, +hl: {Nat.is_lt(n, SC.length(Maybe<&2, T>, vl)) == True{} : Bool}, +hv: {ST.some_b(T, v) == True{} : Bool}, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {ST.slok(~T, xs, fr, SC.update(Maybe<&2, T>, vl, n, v)) == True{} : Bool}:
30 match xs:
31 case Nil{}:
32 {==}
33 case Con{+x, +t}:
34 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
35 +h1 = L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
36 +hx = L.and_intro(Nat.is_lt(x, fr), ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x), L.and_left(Nat.is_lt(x, fr), ST.live(T, vl, x), h0), live_c(T, vl, n, v, x, hl, hv, L.and_right(Nat.is_lt(x, fr), ST.live(T, vl, x), h0), Nat.is_eq(n, x), {==}))
37 L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x)), ST.slok(~T, t, fr, SC.update(Maybe<&2, T>, vl, n, v)), hx, slok_upd(~T, t, fr, vl, n, v, hl, hv, h1))
38
39def ne_hd(+x: Nat, +n: Nat, +t: List<&2, Nat>, +h: {NL.memn(n, Con{x, t}) == False{} : Bool}) -> {Nat.is_eq(n, x) == False{} : Bool}:
40 NL.ne_sym(x, n, NL.or_ff_l(Nat.is_eq(x, n), NL.memn(n, t), h))
41
42def ne_tl(+x: Nat, +n: Nat, +t: List<&2, Nat>, +h: {NL.memn(n, Con{x, t}) == False{} : Bool}) -> {NL.memn(n, t) == False{} : Bool}:
43 NL.or_ff_r(Nat.is_eq(x, n), NL.memn(n, t), h)
44
45# a write off the ids keeps them as they were
46def slok_off(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +v: Maybe<&2, T>, +hn: {NL.memn(n, xs) == False{} : Bool}, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {ST.slok(~T, xs, fr, SC.update(Maybe<&2, T>, vl, n, v)) == True{} : Bool}:
47 match xs:
48 case Nil{}:
49 {==}
50 case Con{+x, +t}:
51 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
52 +h1 = L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
53 +hx = RL.by_eq(Bool.and(Nat.is_lt(x, fr), ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x)), Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_lt(x, fr), z), ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x), ST.live(T, vl, x), live_other(T, vl, n, v, x, ne_hd(x, n, t, hn))), h0)
54 L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x)), ST.slok(~T, t, fr, SC.update(Maybe<&2, T>, vl, n, v)), hx, slok_off(~T, t, fr, vl, n, v, ne_tl(x, n, t, hn), h1))
55
56def flok_off(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +v: Maybe<&2, T>, +hn: {NL.memn(n, xs) == False{} : Bool}, +h: {ST.flok(~T, xs, fr, vl) == True{} : Bool}) -> {ST.flok(~T, xs, fr, SC.update(Maybe<&2, T>, vl, n, v)) == True{} : Bool}:
57 match xs:
58 case Nil{}:
59 {==}
60 case Con{+x, +t}:
61 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))), ST.flok(~T, t, fr, vl), h)
62 +h1 = L.and_right(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))), ST.flok(~T, t, fr, vl), h)
63 +hx = RL.by_eq(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x))), Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_lt(x, fr), Bool.not(z)), ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x), ST.live(T, vl, x), live_other(T, vl, n, v, x, ne_hd(x, n, t, hn))), h0)
64 L.and_intro(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, SC.update(Maybe<&2, T>, vl, n, v), x))), ST.flok(~T, t, fr, SC.update(Maybe<&2, T>, vl, n, v)), hx, flok_off(~T, t, fr, vl, n, v, ne_tl(x, n, t, hn), h1))
65
66# a larger bound
67def slok_mono(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +fr2: Nat, +vl: List<&2, Maybe<&2, T>>, +hle: {Nat.is_le(fr, fr2) == True{} : Bool}, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {ST.slok(~T, xs, fr2, vl) == True{} : Bool}:
68 match xs:
69 case Nil{}:
70 {==}
71 case Con{+x, +t}:
72 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
73 +h1 = L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
74 +hx = L.and_intro(Nat.is_lt(x, fr2), ST.live(T, vl, x), N.lt_le_trans(x, fr, fr2, L.and_left(Nat.is_lt(x, fr), ST.live(T, vl, x), h0), hle), L.and_right(Nat.is_lt(x, fr), ST.live(T, vl, x), h0))
75 L.and_intro(Bool.and(Nat.is_lt(x, fr2), ST.live(T, vl, x)), ST.slok(~T, t, fr2, vl), hx, slok_mono(~T, t, fr, fr2, vl, hle, h1))
76
77def flok_mono(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +fr2: Nat, +vl: List<&2, Maybe<&2, T>>, +hle: {Nat.is_le(fr, fr2) == True{} : Bool}, +h: {ST.flok(~T, xs, fr, vl) == True{} : Bool}) -> {ST.flok(~T, xs, fr2, vl) == True{} : Bool}:
78 match xs:
79 case Nil{}:
80 {==}
81 case Con{+x, +t}:
82 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))), ST.flok(~T, t, fr, vl), h)
83 +h1 = L.and_right(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))), ST.flok(~T, t, fr, vl), h)
84 +hx = L.and_intro(Nat.is_lt(x, fr2), Bool.not(ST.live(T, vl, x)), N.lt_le_trans(x, fr, fr2, L.and_left(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x)), h0), hle), L.and_right(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x)), h0))
85 L.and_intro(Bool.and(Nat.is_lt(x, fr2), Bool.not(ST.live(T, vl, x))), ST.flok(~T, t, fr2, vl), hx, flok_mono(~T, t, fr, fr2, vl, hle, h1))
86
87# a vacant id is on no list of live ids
88def vac_c(-T: Data, +x: Nat, +y: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {ST.live(T, vl, x) == False{} : Bool}, +hy: {ST.live(T, vl, y) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +m: Bool, +ih: {m == False{} : Bool}) -> {Bool.or(c, m) == False{} : Bool}:
89 match c:
90 case True{}:
91 +hy2 = L.subst(Nat, z => {ST.live(T, vl, z) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy)
92 Empty.absurd({Bool.or(True{}, m) == False{} : Bool}, L.true_not_false(ST.live(T, vl, x), hy2, hx))
93 case False{}:
94 ih
95
96def vac_ns(~T: Data, +x: Nat, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {ST.live(T, vl, x) == False{} : Bool}, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {NL.memn(x, xs) == False{} : Bool}:
97 match xs:
98 case Nil{}:
99 {==}
100 case Con{+y, +t}:
101 +h0 = L.and_left(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h)
102 +h1 = L.and_right(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h)
103 vac_c(T, x, y, vl, hx, L.and_right(Nat.is_lt(y, fr), ST.live(T, vl, y), h0), Nat.is_eq(y, x), {==}, NL.memn(x, t), vac_ns(~T, x, t, fr, vl, hx, h1))
104
105# the last id of a (a ++ b live) is off a vacant list
106def lin_vac(~T: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +fl: List<&2, Nat>, +hs: {ST.slok(~T, SC.append(Nat, a, b), fr, vl) == True{} : Bool}, +hf: {ST.flok(~T, fl, fr, vl) == True{} : Bool}) -> {RL.lastin(a, fl) == False{} : Bool}:
107 match a:
108 case Nil{}:
109 {==}
110 case Con{+a0, +t}:
111 +z = NL.lastn(t, a0)
112 +hm = NL.mem_app_l(z, Con{a0, t}, b, NL.lastn_mem(t, a0))
113 RL.live_nf(~T, z, fl, fr, vl, L.and_right(Nat.is_lt(z, fr), ST.live(T, vl, z), RL.slok_mem(~T, z, SC.append(Nat, Con{a0, t}, b), fr, vl, hs, hm)), hf)