proofs/containers/dlist_iterator/proof.bend source
proofs/containers/dlist_iterator/proof.bend on the hub · documented module
import Baseimport ../../../src/containers/dlist_iterator.bend as Iimport ../../../src/containers/doubly_linked_list.bend as Dimport ../../../src/containers/types/doubly_linked_list.bend as Eimport ../../../src/containers/internal/dlist_storage.bend as Rimport ../../../spec/containers/dlist_iterator.bend as S# Component laws over the actual cursor implementation. These are not a full# sequence-refinement proof for all edits/traces or the underlying arena.def 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>}: {==}def 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>}: match s: case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}: {==}def 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>}: {==}def 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>}: match s: case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}: {==}def 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}: {==}def 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}: {==}def 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>}: {==}def 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>}: {==}def 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>}: {==}def 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>}: {==}def 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>}: match s: case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}: {==}def 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>}: {==}def 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>}: match s: case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}: {==}def 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}: {==}def 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}: {==}def 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>}: {==}def 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>}: {==}def 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>}: {==}# The end-gap insertion is exactly the public DLL append, including capacity# growth, free-slot reuse, and generation bookkeeping. This is an algorithm# bridge, not merely an equality with a model that invokes the iterator.def 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>}: match s: case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}: {==}def 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>}: match s: case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}: {==}def 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>}: {==}def 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>}: {==}def 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>}: {==}# ==== the contract of dlist_iterator (stated in spec/containers/dlist_iterator.bend) ====================def 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}: has_next_state(s, n, last, f, i)def 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>}: next_exhausted(s, last, f, i)def 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>}: set_requires_current(s, n, f, i, x)def 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>}: remove_requires_current(s, n, f, i)