BYTE_LAWS.bend open laws/TODOs

raw source on the hub · import 0xc409b77d3230ca33374caf6b0993f0cb/BYTE_LAWS.bend as BYTE_LAWS

3 imports

import Base
import ./bytes.bend as B
import ./byte_model.bend as M

Laws

law list_right provedin BYTE_PROOF.bendsource · line 6 · raw

@+s:List<&2, U32> -> {List.append(&2, U32, s, []) == s : List<&2, U32>}

Auxiliary list algebra, universal.

law list_assoc provedin BYTE_PROOF.bendsource · line 10 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+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 provedin BYTE_PROOF.bendsource · line 16 · raw

@+a:List<&2, List<&2, U32>> -> @+b:List<&2, List<&2, U32>> -> {0xc409b77d3230ca33374caf6b0993f0cb/byte_model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/byte_model.join(a, b)) == List.append(&2, U32, 0xc409b77d3230ca33374caf6b0993f0cb/byte_model.flatten(a), 0xc409b77d3230ca33374caf6b0993f0cb/byte_model.flatten(b)) : List<&2, U32>}

law emit_model provedin BYTE_PROOF.bendsource · line 22 · raw

@+t:0xc409b77d3230ca33374caf6b0993f0cb/bytes.Tree -> @+suffix:List<&2, U32> -> {0xc409b77d3230ca33374caf6b0993f0cb/bytes.emit(t, suffix) == List.append(&2, U32, 0xc409b77d3230ca33374caf6b0993f0cb/byte_model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/byte_model.chunks(t)), suffix) : List<&2, U32>}

Universal refinement, including an arbitrary suffix.

law finish_model provedin BYTE_PROOF.bendsource · line 27 · raw

@+t:0xc409b77d3230ca33374caf6b0993f0cb/bytes.Tree -> @+cap:U32 -> @+n:U32 -> {0xc409b77d3230ca33374caf6b0993f0cb/bytes.finish(0xc409b77d3230ca33374caf6b0993f0cb/bytes.Buffer{cap, n, t}) == 0xc409b77d3230ca33374caf6b0993f0cb/byte_model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/byte_model.chunks(t)) : List<&2, U32>}

law empty provedin BYTE_PROOF.bendsource · line 34 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/bytes.finish(0xc409b77d3230ca33374caf6b0993f0cb/bytes.empty(0)) == [] : List<&2, U32>}

Concrete normalization, including capacity zero, overflow and invalid bytes.

law content provedin BYTE_PROOF.bendsource · line 37 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/byte_model.observe(0xc409b77d3230ca33374caf6b0993f0cb/bytes.append(0xc409b77d3230ca33374caf6b0993f0cb/bytes.empty(4), [0, 127, 128, 255])) == Done{([0, 127, 128, 255], 4)} : Result<&1, &1, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Error, Pair(List<&2, U32>, U32)>}

law invalid provedin BYTE_PROOF.bendsource · line 40 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/byte_model.observe(0xc409b77d3230ca33374caf6b0993f0cb/bytes.byte(0xc409b77d3230ca33374caf6b0993f0cb/bytes.empty(4), 256)) == Fail{0xc409b77d3230ca33374caf6b0993f0cb/bytes.InvalidByte{256}} : Result<&1, &1, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Error, Pair(List<&2, U32>, U32)>}

law full provedin BYTE_PROOF.bendsource · line 43 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/byte_model.observe(0xc409b77d3230ca33374caf6b0993f0cb/bytes.byte(0xc409b77d3230ca33374caf6b0993f0cb/bytes.empty(0), 0)) == Fail{0xc409b77d3230ca33374caf6b0993f0cb/bytes.Limit{}} : Result<&1, &1, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Error, Pair(List<&2, U32>, U32)>}

law compose_content provedin BYTE_PROOF.bendsource · line 46 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/byte_model.observe(0xc409b77d3230ca33374caf6b0993f0cb/bytes.compose(0xc409b77d3230ca33374caf6b0993f0cb/bytes.Buffer{4, 2, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Chunk{[0, 97]}}, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Buffer{2, 2, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Chunk{[255, 10]}})) == Done{([0, 97, 255, 10], 4)} : Result<&1, &1, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Error, Pair(List<&2, U32>, U32)>}

law overflow provedin BYTE_PROOF.bendsource · line 49 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/bytes.combine(U32.is_le(1, U32.sub(4294967295, 4294967295)), 4294967295, 4294967295, 1, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Empty{}, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Empty{}) == Fail{0xc409b77d3230ca33374caf6b0993f0cb/bytes.Limit{}} : Result<&1, &1, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Error, 0xc409b77d3230ca33374caf6b0993f0cb/bytes.Builder>}