proofs/lib/lemmas/proofs/map_route_boolean.bend

bend-collections-laws-containers@1.0.0.0 · 42 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as R
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_routes.bend as D
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_prefix.bend as P
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_string_prefix.bend as Prefix
7
8law leaf_boolean:
9  for +key: String
10  for +position: Nat
11  for +side: Bool
12  for route: {Map.bit(key, position) == (key, side) : String & Bool}
13  {Bool.not(Bool.xor(Inv.bit_value(Map.bit(key, position)), side)) == True{} : Bool}
14def leaf_boolean(key, position, side, route):
15  %Equal.sym(String & Bool, Map.bit(key, position), (key, side), route) : {Bool.not(Bool.xor(Inv.bit_value(_), side)) == True{} : Bool}
16  Equal.cong(Bool, Bool, Bool.not, Bool.xor(side, side), False{}, Prefix.xor_self(side))
17
18law routed_boolean:
19  for -V: Data
20  for tree: Map<&2, V>
21  for +position: Nat
22  for +side: Bool
23  for route: R.routed(V, tree, position, side)
24  {Inv.routed(V, tree, position, side) == True{} : Bool}
25def routed_boolean(V, tree, position, side, route):
26  match tree:
27    case MTip{}: {==}
28    case MLeaf{key, value}: leaf_boolean(key, position, side, route)
29    case MNode{p, +lo, +hi}:
30      (left, right) = route
31      P.conjunction(Inv.routed(V, lo, position, side), Inv.routed(V, hi, position, side), routed_boolean(V, lo, position, side, left), routed_boolean(V, hi, position, side, right))
32
33law deletion_preserves:
34  for -V: Data
35  for +tree: Map<&2, V>
36  for +key: String
37  for +position: Nat
38  for +side: Bool
39  for route: {Inv.routed(V, tree, position, side) == True{} : Bool}
40  {Inv.routed(V, Map.del(&2, V, tree, key), position, side) == True{} : Bool}
41def deletion_preserves(V, tree, key, position, side, route):
42  routed_boolean(V, Map.del(&2, V, tree, key), position, side, D.preserves_routing(V, tree, key, position, side, R.routed_certificate(V, tree, position, side, route)))