proofs/containers/dlist_iterator/proof.bend
bend-collections-laws-containers@1.0.0.0 · 106 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/dlist_iterator.bend as I
3import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
5import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
6import bend-collections-laws-containers@1.0.0.0/spec/containers/dlist_iterator.bend as S
7
8# Component laws over the actual cursor implementation. These are not a full
9# sequence-refinement proof for all edits/traces or the underlying arena.
10def finish_owns(s: D.DList<U32>, n: U32, last: U32, f: Bool, i: Nat) -> {I.finish(~U32, I.IT{s, n, last, f, i}) == s : D.DList<U32>}:
11 {==}
12
13def next_exhausted(s: D.DList<U32>, +last: U32, +f: Bool, +i: Nat) -> {I.next(~U32, I.IT{s, 0, last, f, i}) == (I.IT{s, 0, last, f, i}, Fail{I.Exhausted{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, U32>}:
14 match s:
15 case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
16 {==}
17
18def set_requires_current(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat, x: U32) -> {I.set(~U32, I.IT{s, n, 0, f, i}, x) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
19 {==}
20
21def remove_requires_current(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat) -> {I.remove(~U32, I.IT{s, n, 0, f, i}) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
22 match s:
23 case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
24 {==}
25
26def has_next_state(s: D.DList<U32>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_next(~U32, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, I.present(n)) : I.Iterator<U32> & Bool}:
27 {==}
28
29def has_previous_state(s: D.DList<U32>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_previous(~U32, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, Nat.is_lt(0n, i)) : I.Iterator<U32> & Bool}:
30 {==}
31
32def added_clears_current(s: D.DList<U32>, +n: U32, last: U32, +f: Bool, +i: Nat, h: E.Handle) -> {I.added(~U32, n, last, f, i, (s, Done{h})) == (I.IT{s, n, 0, f, 1n+i}, Done{Unit{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
33 {==}
34
35def removed_forward(s: D.DList<U32>, n: U32, last: U32, +i: Nat, +after: U32, x: U32) -> {I.removed(~U32, n, last, True{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, True{}, Nat.sub(i, 1n)}, Done{Unit{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
36 {==}
37
38def removed_backward(s: D.DList<U32>, n: U32, last: U32, +i: Nat, +after: U32, x: U32) -> {I.removed(~U32, n, last, False{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, False{}, i}, Done{Unit{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
39 {==}
40
41def finish_owns_string(s: D.DList<String>, n: U32, last: U32, f: Bool, i: Nat) -> {I.finish(~String, I.IT{s, n, last, f, i}) == s : D.DList<String>}:
42 {==}
43
44def next_exhausted_string(s: D.DList<String>, +last: U32, +f: Bool, +i: Nat) -> {I.next(~String, I.IT{s, 0, last, f, i}) == (I.IT{s, 0, last, f, i}, Fail{I.Exhausted{}}) : I.Iterator<String> & Result<&2, &2, I.Error, String>}:
45 match s:
46 case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
47 {==}
48
49def set_requires_current_string(s: D.DList<String>, +n: U32, +f: Bool, +i: Nat, x: String) -> {I.set(~String, I.IT{s, n, 0, f, i}, x) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
50 {==}
51
52def remove_requires_current_string(s: D.DList<String>, +n: U32, +f: Bool, +i: Nat) -> {I.remove(~String, I.IT{s, n, 0, f, i}) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
53 match s:
54 case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
55 {==}
56
57def has_next_state_string(s: D.DList<String>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_next(~String, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, I.present(n)) : I.Iterator<String> & Bool}:
58 {==}
59
60def has_previous_state_string(s: D.DList<String>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_previous(~String, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, Nat.is_lt(0n, i)) : I.Iterator<String> & Bool}:
61 {==}
62
63def added_clears_current_string(s: D.DList<String>, +n: U32, last: U32, +f: Bool, +i: Nat, h: E.Handle) -> {I.added(~String, n, last, f, i, (s, Done{h})) == (I.IT{s, n, 0, f, 1n+i}, Done{Unit{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
64 {==}
65
66def removed_forward_string(s: D.DList<String>, n: U32, last: U32, +i: Nat, +after: U32, x: String) -> {I.removed(~String, n, last, True{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, True{}, Nat.sub(i, 1n)}, Done{Unit{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
67 {==}
68
69def removed_backward_string(s: D.DList<String>, n: U32, last: U32, +i: Nat, +after: U32, x: String) -> {I.removed(~String, n, last, False{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, False{}, i}, Done{Unit{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
70 {==}
71
72# The end-gap insertion is exactly the public DLL append, including capacity
73# growth, free-slot reuse, and generation bookkeeping. This is an algorithm
74# bridge, not merely an equality with a model that invokes the iterator.
75def end_gap_is_append(s: D.DList<U32>, x: U32) -> {I.cursor_insert_gap(~U32, s, 0, x) == I.insert_gap_result(~U32, D.push_back(~U32, s, x)) : D.DList<U32> & Result<&2, &2, E.Error, E.Handle>}:
76 match s:
77 case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
78 {==}
79
80def end_gap_is_append_string(s: D.DList<String>, x: String) -> {I.cursor_insert_gap(~String, s, 0, x) == I.insert_gap_result(~String, D.push_back(~String, s, x)) : D.DList<String> & Result<&2, &2, E.Error, E.Handle>}:
81 match s:
82 case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
83 {==}
84
85def move_forward_cursor(n: U32, last: U32, f: Bool, +i: Nat, +h: U32, +after: U32, +x: U32) -> {I.move_meta(~U32, n, last, f, i, h, after, True{}, Done{x}) == I.M{after, h, True{}, 1n+i, Done{x}} : I.Move<U32>}:
86 {==}
87
88def move_backward_cursor(n: U32, last: U32, f: Bool, +i: Nat, +h: U32, +x: U32) -> {I.move_meta(~U32, n, last, f, i, h, h, False{}, Done{x}) == I.M{h, h, False{}, Nat.sub(i, 1n), Done{x}} : I.Move<U32>}:
89 {==}
90
91def failed_move_preserves_cursor(+n: U32, +last: U32, +f: Bool, +i: Nat, h: U32, after: U32, forward: Bool, +e: I.Error) -> {I.move_meta(~U32, n, last, f, i, h, after, forward, Fail{e}) == I.M{n, last, f, i, Fail{e}} : I.Move<U32>}:
92 {==}
93
94# ==== the contract of dlist_iterator (stated in spec/containers/dlist_iterator.bend) ====================
95
96def has_element(s: D.DList<U32>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_next(~U32, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, I.present(n)) : I.Iterator<U32> & Bool}:
97 has_next_state(s, n, last, f, i)
98
99def next_at_end(s: D.DList<U32>, +last: U32, +f: Bool, +i: Nat) -> {I.next(~U32, I.IT{s, 0, last, f, i}) == (I.IT{s, 0, last, f, i}, Fail{I.Exhausted{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, U32>}:
100 next_exhausted(s, last, f, i)
101
102def replace_pre(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat, x: U32) -> {I.set(~U32, I.IT{s, n, 0, f, i}, x) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
103 set_requires_current(s, n, f, i, x)
104
105def delete_pre(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat) -> {I.remove(~U32, I.IT{s, n, 0, f, i}) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
106 remove_requires_current(s, n, f, i)