BYTE_LAWS.bend source

BYTE_LAWS.bend on the hub · documented module

import Baseimport ./bytes.bend as Bimport ./byte_model.bend as M# Auxiliary list algebra, universal.law list_right:  for +s: List<&2,U32>  {List.append(&2,U32,s, Nil{}) == s : List<&2,U32>}law list_assoc:  for +a: List<&2,U32>  for +b: List<&2,U32>  for +c: List<&2,U32>  {List.append(&2,U32,List.append(&2,U32,a,b),c) == List.append(&2,U32,a,List.append(&2,U32,b,c)) : List<&2,U32>}law flatten_join:  for +a: List<&2,List<&2,U32>>  for +b: List<&2,List<&2,U32>>  {M.flatten(M.join(a,b)) == List.append(&2,U32,M.flatten(a),M.flatten(b)) : List<&2,U32>}# Universal refinement, including an arbitrary suffix.law emit_model:  for +t: B.Tree  for +suffix: List<&2,U32>  {B.emit(t,suffix) == List.append(&2,U32,M.flatten(M.chunks(t)),suffix) : List<&2,U32>}law finish_model:  for +t: B.Tree  for +cap: U32  for +n: U32  {B.finish(B.Buffer{cap,n,t}) == M.flatten(M.chunks(t)) : List<&2,U32>}# Concrete normalization, including capacity zero, overflow and invalid bytes.law empty:  {B.finish(B.empty(0)) == [] : List<&2,U32>}law content:  {M.observe(B.append(B.empty(4),[0,127,128,255])) == Done{([0,127,128,255],4)} : Result<B.Error,List<&2,U32> & U32>}law invalid:  {M.observe(B.byte(B.empty(4),256)) == Fail{B.InvalidByte{256}} : Result<B.Error,List<&2,U32> & U32>}law full:  {M.observe(B.byte(B.empty(0),0)) == Fail{B.Limit{}} : Result<B.Error,List<&2,U32> & U32>}law compose_content:  {M.observe(B.compose(B.Buffer{4,2,B.Chunk{[0,97]}},B.Buffer{2,2,B.Chunk{[255,10]}})) == Done{([0,97,255,10],4)} : Result<B.Error,List<&2,U32> & U32>}law overflow:  {B.combine(U32.is_le(1,U32.sub(4294967295,4294967295)),4294967295,4294967295,1,B.Empty{},B.Empty{}) == Fail{B.Limit{}} : Result<B.Error,B.Builder>}