1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/doubly_linked_list.bend as S
6	import ./state.bend as ST
7	import ./rel.bend as RL
8	import ./vals.bend as VA
9	import ../../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	
15	def 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	
18	def 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	
21	def 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
29	def 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	
39	def 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	
42	def 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
46	def 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	
56	def 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
67	def 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	
77	def 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
88	def 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	
96	def 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
106	def 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)