LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./main.bend as Simport ./types.bend as Timport ./observations.bend as Oimport ./proof_observations.bend as P# Universal over file IDs, fixed inhabited text shapes. Not a theorem for all strings.law content_identity:  for id: U32  {P.text(S.Source.new(id,"a😀\nβ")) == Done{"a😀\nβ"} : Result<T.Error,String>}law file_identity:  for id: U32  {P.file(S.Source.new(id,"a😀\nβ")) == Done{id} : Result<T.Error,U32>}law empty_content:  for id: U32  {P.text(S.Source.bounded(id,"",0)) == Done{""} : Result<T.Error,String>}law empty_lines:  for id: U32  {P.lines(S.Source.new(id,"")) == Done{1} : Result<T.Error,U32>}law scalar_units:  for id: U32  {P.length(S.Source.new(id,"a😀\nβ")) == Done{4} : Result<T.Error,U32>}# Concrete normalization theorems through public observations and independent model.law indexed_value:  {O.get("a😀\nβ",1) == True{} : Bool}law peek_codepoint:  {O.peek("a😀",T.Cursor{7,1},Done{Some{'😀'}}) == True{} : Bool}law bump_restore_content:  {O.bump("a😀",T.Cursor{7,1},T.Cursor{7,2},Some{'😀'}) == True{} : Bool}law eof_fixed_point:  {O.bump("a😀",T.Cursor{7,2},T.Cursor{7,2},None{}) == True{} : Bool}law span_order:  {O.extract("a😀\nβ",T.Span{7,1,3},Done{"😀\n"}) == True{} : Bool}law empty_eof_span:  {O.span("a😀",2,2) == True{} : Bool}law newline_location:  {O.locate("a😀\nβ",3) == True{} : Bool}law newline_roundtrip:  {O.roundtrip("a😀\nβ",3) == True{} : Bool}law cr_is_content:  {O.locate("a\rb",2) == True{} : Bool}law crlf_location:  {O.locate("a\r\nb",3) == True{} : Bool}law trailing_line:  {O.metadata("\n",2) == True{} : Bool}law canonical_location:  {O.offset("a\nb",T.Location{0,2}) == True{} : Bool}law foreign_cursor:  {O.restore("a",T.Cursor{8,0},Fail{T.ForeignFile{}}) == True{} : Bool}law foreign_span:  {O.extract("a",T.Span{8,0,1},Fail{T.ForeignFile{}}) == True{} : Bool}law rejected_span:  {O.span_reject("ab",2,1) == True{} : Bool}law rejected_offset:  {O.cursor("a",2,Fail{T.Bounds{}}) == True{} : Bool}law exhausted_limit:  {O.rejected(T.Limit{},S.Source.bounded(7,"abc",2)) == True{} : Bool}law invalid_scalar:  {O.rejected(T.InvalidScalar{},S.Source.new(7,SCon{Chr{55296},""})) == True{} : Bool}# Auxiliary helper normalization over arbitrary source and candidate cursor.# Public conditional wrapper theorems below establish bounds and state preservation.law checked_cursor:  for s: S.Source  for id: U32  for i: U32  {S.cursor_if(s,T.Cursor{id,i},True{}) == (s,Done{T.Cursor{id,i}}) : S.Source & Result<T.Error,T.Cursor>}law accepted_cursor:  for s: S.Source  for i: U32  for valid: {U32.is_le(i,P.size(s)) == True{} : Bool}  {S.Source.cursor(s,i) == (s,Done{T.Cursor{P.identity(s),i}}) : S.Source & Result<T.Error,T.Cursor>}law rejected_cursor:  for s: S.Source  for i: U32  for invalid: {U32.is_le(i,P.size(s)) == False{} : Bool}  {S.Source.cursor(s,i) == (s,Fail{T.Bounds{}}) : S.Source & Result<T.Error,T.Cursor>}law accepted_span:  for s: S.Source  for a: U32  for b: U32  for valid: {Bool.and(U32.is_le(a,b),U32.is_le(b,P.size(s))) == True{} : Bool}  {S.Source.span(s,a,b) == (s,Done{T.Span{P.identity(s),a,b}}) : S.Source & Result<T.Error,T.Span>}law rejected_span_universal:  for s: S.Source  for a: U32  for b: U32  for invalid: {Bool.and(U32.is_le(a,b),U32.is_le(b,P.size(s))) == False{} : Bool}  {S.Source.span(s,a,b) == (s,Fail{T.InvalidRange{}}) : S.Source & Result<T.Error,T.Span>}law foreign_restore:  for s: S.Source  for foreign: U32  for i: U32  for different: {U32.is_eq(foreign,P.identity(s)) == False{} : Bool}  {S.Source.restore(s,T.Cursor{foreign,i}) == (s,Fail{T.ForeignFile{}}) : S.Source & Result<T.Error,T.Cursor>}law inhabited_cursor_domain:  {O.cursor("ab",1,Done{T.Cursor{7,1}}) == True{} : Bool}law inhabited_span_domain:  {O.span("ab",0,2) == True{} : Bool}law maximum_policy:  {S.Source.maximum() == 16777215 : U32}