law primitive_write_read

bendtorch-core@0.1.0.0 · src/storage/LAWS.bend:57

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

57law primitive_write_read:
58  for -T: Data
59  for +d: Nat
60  for array: Array<T>
61  for +i: U32
62  for +value: T
63  for valid: Model.Balanced(T, d, array)
64  {Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)) == Some{value} : Maybe<&2, T>}