proofs/containers/stack/proof.bend source

proofs/containers/stack/proof.bend on the hub · documented module

import Baseimport ../../../src/containers/stack.bend as Dimport ../../../spec/containers/stack.bend as Simport ../../../spec/lib/common.bend as Cimport ../../../src/containers/types/stack.bend as Eimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../../spec/lib/sequence.bend as Vimport ../../lib/sequence.bend as VL# Universal one-step refinement, including cached count preservation and# empty errors. Concrete instances in STACK_COMPONENT_PROOF.bend.def real(~T: Data, +xs: List<&2, T>) -> D.Stack<T>:  D.ST{xs, C.length(T, xs)}def lift(~T: Data, r: List<&2, T> & E.Obs<T>) -> D.Stack<T> & E.Obs<T>:  (xs, obs) = r  (real(~T, xs), obs)def step_correct(~T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> {D.step(~T, real(~T, xs), op) == lift(~T, S.step(T, xs, op)) : D.Stack<T> & E.Obs<T>}:  match xs op:    case Nil{} E.Push{v}:      {==}    case Nil{} E.Length{}:      {==}    case Nil{} E.ToList{}:      {==}    case Nil{} E.Peek{}:      {==}    case Nil{} E.Pop{}:      {==}    case Con{+x, +tail} E.Push{v}:      {==}    case Con{+x, +tail} E.Length{}:      {==}    case Con{+x, +tail} E.ToList{}:      {==}    case Con{+x, +tail} E.Peek{}:      {==}    case Con{+x, +tail} E.Pop{}:      Equal.cong(Nat, D.Stack<T> & E.Obs<T>, n => (D.ST{tail, n}, E.OItem{Done{x}}), Nat.sub(C.length(T, tail), 0n), C.length(T, tail), N.sub_zero(C.length(T, tail)))def constructor(~T: Data) -> {D.new(~T) == real(~T, Nil{}) : D.Stack<T>}:  {==}# ==== the contract of stack (stated in spec/containers/stack.bend) ====================# ---- the implementation ----def impl(~T: Data, +xs: List<&2, T>, +op: E.Op<T>, -Post: (D.Stack<T> & E.Obs<T>) -> Type, pf: Post(lift(~T, S.step(T, xs, op)))) -> Post(D.step(~T, real(~T, xs), op)):  L.subst(D.Stack<T> & E.Obs<T>, Post, lift(~T, S.step(T, xs, op)), D.step(~T, real(~T, xs), op), Equal.sym(D.Stack<T> & E.Obs<T>, D.step(~T, real(~T, xs), op), lift(~T, S.step(T, xs, op)), step_correct(~T, xs, op)), pf)# ---- Length, iteration ----def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}# ---- Empty_Vector ----def new_empty(-T: Data) -> S.Empty_Vector.new_empty(T):  {==}def new_impl(~T: Data) -> {D.new(~T) == real(~T, Nil{}) : D.Stack<T>}:  constructor(~T)# ---- Prepend: Length + 1, Element (First) = New_Item, Range_Shifted (Old, New, First, Last'Old, 1) ----def push_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_length(T, xs, v):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def push_first(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_first(T, xs, v):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def push_is(-T: Data, +xs: List<&2, T>, +v: T) -> {S.nx(T, xs, E.Push{v}) == Con{v, xs} : List<&2, T>}:  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def push_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_shifted(T, xs, v):  L.subst(List<&2, T>, z => V.RangeShifted(T, xs, z, 0n, C.length(T, xs), 1n), Con{v, xs}, S.nx(T, xs, E.Push{v}), Equal.sym(List<&2, T>, S.nx(T, xs, E.Push{v}), Con{v, xs}, push_is(T, xs, v)), VL.cons_shifted(T, xs, v))# ---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); pop returns First_Element'Old ----def pop_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_length(T, h, t):  {==}def pop_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_shifted(T, h, t):  VL.tail_shifted(T, h, t)def pop_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_result(T, h, t):  {==}def pop_empty(-T: Data) -> S.Delete_First.pop_empty(T):  {==}# ---- First_Element: Element (Model, First); nothing changes ----def peek_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_first(T, h, t):  ({==}, {==})def peek_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_frame(T, xs):  match xs:    case Nil{}:      {==}    case Con{h, t}:      {==}def peek_empty(-T: Data) -> S.First_Element.peek_empty(T):  {==}