1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/hash_table.bend as S 7 import ../../../spec/containers/lru.bend as SP 8 import ../../../src/math/u64.bend as W 9 import ../hash_table/keys.bend as K 10 import ../hash_table/state.bend as HT 11 import ./state.bend as ST 12 import ../../lib/nat_list.bend as NL 13 14 # List algebra for the recency list and the model's keys: membership, 15 # duplicate-freedom and the per-slot predicates over appends. 16 17 18 # ---- Bool algebra ---- 19 20 21 22 23 24 # not (x or y) and (z and not w) == (not x and z) and not (y or w) 25 26 27 # ---- slot lists ---- 28 29 30 31 32 # ---- key lists ---- 33 34 35 def mem_app_s(+x: String, +a: List<&2, String>, +b: List<&2, String>) -> {S.mem(x, SC.append(String, a, b)) == Bool.or(S.mem(x, a), S.mem(x, b)) : Bool}: 36 match a: 37 case Nil{}: 38 {==} 39 case Con{+h, +t}: 40 Equal.trans(Bool, Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, b))), Bool.or(S.str_eq(h, x), Bool.or(S.mem(x, t), S.mem(x, b))), Bool.or(Bool.or(S.str_eq(h, x), S.mem(x, t)), S.mem(x, b)), Equal.cong(Bool, Bool, z => Bool.or(S.str_eq(h, x), z), S.mem(x, SC.append(String, t, b)), Bool.or(S.mem(x, t), S.mem(x, b)), mem_app_s(x, t, b)), NL.or_assoc(S.str_eq(h, x), S.mem(x, t), S.mem(x, b))) 41 42 def mem_mid_s(+x: String, +a: List<&2, String>, +s: String, +b: List<&2, String>) -> {S.mem(x, SC.append(String, a, Con{s, b})) == Bool.or(S.mem(x, SC.append(String, a, b)), S.str_eq(s, x)) : Bool}: 43 match a: 44 case Nil{}: 45 NL.or_comm(S.str_eq(s, x), S.mem(x, b)) 46 case Con{+h, +t}: 47 Equal.trans(Bool, Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, Con{s, b}))), Bool.or(S.str_eq(h, x), Bool.or(S.mem(x, SC.append(String, t, b)), S.str_eq(s, x))), Bool.or(Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, b))), S.str_eq(s, x)), Equal.cong(Bool, Bool, z => Bool.or(S.str_eq(h, x), z), S.mem(x, SC.append(String, t, Con{s, b})), Bool.or(S.mem(x, SC.append(String, t, b)), S.str_eq(s, x)), mem_mid_s(x, t, s, b)), NL.or_assoc(S.str_eq(h, x), S.mem(x, SC.append(String, t, b)), S.str_eq(s, x))) 48 49 def nd_mid_s(+a: List<&2, String>, +s: String, +b: List<&2, String>) -> {S.nodup(SC.append(String, a, Con{s, b})) == Bool.and(S.nodup(SC.append(String, a, b)), Bool.not(S.mem(s, SC.append(String, a, b)))) : Bool}: 50 match a: 51 case Nil{}: 52 NL.and_comm(Bool.not(S.mem(s, b)), S.nodup(b)) 53 case Con{+h, +t}: 54 +X = S.mem(h, SC.append(String, t, b)) 55 +Z = S.nodup(SC.append(String, t, b)) 56 +Wm = S.mem(s, SC.append(String, t, b)) 57 +e1 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(z), S.nodup(SC.append(String, t, Con{s, b}))), S.mem(h, SC.append(String, t, Con{s, b})), Bool.or(X, S.str_eq(s, h)), mem_mid_s(h, t, s, b)) 58 +e2 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), z), S.nodup(SC.append(String, t, Con{s, b})), Bool.and(Z, Bool.not(Wm)), nd_mid_s(t, s, b)) 59 +e3 = NL.bt_mid(X, S.str_eq(s, h), Z, Wm) 60 +e4 = Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(z, Wm))), S.str_eq(s, h), S.str_eq(h, s), K.str_sym(s, h)) 61 Equal.trans(Bool, S.nodup(SC.append(String, Con{h, t}, Con{s, b})), Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), S.nodup(SC.append(String, t, Con{s, b}))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e1, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), S.nodup(SC.append(String, t, Con{s, b}))), Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e2, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(s, h), Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e3, e4))) 62 63 # ---- slot predicates ---- 64 65 def sall_app(~V: Data, +p: ST.SP1, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {ST.sall(~V, p, SC.append(Nat, a, b)) == Bool.and(ST.sall(~V, p, a), ST.sall(~V, p, b)) : Bool}: 66 match a: 67 case Nil{}: 68 {==} 69 case Con{+h, +t}: 70 Equal.trans(Bool, Bool.and(ST.sev(~V, p, h), ST.sall(~V, p, SC.append(Nat, t, b))), Bool.and(ST.sev(~V, p, h), Bool.and(ST.sall(~V, p, t), ST.sall(~V, p, b))), Bool.and(Bool.and(ST.sev(~V, p, h), ST.sall(~V, p, t)), ST.sall(~V, p, b)), Equal.cong(Bool, Bool, z => Bool.and(ST.sev(~V, p, h), z), ST.sall(~V, p, SC.append(Nat, t, b)), Bool.and(ST.sall(~V, p, t), ST.sall(~V, p, b)), sall_app(~V, p, t, b)), NL.and_assoc(ST.sev(~V, p, h), ST.sall(~V, p, t), ST.sall(~V, p, b))) 71 72 def sa_c(~V: Data, +p: ST.SP1, +x: Nat, +s0: Nat, +t: List<&2, Nat>, +h: {Bool.and(ST.sev(~V, p, s0), ST.sall(~V, p, t)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hs: {ST.sall(~V, p, t) == True{} : Bool} -> @hm2: {NL.memn(x, t) == True{} : Bool} -> {ST.sev(~V, p, x) == True{} : Bool}) -> {ST.sev(~V, p, x) == True{} : Bool}: 73 match c: 74 case True{}: 75 L.subst(Nat, z => {ST.sev(~V, p, z) == True{} : Bool}, s0, x, N.eq_from_is_eq(s0, x, hc), L.and_left(ST.sev(~V, p, s0), ST.sall(~V, p, t), h)) 76 case False{}: 77 rec(L.and_right(ST.sev(~V, p, s0), ST.sall(~V, p, t), h), hm) 78 79 # p holds at a member 80 def sall_mem(~V: Data, +p: ST.SP1, +x: Nat, +xs: List<&2, Nat>, +h: {ST.sall(~V, p, xs) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {ST.sev(~V, p, x) == True{} : Bool}: 81 match xs: 82 case Nil{}: 83 Empty.absurd({ST.sev(~V, p, x) == True{} : Bool}, L.false_true(hm)) 84 case Con{+s0, +t}: 85 sa_c(~V, p, x, s0, t, h, Nat.is_eq(s0, x), {==}, hm, hs => hm2 => sall_mem(~V, p, x, t, hs, hm2)) 86 87 # ---- the model's entries ---- 88 89 90 def es_app(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {ST.es(~V, ll, kl, el, SC.append(Nat, a, b)) == SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)) : List<&2, SP.Ent>}: 91 match a: 92 case Nil{}: 93 {==} 94 case Con{+h, +t}: 95 +x = ST.sent_m(~V, ll, kl, h, HT.nthm(~V, el, h)) 96 Equal.trans(List<&2, SP.Ent>, SC.append(SP.Ent, x, ST.es(~V, ll, kl, el, SC.append(Nat, t, b))), SC.append(SP.Ent, x, SC.append(SP.Ent, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))), SC.append(SP.Ent, SC.append(SP.Ent, x, ST.es(~V, ll, kl, el, t)), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, z => SC.append(SP.Ent, x, z), ST.es(~V, ll, kl, el, SC.append(Nat, t, b)), SC.append(SP.Ent, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b)), es_app(~V, ll, kl, el, t, b)), Equal.sym(List<&2, SP.Ent>, SC.append(SP.Ent, SC.append(SP.Ent, x, ST.es(~V, ll, kl, el, t)), ST.es(~V, ll, kl, el, b)), SC.append(SP.Ent, x, SC.append(SP.Ent, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))), LL.append_assoc(SP.Ent, x, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b)))) 97 98 def keys_app(~V: Data, +a: List<&2, SP.Ent>, +b: List<&2, SP.Ent>) -> {SP.keys_of(~V, SC.append(SP.Ent, a, b)) == SC.append(String, SP.keys_of(~V, a), SP.keys_of(~V, b)) : List<&2, String>}: 99 match a: 100 case Nil{}: 101 {==} 102 case Con{SP.LE{+k, +v, +t, +d}, +r}: 103 LL.cons_cong(String, k, SP.keys_of(~V, SC.append(SP.Ent, r, b)), SC.append(String, SP.keys_of(~V, r), SP.keys_of(~V, b)), keys_app(~V, r, b)) 104 105 def snoc_app(~V: Data, +a: List<&2, SP.Ent>, +e: SP.Ent) -> {SP.snoc(~V, a, e) == SC.append(SP.Ent, a, Con{e, Nil{}}) : List<&2, SP.Ent>}: 106 match a: 107 case Nil{}: 108 {==} 109 case Con{+h, +t}: 110 LL.cons_cong(SP.Ent, h, SP.snoc(~V, t, e), SC.append(SP.Ent, t, Con{e, Nil{}}), snoc_app(~V, t, e)) 111 112 # no entry of a has key 113 def enk(~V: Data, a: List<&2, SP.Ent>, +key: String) -> Bool: 114 match a: 115 case Nil{}: 116 True{} 117 case Con{SP.LE{+k, v, t, d}, r}: 118 Bool.and(Bool.not(S.str_eq(k, key)), enk(~V, r, key)) 119 120 def drop_c(~V: Data, +k: String, +v: V, +t: U32, +d: W.U64, +r: List<&2, SP.Ent>, +b: List<&2, SP.Ent>, +key: String, +c: Bool, +hc: {S.str_eq(k, key) == c : Bool}, +h: {Bool.not(c) == True{} : Bool}, +ih: {SP.drop(~V, SC.append(SP.Ent, r, b), key) == SC.append(SP.Ent, r, SP.drop(~V, b, key)) : List<&2, SP.Ent>}) -> {SP.drop(~V, SC.append(SP.Ent, Con{SP.LE{k, v, t, d}, r}, b), key) == SC.append(SP.Ent, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent>}: 121 match c: 122 case True{}: 123 Empty.absurd({SP.drop(~V, SC.append(SP.Ent, Con{SP.LE{k, v, t, d}, r}, b), key) == SC.append(SP.Ent, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent>}, L.false_true(h)) 124 case False{}: 125 L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent>, z, SC.append(SP.Ent, r, b), Con{SP.LE{k, v, t, d}, SP.drop(~V, SC.append(SP.Ent, r, b), key)}) == SC.append(SP.Ent, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent>}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, hc), LL.cons_cong(SP.Ent, SP.LE{k, v, t, d}, SP.drop(~V, SC.append(SP.Ent, r, b), key), SC.append(SP.Ent, r, SP.drop(~V, b, key)), ih)) 126 127 # drop skips a prefix without key 128 def drop_app(~V: Data, +a: List<&2, SP.Ent>, +b: List<&2, SP.Ent>, +key: String, +h: {enk(~V, a, key) == True{} : Bool}) -> {SP.drop(~V, SC.append(SP.Ent, a, b), key) == SC.append(SP.Ent, a, SP.drop(~V, b, key)) : List<&2, SP.Ent>}: 129 match a: 130 case Nil{}: 131 {==} 132 case Con{SP.LE{+k, +v, +t, +d}, +r}: 133 drop_c(~V, k, v, t, d, r, b, key, S.str_eq(k, key), {==}, L.and_left(Bool.not(S.str_eq(k, key)), enk(~V, r, key), h), drop_app(~V, r, b, key, L.and_right(Bool.not(S.str_eq(k, key)), enk(~V, r, key), h))) 134 135 # ---- splitting a duplicate-free list ---- 136 137 138 139 140 141 142 143 144 145 # a member of x is not in a 146 147 148 # a member of a is not in x