~/bend-docscommunity

LAWS.bend open laws/TODOs

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

2 imports
import Base
import ./lib.bend as R

Laws

law empty_is_new provedin PROOF.bendsource · line 5 · raw

@c:Nat -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.empty(c) == 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(c) : 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf}

Construction and empty-state laws.

law capacity_new provedin PROOF.bendsource · line 9 · raw

@c:Nat -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.capacity(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(c)) == c : Nat}

law length_new provedin PROOF.bendsource · line 13 · raw

@c:Nat -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.length(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(c)) == 0n : Nat}

law empty_new provedin PROOF.bendsource · line 17 · raw

@c:Nat -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.is_empty(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(c)) == True{} : Bool}

law new_zero provedin PROOF.bendsource · line 21 · raw

{0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(0n) == 0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{0n, 0n, 0n, []} : 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf}

law new_one provedin PROOF.bendsource · line 24 · raw

{0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(1n) == 0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 0n, [0]} : 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf}

law pop_empty provedin PROOF.bendsource · line 28 · raw

@c:Nat -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.pop(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(c)) == None{} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Pop>}

Empty observations and zero-capacity behavior.

law peek_empty provedin PROOF.bendsource · line 32 · raw

@c:Nat -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.peek(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(c)) == None{} : Maybe<&2, U32>}

law to_list_empty provedin PROOF.bendsource · line 36 · raw

{0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.to_list(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(0n)) == [] : List<&2, U32>}

law zero_push_fails provedin PROOF.bendsource · line 39 · raw

@x:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.push(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(0n), x) == None{} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Push>}

law zero_is_full provedin PROOF.bendsource · line 43 · raw

{0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.is_full(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(0n)) == True{} : Bool}

law push_one provedin PROOF.bendsource · line 47 · raw

@x:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.push(0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.new(1n), x) == Some{0x831d2a84246839cb2e33f4e7653d3f09/lib.PushResult{0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 1n, [x]}}} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Push>}

Singleton push/pop/peek behavior.

law one_is_full_after_push provedin PROOF.bendsource · line 55 · raw

@x:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.is_full(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 1n, [x]}) == True{} : Bool}

law push_full_fails provedin PROOF.bendsource · line 61 · raw

@x:U32 -> @y:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.push(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 1n, [x]}, y) == None{} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Push>}

law peek_one provedin PROOF.bendsource · line 70 · raw

@x:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.peek(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 1n, [x]}) == Some{x} : Maybe<&2, U32>}

law pop_one provedin PROOF.bendsource · line 78 · raw

@x:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.pop(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 1n, [x]}) == Some{0x831d2a84246839cb2e33f4e7653d3f09/lib.PopResult{x, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 0n, [x]}}} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Pop>}

law to_list_one provedin PROOF.bendsource · line 86 · raw

@x:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.to_list(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{1n, 0n, 1n, [x]}) == [x] : List<&2, U32>}

law to_list_two provedin PROOF.bendsource · line 95 · raw

@x:U32 -> @y:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.to_list(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 0n, 2n, [x, y]}) == [x, y] : List<&2, U32>}

A two-slot buffer demonstrates FIFO order and physical wrap-around.

law pop_two provedin PROOF.bendsource · line 104 · raw

@x:U32 -> @y:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.pop(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 0n, 2n, [x, y]}) == Some{0x831d2a84246839cb2e33f4e7653d3f09/lib.PopResult{x, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 1n, 1n, [x, y]}}} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Pop>}

law wrapped_push provedin PROOF.bendsource · line 113 · raw

@x:U32 -> @y:U32 -> @z:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.push(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 1n, 1n, [x, y]}, z) == Some{0x831d2a84246839cb2e33f4e7653d3f09/lib.PushResult{0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 1n, 2n, [z, y]}}} : Maybe<&2, 0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.Push>}

law wrapped_to_list provedin PROOF.bendsource · line 123 · raw

@x:U32 -> @y:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.to_list(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 1n, 2n, [x, y]}) == [y, x] : List<&2, U32>}

law length_full provedin PROOF.bendsource · line 132 · raw

@x:U32 -> @y:U32 -> {0x831d2a84246839cb2e33f4e7653d3f09/lib.RingBuf.length(0x831d2a84246839cb2e33f4e7653d3f09/lib.RB{2n, 1n, 2n, [x, y]}) == 2n : Nat}