Cairn · module
Cairn.Frame.Bytes
lean/Cairn/Frame/Bytes.lean
The byte layer of the boundary format (docs/frame.md): little-endian primitives, three ways.
Enc.*encode toList UInt8. They are the specification: short, and what the round-trip theorems talk about.Decis a decoder overList UInt8(consume a prefix, return the value and the rest). Each primitive has a round-trip lemma of the formd (Enc.x v ++ rest) = some (v, rest), which is what makes the whole-frame theorems compose.Put.*append to aByteArray. They are what runs;Put.x_datasays each one appends exactlyEnc.xto the buffer's bytes.
Integers that cross the boundary are 32-bit: Int as two's complement (i32), Nat as
unsigned (u32). The round trip needs the value to fit, stated with FitsI32 and FitsU32.
Order
Definitions 51
FitsU32 (n : Nat) : PropInstances
FitsI32 (v : Int) : PropInstances
FitsStr (s : String) : PropA string whose UTF-8 encoding has a u32 length.
Instances
FitsU64 (n : Nat) : PropInstances
FitsI64 (v : Int) : PropInstances
FitsBytes (b : ByteArray) : PropA byte payload with a u32 length.
Instances
toU32 (v : Int) : Nat
Two's complement, as an unsigned 32-bit value.
ofU32 (n : Nat) : Int
toU64 (v : Int) : Nat
Two's complement, as an unsigned 64-bit value.
ofU64 (n : Nat) : Int
i32Word (v : Int) : UInt32
The two's-complement word of v, without big-integer arithmetic: 2³² is not a small number
to Lean's runtime, so v % 4294967296 (and even the literal) goes through GMP.
satU32 (n : Nat) : Nat
Clamp to the largest u32 (font fields cross saturating, docs/frame.md).
satI32 (v : Int) : Int
Clamp to the i32 range (a text draw's tracking crosses saturating, like font fields).
ofBytes (a b c d : UInt8) : Nat
u32 (n : Nat) : List UInt8
i32 (v : Int) : List UInt8
bool (b : Bool) : List UInt8
u64 (n : Nat) : List UInt8
Low word, then high word.
i64 (v : Int) : List UInt8
bytes (b : ByteArray) : List UInt8
u32 byte length, then the bytes.
str (s : String) : List UInt8
u32 byte length, then the UTF-8 bytes.
pad (n : Nat) : List UInt8
Reserved bytes: written as zero, ignored when read.
sect (body : List UInt8) : List UInt8
A sized section: u32 byte length, then the body.
Dec (α : Type) : Type
Consume a prefix of the input; none is a decoding error.
Instances
pure {α : Type} (a : α) : Dec α
bind {α β : Type} (d : Dec α) (f : α → Dec β) : Dec β
fail {α : Type} : Dec α
byte : Dec UInt8
u32 : Dec Nat
i32 : Dec Int
bool : Dec Bool
u64 : Dec Nat
i64 : Dec Int
take (n : Nat) : Dec (List UInt8)
skip (n : Nat) : Dec Unit
str : Dec String
bytes : Dec ByteArray
count {α : Type} (d : Dec α) : Nat → Dec (List α)n values, one after another.
sect {α : Type} (d : Dec α) : Dec αA sized section: read the u32 byte length, decode the body with d, which must consume
it exactly.
run {α : Type} (d : Dec α) (l : List UInt8) : Option αDecode all of l; trailing bytes are an error.
u8 (b : ByteArray) (v : UInt8) : ByteArray
word (b : ByteArray) (w : UInt32) : ByteArray
A machine word, little-endian, by shifts.
u32 (b : ByteArray) (n : Nat) : ByteArray
i32 (b : ByteArray) (v : Int) : ByteArray
bool (b : ByteArray) (v : Bool) : ByteArray
str (b : ByteArray) (s : String) : ByteArray
u64 (b : ByteArray) (n : Nat) : ByteArray
i64 (b : ByteArray) (v : Int) : ByteArray
bytes (b x : ByteArray) : ByteArray
pad (b : ByteArray) : Nat → ByteArray
setU32 (b : ByteArray) (i n : Nat) : ByteArray
Overwrite the four bytes at i with n (for a section length, once the body is known).
Theorems 45
fitsU32_zero : FitsU32 0
toU64_fits (v : Int) : FitsU64 (toU64 v)
ofU64_toU64 {v : Int} (h : FitsI64 v) : ofU64 (toU64 v) = v
i32Word_eq (v : Int) : i32Word v = UInt32.ofNat (toU32 v)
toU32_fits (v : Int) : FitsU32 (toU32 v)
ofU32_toU32 {v : Int} (h : FitsI32 v) : ofU32 (toU32 v) = v
satU32_of_fits {n : Nat} (h : FitsU32 n) : satU32 n = n
satU32_fits (n : Nat) : FitsU32 (satU32 n)
satI32_of_fits {v : Int} (h : FitsI32 v) : satI32 v = v
satI32_fits (v : Int) : FitsI32 (satI32 v)
ofBytes_lt (a b c d : UInt8) : ofBytes a b c d < 4294967296
length_u32 (n : Nat) : (u32 n).length = 4
length_i32 (v : Int) : (i32 v).length = 4
length_u64 (n : Nat) : (u64 n).length = 8
length_i64 (v : Int) : (i64 v).length = 8
pure_apply {α : Type} (a : α) (l : List UInt8) : pure a l = some (a, l)
bind_apply {α β : Type} (d : Dec α) (f : α → Dec β) (l : List UInt8) :
(d >>= f) l =
match d l with
| some (a, r) => f a r
| none => none
fail_apply {α : Type} (l : List UInt8) : fail l = none
bind_of_eq {α β : Type} {d : Dec α} {f : α → Dec β} {l r : List UInt8}
{a : α} (h : d l = some (a, r)) : (d >>= f) l = f a rThe step every compound round-trip proof takes: run the first decoder, continue.
byte_cons (b : UInt8) (r : List UInt8) : byte (b :: r) = some (b, r)
u32_enc {n : Nat} (h : FitsU32 n) (r : List UInt8) :
u32 (Enc.u32 n ++ r) = some (n, r)
i32_enc {v : Int} (h : FitsI32 v) (r : List UInt8) :
i32 (Enc.i32 v ++ r) = some (v, r)
u64_enc {n : Nat} (h : FitsU64 n) (r : List UInt8) :
u64 (Enc.u64 n ++ r) = some (n, r)
i64_enc {v : Int} (h : FitsI64 v) (r : List UInt8) :
i64 (Enc.i64 v ++ r) = some (v, r)
bool_enc (b : Bool) (r : List UInt8) : bool (Enc.bool b ++ r) = some (b, r)
take_enc (l r : List UInt8) : take l.length (l ++ r) = some (l, r)
skip_pad (n : Nat) (r : List UInt8) : skip n (Enc.pad n ++ r) = some ((), r)
fromUTF8?_toUTF8 (s : String) :
String.fromUTF8? { data := s.toUTF8.data.toList.toArray } = some s
str_enc {s : String} (h : FitsStr s) (r : List UInt8) :
str (Enc.str s ++ r) = some (s, r)
bytes_enc {b : ByteArray} (h : FitsBytes b) (r : List UInt8) :
bytes (Enc.bytes b ++ r) = some (b, r)
count_enc {α : Type} {d : Dec α} {e : α → List UInt8} (xs : List α)
(h : ∀ (x : α), x ∈ xs → ∀ (r : List UInt8), d (e x ++ r) = some (x, r))
(r : List UInt8) : d.count xs.length (List.flatMap e xs ++ r) = some (xs, r)
sect_enc {α : Type} {d : Dec α} {body : List UInt8} {a : α}
(hd : d body = some (a, [])) (hn : FitsU32 body.length) (r : List UInt8) :
d.sect (Enc.sect body ++ r) = some (a, r)
run_enc {α : Type} {d : Dec α} {l : List UInt8} {a : α}
(h : d (l ++ []) = some (a, [])) : d.run l = some a
u8_data (b : ByteArray) (v : UInt8) : (u8 b v).data.toList = b.data.toList ++ [v]
shift8 (n : Nat) : (UInt32.ofNat n >>> 8).toUInt8 = UInt8.ofNat (n / 256)
shift16 (n : Nat) : (UInt32.ofNat n >>> 16).toUInt8 = UInt8.ofNat (n / 65536)
shift24 (n : Nat) :
(UInt32.ofNat n >>> 24).toUInt8 = UInt8.ofNat (n / 16777216)
u32_data (b : ByteArray) (n : Nat) : (u32 b n).data.toList = b.data.toList ++ Enc.u32 n
i32_data (b : ByteArray) (v : Int) : (i32 b v).data.toList = b.data.toList ++ Enc.i32 v
bool_data (b : ByteArray) (v : Bool) : (bool b v).data.toList = b.data.toList ++ Enc.bool v
str_data (b : ByteArray) (s : String) : (str b s).data.toList = b.data.toList ++ Enc.str s
u64_data (b : ByteArray) (n : Nat) : (u64 b n).data.toList = b.data.toList ++ Enc.u64 n
i64_data (b : ByteArray) (v : Int) : (i64 b v).data.toList = b.data.toList ++ Enc.i64 v
bytes_data (b x : ByteArray) :
(bytes b x).data.toList = b.data.toList ++ Enc.bytes x
pad_data (b : ByteArray) (n : Nat) : (pad b n).data.toList = b.data.toList ++ Enc.pad n
Instances 7
instDecidableFitsU32 (n : Nat) : Decidable (FitsU32 n)
instDecidableFitsI32 (v : Int) : Decidable (FitsI32 v)
instDecidableFitsStr (s : String) : Decidable (FitsStr s)
instDecidableFitsU64 (n : Nat) : Decidable (FitsU64 n)
instDecidableFitsI64 (v : Int) : Decidable (FitsI64 v)
instDecidableFitsBytes (b : ByteArray) : Decidable (FitsBytes b)
instMonad : Monad Dec