~/bend-docscommunity

LAWS.bend open laws/TODOs

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

5 imports
import Base
import ./main.bend as S
import ./types.bend as T
import ./observations.bend as O
import ./proof_observations.bend as P

Laws

law content_identity provedin PROOF.bendsource · line 8 · raw

@id:U32 -> {0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.text(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.new(id, "a😀\nβ")) == Done{"a😀\nβ"} : Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, String>}

Universal over file IDs, fixed inhabited text shapes. Not a theorem for all strings.

law file_identity provedin PROOF.bendsource · line 12 · raw

@id:U32 -> {0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.file(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.new(id, "a😀\nβ")) == Done{id} : Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, U32>}

law empty_content provedin PROOF.bendsource · line 16 · raw

@id:U32 -> {0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.text(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.bounded(id, "", 0)) == Done{""} : Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, String>}

law empty_lines provedin PROOF.bendsource · line 20 · raw

@id:U32 -> {0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.lines(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.new(id, "")) == Done{1} : Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, U32>}

law scalar_units provedin PROOF.bendsource · line 24 · raw

@id:U32 -> {0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.length(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.new(id, "a😀\nβ")) == Done{4} : Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, U32>}

law indexed_value provedin PROOF.bendsource · line 29 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.get("a😀\nβ", 1) == True{} : Bool}

Concrete normalization theorems through public observations and independent model.

law peek_codepoint provedin PROOF.bendsource · line 31 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.peek("a😀", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{7, 1}, Done{Some{'😀'}}) == True{} : Bool}

law bump_restore_content provedin PROOF.bendsource · line 33 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.bump("a😀", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{7, 1}, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{7, 2}, Some{'😀'}) == True{} : Bool}

law eof_fixed_point provedin PROOF.bendsource · line 35 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.bump("a😀", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{7, 2}, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{7, 2}, None{}) == True{} : Bool}

law span_order provedin PROOF.bendsource · line 37 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.extract("a😀\nβ", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Span{7, 1, 3}, Done{"😀\n"}) == True{} : Bool}

law empty_eof_span provedin PROOF.bendsource · line 39 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.span("a😀", 2, 2) == True{} : Bool}

law newline_location provedin PROOF.bendsource · line 41 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.locate("a😀\nβ", 3) == True{} : Bool}

law newline_roundtrip provedin PROOF.bendsource · line 43 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.roundtrip("a😀\nβ", 3) == True{} : Bool}

law cr_is_content provedin PROOF.bendsource · line 45 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.locate("a\rb", 2) == True{} : Bool}

law crlf_location provedin PROOF.bendsource · line 47 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.locate("a\r\nb", 3) == True{} : Bool}

law trailing_line provedin PROOF.bendsource · line 49 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.metadata("\n", 2) == True{} : Bool}

law canonical_location provedin PROOF.bendsource · line 51 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.offset("a\nb", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Location{0, 2}) == True{} : Bool}

law foreign_cursor provedin PROOF.bendsource · line 53 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.restore("a", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{8, 0}, Fail{0x88d5b48c03f82f217d3a2aa0656744f4/types.ForeignFile{}}) == True{} : Bool}

law foreign_span provedin PROOF.bendsource · line 55 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.extract("a", 0x88d5b48c03f82f217d3a2aa0656744f4/types.Span{8, 0, 1}, Fail{0x88d5b48c03f82f217d3a2aa0656744f4/types.ForeignFile{}}) == True{} : Bool}

law rejected_span provedin PROOF.bendsource · line 57 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.span_reject("ab", 2, 1) == True{} : Bool}

law rejected_offset provedin PROOF.bendsource · line 59 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.cursor("a", 2, Fail{0x88d5b48c03f82f217d3a2aa0656744f4/types.Bounds{}}) == True{} : Bool}

law exhausted_limit provedin PROOF.bendsource · line 61 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.rejected(0x88d5b48c03f82f217d3a2aa0656744f4/types.Limit{}, 0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.bounded(7, "abc", 2)) == True{} : Bool}

