Cairn.Frame.Events
lean/Cairn/Frame/Events.lean
Event byte format v2 (host → Lean, docs/frame.md): specification encoder
Wire.Enc.events, decoder Wire.Dec.events, and the round trip decodeEvents_encodeEvents.
header "CAEV" u16 version=2 u16 flags=0 u32 count 12 bytes
events count records, each [tag, a, b, 0] then fixed fields, then at most one string
A surface record (tag 21) is its head and a u32 place followed by one whole surface-local
record (tags 0–17), so every record still stands alone.
Lean only decodes events at run time (the host encodes them), and a frame's events are a handful of records, so the decoder runs the list specification directly on the buffer's bytes.
Imports Cairn.Input, Cairn.Frame.Encode
Definitions 32
code : Button → UInt8
ofCode : UInt8 → Option Button
code : Fault → UInt8
ofCode : UInt8 → Option Fault
code : Reply → UInt8
done 0, bytes 1, http 2, failed 3, names 4, app 5, flag 6, image 7.
faultCode : Reply → UInt8
code : SubEvent → UInt8
tick 0, changed 1, audio 2, keyDown 3, keyUp 4, otherKey 5, failed 6,
started 7, evicted 8.
faultCode : SubEvent → UInt8
fitsTime (t : Time) : Bool
fitsLevel (l : Level) : Bool
fitsSubEvent : SubEvent → Bool
fitsReply : Reply → Bool
fitsEvent : Event → Bool
head (tag a b : UInt8) : List UInt8
The record head: tag, two small fields, a reserved zero.
replyBody : Reply → List UInt8
A reply's fields after its record head and id.
level (l : Level) : List UInt8
subEventBody : SubEvent → List UInt8
A subscription event's fields after its record head and id.
event : Event → List UInt8
eventsMagic : List UInt8
eventsHeader : List UInt8
events (es : List Event) : List UInt8
opt {α : Type} (present : UInt8) (a : α) : Dec (Option α)
replyBody (code fault : UInt8) : Dec Reply
level : Dec Level
subEventBody (code fault : UInt8) : Dec SubEvent
The body of a subscription event with code code; only failed has a fault.
headed (k : UInt8 → UInt8 → UInt8 → Dec Event) : Dec Event
Read a record head, then the rest of the record by its tag.
body (tag a b : UInt8) : Dec Event
Every record but surface, after its head.
plain : Dec Event
A record other than surface.
event : Dec Event
One record. A surface record holds exactly one surface-local record.
events : Dec (List Event)
encodeEvents (es : Array Event) : ByteArray
decodeEvents (b : ByteArray) : Option (Array Event)
Theorems 11
ofCode_code (b : Button) : ofCode (code b) = some b
ofCode_code (f : Fault) : ofCode (code f) = some f
opt_isSome {α : Type} (o : Option α) (d : α) (r : List UInt8) :
opt (if o.isSome = true then 1 else 0) (o.getD d) r = some (o, r)
replyBody_enc {rp : Reply} (h : fitsReply rp = true) (r : List UInt8) :
replyBody (Reply.code rp) (Reply.faultCode rp) (Enc.replyBody rp ++ r) = some (rp, r)
level_enc {l : Level} (h : fitsLevel l = true) (r : List UInt8) :
level (Enc.level l ++ r) = some (l, r)
subEventBody_enc {e : SubEvent} (h : fitsSubEvent e = true)
(r : List UInt8) :
subEventBody (SubEvent.code e) (SubEvent.faultCode e) (Enc.subEventBody e ++ r) =
some (e, r)
plain_enc {e : Event} (h : fitsEvent e = true) (hs : e.isSurface = false)
(r : List UInt8) : plain (Enc.event e ++ r) = some (e, r)
event_eq_plain (t : UInt8) (l : List UInt8) (ht : t ≠ 21) : event (t :: l) = plain (t :: l)
event_enc {e : Event} (h : fitsEvent e = true) (r : List UInt8) :
event (Enc.event e ++ r) = some (e, r)
events_enc {es : List Event} (h : ∀ (e : Event), e ∈ es → fitsEvent e = true)
(hn : FitsU32 es.length) (r : List UInt8) : events (Enc.events es ++ r) = some (es, r)
decodeEvents_encodeEvents (es : Array Event) (h : es.all Wire.fitsEvent = true) (hn : es.size < 4294967296) : decodeEvents (encodeEvents es) = some es
Round trip. Every batch of events whose values fit the wire's fields decodes to itself.