1	import Base
2	import ./map_bridge.bend as MB
3	import ./invariants.bend as Inv
4	import ./string_compare.bend as N
5	import ./map_insert.bend as I
6	import ./map_difference_order.bend as O
7	import ./map_string_prefix.bend as Prefix
8	import ./recency_bounds.bend as Bounds
9	import ./map_critbit_parts.bend as Parts
10	
11	law strict_transitive:
12	  for +a: Nat
13	  for +b: Nat
14	  for +c: Nat
15	  for ab: {Nat.is_lt(a, b) == True{} : Bool}
16	  for bc: {Nat.is_lt(b, c) == True{} : Bool}
17	  {Nat.is_lt(a, c) == True{} : Bool}
18	def strict_transitive(a, b, c, ab, bc):
19	  Prefix.predecessor_less(a, c, Bounds.le_transitive(1n+a, b, c, O.strict_successor(a, b, ab), O.less_is_le(b, c, bc)))
20	
21	law lower_parent:
22	  for -V: Data
23	  for tree: Map<&2, V>
24	  for +parent: Nat
25	  for +p: Nat
26	  for lower: {Nat.is_lt(parent, p) == True{} : Bool}
27	  for below: {Inv.below(V, tree, p) == True{} : Bool}
28	  {Inv.below(V, tree, parent) == True{} : Bool}
29	def lower_parent(V, tree, parent, p, lower, below):
30	  match tree:
31	    case MTip{}: {==}
32	    case MLeaf{k, v}: {==}
33	    case MNode{q, lo, hi}: strict_transitive(parent, p, q, lower, below)
34	
35	law low:
36	  for -V: Data
37	  for +p: Nat
38	  for +parent: Nat
39	  for hi: Map<&2, V>
40	  for r: Map<&2, V> & Maybe<&2, V>
41	  for lower: {Nat.is_lt(parent, p) == True{} : Bool}
42	  for below: {Inv.below(V, hi, p) == True{} : Bool}
43	  {Inv.below(V, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), parent) == True{} : Bool}
44	def low(V, p, parent, hi, r, lower, below):
45	  match r:
46	    case Tuple{tree, found}:
47	      match tree:
48	        case MTip{}: lower_parent(V, hi, parent, p, lower, below)
49	        case MLeaf{k, v}: lower
50	        case MNode{q, lo, other}: lower
51	
52	law high:
53	  for -V: Data
54	  for +p: Nat
55	  for +parent: Nat
56	  for lo: Map<&2, V>
57	  for r: Map<&2, V> & Maybe<&2, V>
58	  for lower: {Nat.is_lt(parent, p) == True{} : Bool}
59	  for below: {Inv.below(V, lo, p) == True{} : Bool}
60	  {Inv.below(V, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), parent) == True{} : Bool}
61	def high(V, p, parent, lo, r, lower, below):
62	  match r:
63	    case Tuple{tree, found}:
64	      match tree:
65	        case MTip{}: lower_parent(V, lo, parent, p, lower, below)
66	        case MLeaf{k, v}: lower
67	        case MNode{q, other, hi}: lower
68	
69	law leaf:
70	  for -V: Data
71	  for value: V
72	  for key: String
73	  for stored: String
74	  for tag: Cmp
75	  for parent: Nat
76	  {Inv.below(V, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, ((key, stored), tag))), parent) == True{} : Bool}
77	def leaf(V, value, key, stored, tag, parent):
78	  match tag:
79	    case LT{}: {==}
80	    case EQ{}: {==}
81	    case GT{}: {==}
82	
83	law branch:
84	  for -V: Data
85	  for +p: Nat
86	  for +parent: Nat
87	  for +lo: Map<&2, V>
88	  for +hi: Map<&2, V>
89	  for +key: String
90	  for bit: Bool
91	  for route: {Map.bit(key, p) == (key, bit) : String & Bool}
92	  for lower: {Nat.is_lt(parent, p) == True{} : Bool}
93	  for left: {Inv.below(V, lo, p) == True{} : Bool}
94	  for right: {Inv.below(V, hi, p) == True{} : Bool}
95	  {Inv.below(V, Map.del(&2, V, MNode{p, lo, hi}, key), parent) == True{} : Bool}
96	def branch(V, p, parent, lo, hi, key, bit, route, lower, left, right):
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.below(V, Map.del.fin(&2, V, _), parent) == True{} : Bool}
100	      %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), route) : {Inv.below(V, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), parent) == True{} : Bool}
101	      low(V, p, parent, hi, Map.pop(&2, V, lo, key), lower, 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.below(V, Map.del.fin(&2, V, _), parent) == True{} : Bool}
104	      %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), route) : {Inv.below(V, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), parent) == True{} : Bool}
105	      high(V, p, parent, lo, Map.pop(&2, V, hi, key), lower, left)
106	
107	law from_parts:
108	  for -V: Data
109	  for +p: Nat
110	  for +parent: Nat
111	  for +lo: Map<&2, V>
112	  for +hi: Map<&2, V>
113	  for +key: String
114	  for below: {Nat.is_lt(parent, p) == True{} : Bool}
115	  for parts: Parts.NodeFacts(V, p, lo, hi)
116	  {Inv.below(V, Map.del(&2, V, MNode{p, lo, hi}, key), parent) == True{} : Bool}
117	def from_parts(V, p, parent, lo, hi, key, below, parts):
118	  (prefix, ln, hn, lb, hb, lr, hr, lv, hv) = parts
119	  branch(V, p, parent, lo, hi, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), below, lb, hb)
120	
121	# Native deletion either retains the root discriminator or promotes the untouched
122	# sibling. The sibling's ordering is derived from the actual critbit predicate.
123	law preserves_below:
124	  for -V: Data
125	  for tree: Map<&2, V>
126	  for +key: String
127	  for +parent: Nat
128	  for valid: {Inv.critbit(V, tree) == True{} : Bool}
129	  for below: {Inv.below(V, tree, parent) == True{} : Bool}
130	  {Inv.below(V, Map.del(&2, V, tree, key), parent) == True{} : Bool}
131	def preserves_below(V, tree, key, parent, valid, below):
132	  match tree:
133	    case MTip{}: {==}
134	    case MLeaf{+stored, +value}:
135	      %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.below(V, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, _)), parent) == True{} : Bool}
136	      leaf(V, value, key, stored, N.comparison_tag(String, String.cmp(key, stored)), parent)
137	    case MNode{+p, +lo, +hi}:
138	      from_parts(V, p, parent, lo, hi, key, below, Parts.node_parts(V, p, lo, hi, valid))