law invalid_scalar provedin PROOF.bendsource · line 63 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.rejected(0x88d5b48c03f82f217d3a2aa0656744f4/types.InvalidScalar{}, 0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.new(7, "\u{d800}")) == True{} : Bool}

law checked_cursor provedin PROOF.bendsource · line 68 · raw

@s:0x88d5b48c03f82f217d3a2aa0656744f4/main.Source -> @id:U32 -> @i:U32 -> {0x88d5b48c03f82f217d3a2aa0656744f4/main.cursor_if(s, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{id, i}, True{}) == (s, Done{0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{id, i}}) : Pair(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source, Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor>)}

Auxiliary helper normalization over arbitrary source and candidate cursor. Public conditional wrapper theorems below establish bounds and state preservation.

law accepted_cursor provedin PROOF.bendsource · line 74 · raw

@s:0x88d5b48c03f82f217d3a2aa0656744f4/main.Source -> @i:U32 -> @valid:{U32.is_le(i, 0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.size(s)) == True{} : Bool} -> {0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.cursor(s, i) == (s, Done{0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.identity(s), i}}) : Pair(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source, Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor>)}

law rejected_cursor provedin PROOF.bendsource · line 80 · raw

@s:0x88d5b48c03f82f217d3a2aa0656744f4/main.Source -> @i:U32 -> @invalid:{U32.is_le(i, 0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.size(s)) == False{} : Bool} -> {0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.cursor(s, i) == (s, Fail{0x88d5b48c03f82f217d3a2aa0656744f4/types.Bounds{}}) : Pair(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source, Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor>)}

law accepted_span provedin PROOF.bendsource · line 86 · raw

@s:0x88d5b48c03f82f217d3a2aa0656744f4/main.Source -> @a:U32 -> @b:U32 -> @valid:{Bool.and(U32.is_le(a, b), U32.is_le(b, 0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.size(s))) == True{} : Bool} -> {0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.span(s, a, b) == (s, Done{0x88d5b48c03f82f217d3a2aa0656744f4/types.Span{0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.identity(s), a, b}}) : Pair(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source, Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Span>)}

law rejected_span_universal provedin PROOF.bendsource · line 93 · raw

@s:0x88d5b48c03f82f217d3a2aa0656744f4/main.Source -> @a:U32 -> @b:U32 -> @invalid:{Bool.and(U32.is_le(a, b), U32.is_le(b, 0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.size(s))) == False{} : Bool} -> {0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.span(s, a, b) == (s, Fail{0x88d5b48c03f82f217d3a2aa0656744f4/types.InvalidRange{}}) : Pair(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source, Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Span>)}

law foreign_restore provedin PROOF.bendsource · line 100 · raw

@s:0x88d5b48c03f82f217d3a2aa0656744f4/main.Source -> @foreign:U32 -> @i:U32 -> @different:{U32.is_eq(foreign, 0x88d5b48c03f82f217d3a2aa0656744f4/proof_observations.identity(s)) == False{} : Bool} -> {0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.restore(s, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{foreign, i}) == (s, Fail{0x88d5b48c03f82f217d3a2aa0656744f4/types.ForeignFile{}}) : Pair(0x88d5b48c03f82f217d3a2aa0656744f4/main.Source, Result<&1, &1, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Error, 0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor>)}

law inhabited_cursor_domain provedin PROOF.bendsource · line 107 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.cursor("ab", 1, Done{0x88d5b48c03f82f217d3a2aa0656744f4/types.Cursor{7, 1}}) == True{} : Bool}

law inhabited_span_domain provedin PROOF.bendsource · line 109 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/observations.span("ab", 0, 2) == True{} : Bool}

law maximum_policy provedin PROOF.bendsource · line 112 · raw

{0x88d5b48c03f82f217d3a2aa0656744f4/main.Source.maximum == 16777215 : U32}