LAWS.bend open laws/TODOs

raw source on the hub · import 0xf5507d46d06a1a8043dcb1a582194615/LAWS.bend as LAWS

6 imports

import Base
import ./protocol.bend as P
import ./observe.bend as O
import ./cases.bend as C
import ./model.bend as M
import ./main.bend as S

Laws

law first provedin PROOF.bendsource · line 9 · raw

@+name:String -> {0xf5507d46d06a1a8043dcb1a582194615/observe.run([0xf5507d46d06a1a8043dcb1a582194615/protocol.Intern{name}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Resolve{0}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Length{}], 1) == [0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Id{0}, 1, 1, [name]}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Name{name}, 1, 1, [name]}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Number{1}, 1, 1, [name]}] : List<&2, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observation>}

Universal public observations; no preconditions or uninhabited parameters.

law zero_limit provedin PROOF.bendsource · line 14 · raw

@+name:String -> {0xf5507d46d06a1a8043dcb1a582194615/observe.run([0xf5507d46d06a1a8043dcb1a582194615/protocol.Intern{name}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Find{name}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Resolve{0}], 0) == [0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Full{}, 0, 0, []}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Missing{}, 0, 0, []}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Invalid{}, 0, 0, []}] : List<&2, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observation>}

law empty_find provedin PROOF.bendsource · line 19 · raw

@name:String -> {0xf5507d46d06a1a8043dcb1a582194615/observe.run([0xf5507d46d06a1a8043dcb1a582194615/protocol.Find{name}], 3) == [0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Missing{}, 0, 3, []}] : List<&2, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observation>}

law repeat_preserves provedin PROOF.bendsource · line 24 · raw

{0xf5507d46d06a1a8043dcb1a582194615/cases.check(0xf5507d46d06a1a8043dcb1a582194615/cases.repeat, 4) == True{} : Bool}

Concrete normalization/refinement witnesses; not universal refinement proofs.

law full_preserves provedin PROOF.bendsource · line 26 · raw

{0xf5507d46d06a1a8043dcb1a582194615/cases.check(0xf5507d46d06a1a8043dcb1a582194615/cases.full, 1) == True{} : Bool}

law unicode_exact provedin PROOF.bendsource · line 28 · raw

{0xf5507d46d06a1a8043dcb1a582194615/cases.check(0xf5507d46d06a1a8043dcb1a582194615/cases.unicode, 6) == True{} : Bool}

law default_limit provedin PROOF.bendsource · line 30 · raw

{0xf5507d46d06a1a8043dcb1a582194615/observe.trace([0xf5507d46d06a1a8043dcb1a582194615/protocol.Length{}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Limit{}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Resolve{4294967295}], 0xf5507d46d06a1a8043dcb1a582194615/main.Table.new) == [0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Number{0}, 0, 16777216, []}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Number{16777216}, 0, 16777216, []}, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Invalid{}, 0, 16777216, []}] : List<&2, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observation>}

law clamp_limit provedin PROOF.bendsource · line 33 · raw

{0xf5507d46d06a1a8043dcb1a582194615/observe.run([0xf5507d46d06a1a8043dcb1a582194615/protocol.Limit{}], 4294967295) == [0xf5507d46d06a1a8043dcb1a582194615/protocol.Observed{0xf5507d46d06a1a8043dcb1a582194615/protocol.Number{16777216}, 0, 16777216, []}] : List<&2, 0xf5507d46d06a1a8043dcb1a582194615/protocol.Observation>}