proofs/lib/lemmas/src/codec.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/codec.bend as Codec

2 imports

import Base
import ../types/model.bend as T

Laws

law string_roundtrip provedsource · line 44 · raw

@s:String -> {string_decode(string_encode(s)) == s : String}

law natural_roundtrip provedsource · line 50 · raw

@n:Nat -> {natural_decode(natural_encode(n)) == n : Nat}

law integer_roundtrip provedsource · line 61 · raw

@n:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer -> {integer_decode(integer_encode(n)) == n : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer}

law integer_injective provedsource · line 71 · raw

@a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer -> @e:{integer_encode(a) == integer_encode(b) : String} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer}

law string_injective provedsource · line 82 · raw

@a:String -> @b:String -> @e:{string_encode(a) == string_encode(b) : String} -> {a == b : String}

law bit_roundtrip provedsource · line 122 · raw

@b:Bool -> {char_bit(bit_char(b)) == b : Bool}

law word_roundtrip provedsource · line 132 · raw

@n:Nat -> @w:Word(n) -> {word_decode(n, word_encode(n, w)) == w : Word(n)}

law word_injective provedsource · line 149 · raw

@+n:Nat -> @a:Word(n) -> @b:Word(n) -> @e:{word_encode(n, a) == word_encode(n, b) : String} -> {a == b : Word(n)}

law string_equality_preserved provedsource · line 161 · raw

@a:String -> @b:String -> @e:{a == b : String} -> {string_encode(a) == string_encode(b) : String}

law integer_equality_preserved provedsource · line 169 · raw

@a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer -> @e:{a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer} -> {integer_encode(a) == integer_encode(b) : String}

law word_equality_preserved provedsource · line 177 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @e:{a == b : Word(n)} -> {word_encode(n, a) == word_encode(n, b) : String}

law word64_injective provedsource · line 190 · raw

@a:Word(64n) -> @b:Word(64n) -> @e:{word64_encode(a) == word64_encode(b) : String} -> {a == b : Word(64n)}

Definitions

def string_encode source · line 5 · raw

@s:String -> String

Identity preserves all Base String characters, including Chr{0}.

def string_decode source · line 8 · raw

@s:String -> String

def natural_encode source · line 13 · raw

@n:Nat -> String

A unary integer codec: chosen for a simple total inverse, not speed. Every character has code 0; the first character encodes the sign.

def natural_decode source · line 20 · raw

@s:String -> Nat

def integer_encode source · line 23 · raw

@n:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer -> String

def integer_decode_sign source · line 30 · raw

@sign:Bool -> @n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer

def integer_decode source · line 37 · raw

@s:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Integer

def bit_char source · line 92 · raw

@b:Bool -> Char

Fixed-width binary words are a practical integer codec; unlike unary Integer, a 64-bit key always occupies 64 characters. Leading zero bits are retained.

def char_bit source · line 99 · raw

@c:Char -> Bool

def word_encode source · line 104 · raw

@n:Nat -> @w:Word(n) -> String

def word_decode source · line 113 · raw

@n:Nat -> @s:String -> Word(n)

def word64_encode source · line 187 · raw

@w:Word(64n) -> String

The Word64 key codec used by the adapter for bigint keys.