LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./protocol.bend as Pimport ./observe.bend as Oimport ./cases.bend as Cimport ./model.bend as Mimport ./main.bend as S# Universal public observations; no preconditions or uninhabited parameters.law first:  for +name: String  {O.run([P.Intern{name},P.Resolve{0},P.Length{}],1) ==   [P.Observed{P.Id{0},1,1,[name]},P.Observed{P.Name{name},1,1,[name]},P.Observed{P.Number{1},1,1,[name]}] : List<&2,P.Observation>}law zero_limit:  for +name: String  {O.run([P.Intern{name},P.Find{name},P.Resolve{0}],0) ==   [P.Observed{P.Full{},0,0,[]},P.Observed{P.Missing{},0,0,[]},P.Observed{P.Invalid{},0,0,[]}] : List<&2,P.Observation>}law empty_find:  for name: String  {O.run([P.Find{name}],3) == [P.Observed{P.Missing{},0,3,[]}] : List<&2,P.Observation>}# Concrete normalization/refinement witnesses; not universal refinement proofs.law repeat_preserves:  {C.check(C.repeat(),4) == True{} : Bool}law full_preserves:  {C.check(C.full(),1) == True{} : Bool}law unicode_exact:  {C.check(C.unicode(),6) == True{} : Bool}law default_limit:  {O.trace([P.Length{},P.Limit{},P.Resolve{4294967295}],S.Table.new()) ==   [P.Observed{P.Number{0},0,16777216,[]},P.Observed{P.Number{16777216},0,16777216,[]},P.Observed{P.Invalid{},0,16777216,[]}] : List<&2,P.Observation>}law clamp_limit:  {O.run([P.Limit{}],4294967295) == [P.Observed{P.Number{16777216},0,16777216,[]}] : List<&2,P.Observation>}