1 import Base 2 import ./map_bridge.bend as MB 3 import ./string_compare.bend as N 4 import ./map_insert.bend as I 5 import ./map_routing.bend as R 6 import ./invariants.bend as Inv 7 8 # Deletion preserves every existing query/prefix constraint. 9 # This law unfolds native pop, including collapsing an empty child. 10 law conjunction: 11 for a: Bool 12 for b: Bool 13 for left: {a == True{} : Bool} 14 for right: {b == True{} : Bool} 15 {a && b == True{} : Bool} 16 def conjunction(a, b, left, right): 17 %Equal.sym(Bool, a, True{}, left) : {_ && b == True{} : Bool} 18 right 19 20 law low: 21 for -V: Data 22 for p: Nat 23 for +hi: Map<&2, V> 24 for r: Map<&2, V> & Maybe<&2, V> 25 for +query: String 26 for +limit: Nat 27 for left: {Inv.prefix_against(V, query, Map.del.fin(&2, V, r), limit) == True{} : Bool} 28 for right: {Inv.prefix_against(V, query, hi, limit) == True{} : Bool} 29 {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), limit) == True{} : Bool} 30 def low(V, p, hi, r, query, limit, left, right): 31 match r: 32 case Tuple{tree, found}: 33 match tree: 34 case MTip{}: 35 right 36 case MLeaf{+k, +v}: 37 conjunction(Inv.same_prefix(query, k, limit), Inv.prefix_against(V, query, hi, limit), left, right) 38 case MNode{+q, +lo, +other}: 39 conjunction(Inv.prefix_against(V, query, MNode{q, lo, other}, limit), Inv.prefix_against(V, query, hi, limit), left, right) 40 41 law high: 42 for -V: Data 43 for p: Nat 44 for +lo: Map<&2, V> 45 for r: Map<&2, V> & Maybe<&2, V> 46 for +query: String 47 for +limit: Nat 48 for left: {Inv.prefix_against(V, query, lo, limit) == True{} : Bool} 49 for right: {Inv.prefix_against(V, query, Map.del.fin(&2, V, r), limit) == True{} : Bool} 50 {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), limit) == True{} : Bool} 51 def high(V, p, lo, r, query, limit, left, right): 52 match r: 53 case Tuple{tree, found}: 54 match tree: 55 case MTip{}: 56 left 57 case MLeaf{+k, +v}: 58 conjunction(Inv.prefix_against(V, query, lo, limit), Inv.same_prefix(query, k, limit), left, right) 59 case MNode{+q, +other, +hi}: 60 conjunction(Inv.prefix_against(V, query, lo, limit), Inv.prefix_against(V, query, MNode{q, other, hi}, limit), left, right) 61 62 law leaf: 63 for -V: Data 64 for value: V 65 for key: String 66 for stored: String 67 for c: Cmp 68 for query: String 69 for limit: Nat 70 for route: {Inv.same_prefix(query, stored, limit) == True{} : Bool} 71 {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, ((key, stored), c))), limit) == True{} : Bool} 72 def leaf(V, value, key, stored, c, query, limit, route): 73 match c: 74 case LT{}: 75 route 76 case EQ{}: 77 {==} 78 case GT{}: 79 route 80 81 law branch: 82 for -V: Data 83 for +lo: Map<&2, V> 84 for +hi: Map<&2, V> 85 for +p: Nat 86 for +key: String 87 for bit: Bool 88 for e: {Map.bit(key, p) == (key, bit) : String & Bool} 89 for +query: String 90 for +limit: Nat 91 for left: {Inv.prefix_against(V, query, lo, limit) == True{} : Bool} 92 for right: {Inv.prefix_against(V, query, hi, limit) == True{} : Bool} 93 for lp: {Inv.prefix_against(V, query, lo, limit) == True{} : Bool} -> {Inv.prefix_against(V, query, Map.del(&2, V, lo, key), limit) == True{} : Bool} 94 for hp: {Inv.prefix_against(V, query, hi, limit) == True{} : Bool} -> {Inv.prefix_against(V, query, Map.del(&2, V, hi, key), limit) == True{} : Bool} 95 {Inv.prefix_against(V, query, Map.del(&2, V, MNode{p, lo, hi}, key), limit) == True{} : Bool} 96 def branch(V, lo, hi, p, key, bit, e, query, limit, left, right, lp, hp): 97 match bit: 98 case False{}: 99 %Equal.sym(Map<&2, V> & Maybe<&2, V>, Map.pop(&2, V, MNode{p, lo, hi}, key), MB.pop_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, V, p, lo, hi, key)) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, _), limit) == True{} : Bool} 100 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), limit) == True{} : Bool} 101 low(V, p, hi, Map.pop(&2, V, lo, key), query, limit, lp(left), right) 102 case True{}: 103 %Equal.sym(Map<&2, V> & Maybe<&2, V>, Map.pop(&2, V, MNode{p, lo, hi}, key), MB.pop_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, V, p, lo, hi, key)) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, _), limit) == True{} : Bool} 104 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), limit) == True{} : Bool} 105 high(V, p, lo, Map.pop(&2, V, hi, key), query, limit, left, hp(right)) 106 107 law preserves_prefix_against: 108 for -V: Data 109 for tree: Map<&2, V> 110 for +key: String 111 for +query: String 112 for +limit: Nat 113 for +routes: {Inv.prefix_against(V, query, tree, limit) == True{} : Bool} 114 {Inv.prefix_against(V, query, Map.del(&2, V, tree, key), limit) == True{} : Bool} 115 def preserves_prefix_against(V, tree, key, query, limit, routes): 116 match tree: 117 case MTip{}: 118 {==} 119 case MLeaf{+stored, +value}: 120 %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), N.comparison_tag(String, String.cmp(key, stored))), N.string_comparison_shape(key, stored)) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, _)), limit) == True{} : Bool} 121 leaf(V, value, key, stored, N.comparison_tag(String, String.cmp(key, stored)), query, limit, routes) 122 case MNode{+p, +lo, +hi}: 123 left = R.and_left(Inv.prefix_against(V, query, lo, limit), Inv.prefix_against(V, query, hi, limit), routes) 124 right = R.and_right(Inv.prefix_against(V, query, lo, limit), Inv.prefix_against(V, query, hi, limit), routes) 125 branch(V, lo, hi, p, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), query, limit, left, right, r => preserves_prefix_against(V, lo, key, query, limit, r), r => preserves_prefix_against(V, hi, key, query, limit, r)) 126