Cairn.Frame.Encode

code : Role → UInt8

ofCode : UInt8 → Option Role

code : Cursor → UInt8

ofCode : UInt8 → Option Cursor

wire : FontWidth → UInt8

ofWire : UInt8 → Option FontWidth

code : Corner → UInt8

ofCode : UInt8 → Option Corner

checkedCode : Option Bool → UInt8

checkedOfCode : UInt8 → Option (Option Bool)

code : Request.Kind → UInt8

ofCode : UInt8 → Option Request.Kind

code : Permission → UInt8

ofCode : UInt8 → Option Permission

code : Priority → UInt8

ofCode : UInt8 → Option Priority

code : ScrollTarget → UInt8

arg : ScrollTarget → Nat

ofCode : UInt8 → Nat → Option ScrollTarget

code : Sub → UInt8

code : Key → UInt8

scalar : Key → Nat

ofCode (code : UInt8) (scalar : Nat) : Option Key

code (m : Mods) : UInt8

ofCode (b : UInt8) : Option Mods

code : SurfaceKind → UInt8

ofCode : UInt8 → Option SurfaceKind

code : MenuKind → UInt8

ofCode : UInt8 → Option MenuKind

code : ScreenChoice → UInt8

ofCode : UInt8 → Option ScreenChoice

code : Anchor → UInt8

ofCode (code : UInt8) (offset : Nat) : Option Anchor

noShortcut : Shortcut

fu (n : Nat) : Bool

fi (v : Int) : Bool

fs (s : String) : Bool

fitsRect (r : Rect) : Bool

fitsRef (c : ControlRef) : Bool

fitsRange (p : Nat × Nat) : Bool

fitsInts (xs : List Int) : Bool

fitsPaint (p : Paint) : Bool

fitsShadow (s : Shadow) : Bool

fitsDraw : Draw → Bool

fitsAx (n : AxNode) : Bool

fitsTextInput (t : TextInput) : Bool

fu64 (n : Nat) : Bool

fi64 (v : Int) : Bool

fb (b : ByteArray) : Bool

fitsHeaders (hs : List (String × String)) : Bool

fitsPart : Part → Bool

fitsSource : Secret.Source → Bool

fitsSecret (s : Secret) : Bool

fitsRequest : Request → Bool

fitsEffect : Effect → Bool

fitsSub : Sub → Bool

fitsSubCmd : SubCmd → Bool

fitsCanvas (c : Canvas) : Bool

fitsMenuRecord (m : MenuRecord) : Bool

fitsStatus (s : StatusFrame) : Bool

fitsSurface (s : SurfaceFrame) : Bool

fitsFrame (f : Frame) : Bool

rect (r : Rect) : List UInt8

point (p : Point) : List UInt8

size (s : Size) : List UInt8

color (c : Color) : List UInt8

ref (c : ControlRef) : List UInt8

range (p : Nat × Nat) : List UInt8

noColor : Color

list {α : Type} (e : α → List UInt8) (xs : List α) : List UInt8

ints (xs : List Int) : List UInt8

intLists (xss : List (List Int)) : List UInt8

draw : Draw → List UInt8

ax (n : AxNode) : List UInt8

textInput : Option TextInput → List UInt8

cursor (c : Cursor) : List UInt8

header1 (kv : String × String) : List UInt8

headers (hs : List (String × String)) : List UInt8

part : Part → List UInt8

sourceCode : Secret.Source → UInt8

source : Secret.Source → List UInt8

secret (s : Secret) : List UInt8

optSecret : Option Secret → List UInt8

parts (ps : List Part) : List UInt8

requestBody : Request → List UInt8

effect : Effect → List UInt8

subBody : Sub → List UInt8

subCmd : SubCmd → List UInt8

wake (w : Option Nat) : List UInt8

magic : List UInt8

canvas (c : Canvas) : List UInt8

menuRecord (m : MenuRecord) : List UInt8

status (s : StatusFrame) : List UInt8

surface (s : SurfaceFrame) : List UInt8

header : List UInt8

frame (f : Frame) : List UInt8

expect (bs : List UInt8) : Dec Unit

rect : Dec Rect

point : Dec Point

size : Dec Size

color : Dec Color

ref : Dec ControlRef

range : Dec (Nat × Nat)

list {α : Type} (d : Dec α) : Dec (List α)

ints : Dec (List Int)

intLists : Dec (List (List Int))

draw : Dec Draw

ax : Dec AxNode

textInput : Dec (Option TextInput)

cursor : Dec Cursor

header1 : Dec (String × String)

headers : Dec (List (String × String))

part : Dec Part

optSecret : Dec (Option Secret)

parts : Dec (List Part)

requestBody (redact : Bool) : Request.Kind → Dec Request

effect : Dec Effect

subBody : UInt8 → Dec Sub

subCmd : Dec SubCmd

wake : Dec (Option Nat)

canvas : Dec Canvas

shortcut (has : Bool) (key : UInt8) (scalar : Nat) (mods : UInt8) :
  Dec (Option Shortcut)

menuRecord : Dec MenuRecord

status : Dec StatusFrame

surface : Dec SurfaceFrame

frame : Dec Frame

SizeOk (f : Frame) : Prop

str (s : String) : Nat

ints (xs : List Int) : Nat

intLists (xss : List (List Int)) : Nat

draw : Draw → Nat

ax (n : AxNode) : Nat

bytes (b : ByteArray) : Nat

headers (hs : List (String × String)) : Nat

part : Part → Nat

parts (ps : List Part) : Nat

source : Secret.Source → Nat

secret (s : Secret) : Nat

optSecret : Option Secret → Nat

requestBody : Request → Nat

effect : Effect → Nat

subBody : Sub → Nat

subCmd : SubCmd → Nat

textInput : Option TextInput → Nat

list {α : Type} (len : α → Nat) (xs : Array α) : Nat

canvas (c : Canvas) : Nat

menuRecord (m : MenuRecord) : Nat

status (s : StatusFrame) : Nat

surface (s : SurfaceFrame) : Nat

rect (b : ByteArray) (r : Rect) : ByteArray

point (b : ByteArray) (p : Point) : ByteArray

color (b : ByteArray) (c : Color) : ByteArray

ref (b : ByteArray) (c : ControlRef) : ByteArray

range (b : ByteArray) (p : Nat × Nat) : ByteArray

ints (b : ByteArray) (xs : List Int) : ByteArray

intLists (b : ByteArray) (xss : List (List Int)) : ByteArray

draw (b : ByteArray) : Draw → ByteArray

ax (b : ByteArray) (n : AxNode) : ByteArray

textInput (b : ByteArray) : Option TextInput → ByteArray

cursor (b : ByteArray) (c : Cursor) : ByteArray

header1 (b : ByteArray) (kv : String × String) : ByteArray

headers (b : ByteArray) (hs : List (String × String)) : ByteArray

part (b : ByteArray) : Part → ByteArray

parts (b : ByteArray) (ps : List Part) : ByteArray

source (b : ByteArray) : Secret.Source → ByteArray

secret (b : ByteArray) (s : Secret) : ByteArray

optSecret (b : ByteArray) : Option Secret → ByteArray

requestBody (b : ByteArray) : Request → ByteArray

effect (b : ByteArray) : Effect → ByteArray

subBody (b : ByteArray) : Sub → ByteArray

subCmd (b : ByteArray) : SubCmd → ByteArray

wake (b : ByteArray) (w : Option Nat) : ByteArray

list {α : Type} (put : ByteArray → α → ByteArray) (len : α → Nat)
  (b : ByteArray) (xs : Array α) : ByteArray

canvas (b : ByteArray) (c : Canvas) : ByteArray

menuRecord (b : ByteArray) (m : MenuRecord) : ByteArray

status (b : ByteArray) (s : StatusFrame) : ByteArray

surface (b : ByteArray) (s : SurfaceFrame) : ByteArray

frame (f : Frame) : ByteArray

encodeFrame (f : Frame) : ByteArray

decodeFrame (b : ByteArray) : Option Frame

ofCode_code (r : Role) : ofCode (code r) = some r

ofCode_code (c : Cursor) : ofCode (code c) = some c

ofWire_wire (w : FontWidth) : ofWire (wire w) = some w

ofCode_code (c : Corner) : ofCode (code c) = some c

checkedOfCode_code (c : Option Bool) : checkedOfCode (checkedCode c) = some c

ofCode_code (k : Request.Kind) : ofCode (code k) = some k

ofCode_code (p : Permission) : ofCode (code p) = some p

ofCode_code (p : Priority) : ofCode p.code = some p

ofCode_code (t : ScrollTarget) : ofCode t.code t.arg = some t

ofCode_code (k : Key) : ofCode (code k) (scalar k) = some k

scalar_fits (k : Key) : FitsU32 (scalar k)

ofCode_code (m : Mods) : ofCode (code m) = some m

ofCode_code (k : SurfaceKind) : ofCode (code k) = some k

ofCode_code (k : MenuKind) : ofCode (code k) = some k

ofCode_code (c : ScreenChoice) : ofCode (code c) = some c

ofCode_code (a : Anchor) : ofCode (code a) a.offset = some a

fu_iff (n : Nat) : fu n = true ↔ FitsU32 n

fi_iff (v : Int) : fi v = true ↔ FitsI32 v

fs_iff (s : String) : fs s = true ↔ FitsStr s

fitsRef_zero : fitsRef { claim := 0 } = true

fitsRange_zero : fitsRange (0, 0) = true

fu64_iff (n : Nat) : fu64 n = true ↔ FitsU64 n

fi64_iff (v : Int) : fi64 v = true ↔ FitsI64 v

fb_iff (b : ByteArray) : fb b = true ↔ FitsBytes b

expect_enc (bs r : List UInt8) : expect bs (bs ++ r) = some ((), r)

rect_enc {x : Rect} (h : fitsRect x = true) (r : List UInt8) :
  rect (Enc.rect x ++ r) = some (x, r)

point_enc {p : Point} (h1 : FitsI32 p.x) (h2 : FitsI32 p.y)
  (r : List UInt8) : point (Enc.point p ++ r) = some (p, r)

size_enc {s : Size} (h1 : FitsI32 s.w) (h2 : FitsI32 s.h) (r : List UInt8) :
  size (Enc.size s ++ r) = some (s, r)

color_enc (c : Color) (r : List UInt8) :
  color (Enc.color c ++ r) = some (c, r)

ref_enc {c : ControlRef} (h : fitsRef c = true) (r : List UInt8) :
  ref (Enc.ref c ++ r) = some (c, r)

range_enc {p : Nat × Nat} (h : fitsRange p = true) (r : List UInt8) :
  range (Enc.range p ++ r) = some (p, r)

list_enc {α : Type} {d : Dec α} {e : α → List UInt8} (xs : List α)
  (h : ∀ (x : α), x ∈ xs → ∀ (r : List UInt8), d (e x ++ r) = some (x, r))
  (hn : FitsU32 xs.length) (hb : FitsU32 (List.flatMap e xs).length) (r : List UInt8) :
  d.list (Enc.list e xs ++ r) = some (xs, r)

ints_enc {xs : List Int} (h : fitsInts xs = true) (r : List UInt8) :
  ints (Enc.ints xs ++ r) = some (xs, r)

intLists_enc {xss : List (List Int)} (hn : FitsU32 xss.length)
  (h : ∀ (xs : List Int), xs ∈ xss → fitsInts xs = true) (r : List UInt8) :
  intLists (Enc.intLists xss ++ r) = some (xss, r)

draw_enc {x : Draw} (h : fitsDraw x = true) (r : List UInt8) :
  draw (Enc.draw x ++ r) = some (x, r)

ax_enc {x : AxNode} (h : fitsAx x = true) (r : List UInt8) :
  ax (Enc.ax x ++ r) = some (x, r)

textInput_enc {x : Option TextInput} (h : Option.all fitsTextInput x = true)
  (r : List UInt8) : textInput (Enc.textInput x ++ r) = some (x, r)

cursor_enc (c : Cursor) (r : List UInt8) :
  cursor (Enc.cursor c ++ r) = some (c, r)

header1_enc {kv : String × String} (h : (fs kv.fst && fs kv.snd) = true)
  (r : List UInt8) : header1 (Enc.header1 kv ++ r) = some (kv, r)

headers_enc {hs : List (String × String)} (h : fitsHeaders hs = true)
  (r : List UInt8) : headers (Enc.headers hs ++ r) = some (hs, r)

part_enc {x : Part} (h : fitsPart x = true) (r : List UInt8) :
  part (Enc.part x ++ r) = some (x, r)

optSecret_enc {s : Option Secret} (h : Option.all fitsSecret s = true)
  (r : List UInt8) : optSecret (Enc.optSecret s ++ r) = some (s, r)

parts_enc {ps : List Part} (hn : FitsU32 ps.length)
  (h : ∀ (p : Part), p ∈ ps → fitsPart p = true) (r : List UInt8) :
  parts (Enc.parts ps ++ r) = some (ps, r)

requestBody_enc {q : Request} (h : fitsRequest q = true) (r : List UInt8) :
  requestBody q.redact q.kind (Enc.requestBody q ++ r) = some (q, r)

effect_enc {x : Effect} (h : fitsEffect x = true) (r : List UInt8) :
  effect (Enc.effect x ++ r) = some (x, r)

subCmd_enc {x : SubCmd} (h : fitsSubCmd x = true) (r : List UInt8) :
  subCmd (Enc.subCmd x ++ r) = some (x, r)

wake_enc {w : Option Nat} (h : Option.all fu64 w = true) (r : List UInt8) :
  wake (Enc.wake w ++ r) = some (w, r)

length_le_flatMap {α : Type} (e : α → List UInt8) {xs : List α} {x : α}
  (h : x ∈ xs) : (e x).length ≤ (List.flatMap e xs).length

canvas_enc {c : Canvas} (h : fitsCanvas c = true)
  (hs : (Enc.canvas c).length < 4294967296) (r : List UInt8) :
  canvas (Enc.canvas c ++ r) = some (c, r)

menuRecord_enc {m : MenuRecord} (h : fitsMenuRecord m = true)
  (r : List UInt8) : menuRecord (Enc.menuRecord m ++ r) = some (m, r)

status_enc {s : StatusFrame} (h : fitsStatus s = true)
  (hs : (Enc.status s).length < 4294967296) (r : List UInt8) :
  status (Enc.status s ++ r) = some (s, r)

surface_enc {s : SurfaceFrame} (h : fitsSurface s = true)
  (hs : (Enc.surface s).length < 4294967296) (r : List UInt8) :
  surface (Enc.surface s ++ r) = some (s, r)

frame_enc {f : Frame} (h : fitsFrame f = true) (hs : SizeOk f)
  (r : List UInt8) : frame (Enc.frame f ++ r) = some (f, r)

foldl_add {α : Type} (len : α → Nat) (xs : List α) (n : Nat) :
  List.foldl (fun n x => n + len x) n xs = n + (List.map len xs).sum

str_eq (s : String) : str s = (Enc.str s).length

length_flatMap_i32 (xs : List Int) :
  (List.flatMap Enc.i32 xs).length = 4 * xs.length

ints_eq (xs : List Int) : ints xs = (Enc.ints xs).length

intLists_eq (xss : List (List Int)) :
  intLists xss = (Enc.intLists xss).length

draw_eq (d : Draw) : draw d = (Enc.draw d).length

ax_eq (n : AxNode) : ax n = (Enc.ax n).length

bytes_eq (b : ByteArray) : bytes b = (Enc.bytes b).length

headers_eq (hs : List (String × String)) :
  headers hs = (Enc.headers hs).length

part_eq (p : Part) : part p = (Enc.part p).length

parts_eq (ps : List Part) : parts ps = (Enc.parts ps).length

optSecret_eq (s : Option Secret) : optSecret s = (Enc.optSecret s).length

requestBody_eq (r : Request) : requestBody r = (Enc.requestBody r).length

effect_eq (e : Effect) : effect e = (Enc.effect e).length

subCmd_eq (c : SubCmd) : subCmd c = (Enc.subCmd c).length

textInput_eq (t : Option TextInput) : textInput t = (Enc.textInput t).length

list_eq {α : Type} (len : α → Nat) (e : α → List UInt8)
  (h : ∀ (x : α), len x = (e x).length) (xs : Array α) :
  list len xs = (List.flatMap e xs.toList).length

canvas_eq (c : Canvas) : canvas c = (Enc.canvas c).length

menuRecord_eq (m : MenuRecord) : menuRecord m = (Enc.menuRecord m).length

status_eq (s : StatusFrame) : status s = (Enc.status s).length

surface_eq (s : SurfaceFrame) : surface s = (Enc.surface s).length

rect_data (b : ByteArray) (r : Rect) :
  (rect b r).data.toList = b.data.toList ++ Enc.rect r

point_data (b : ByteArray) (p : Point) :
  (point b p).data.toList = b.data.toList ++ Enc.point p

color_data (b : ByteArray) (c : Color) :
  (color b c).data.toList = b.data.toList ++ Enc.color c

ref_data (b : ByteArray) (c : ControlRef) :
  (ref b c).data.toList = b.data.toList ++ Enc.ref c

range_data (b : ByteArray) (p : Nat × Nat) :
  (range b p).data.toList = b.data.toList ++ Enc.range p

foldl_data' {α : Type} (put : ByteArray → α → ByteArray) (e : α → List UInt8)
  (h : ∀ (b : ByteArray) (x : α), (put b x).data.toList = b.data.toList ++ e x)
  (xs : List α) (b : ByteArray) :
  (List.foldl put b xs).data.toList = b.data.toList ++ List.flatMap e xs

ints_data (b : ByteArray) (xs : List Int) :
  (ints b xs).data.toList = b.data.toList ++ Enc.ints xs

intLists_data (b : ByteArray) (xss : List (List Int)) :
  (intLists b xss).data.toList = b.data.toList ++ Enc.intLists xss

draw_data (b : ByteArray) (d : Draw) :
  (draw b d).data.toList = b.data.toList ++ Enc.draw d

ax_data (b : ByteArray) (n : AxNode) :
  (ax b n).data.toList = b.data.toList ++ Enc.ax n

textInput_data (b : ByteArray) (t : Option TextInput) :
  (textInput b t).data.toList = b.data.toList ++ Enc.textInput t

cursor_data (b : ByteArray) (c : Cursor) :
  (cursor b c).data.toList = b.data.toList ++ Enc.cursor c

header1_data (b : ByteArray) (kv : String × String) :
  (header1 b kv).data.toList = b.data.toList ++ Enc.header1 kv

headers_data (b : ByteArray) (hs : List (String × String)) :
  (headers b hs).data.toList = b.data.toList ++ Enc.headers hs

part_data (b : ByteArray) (p : Part) :
  (part b p).data.toList = b.data.toList ++ Enc.part p

parts_data (b : ByteArray) (ps : List Part) :
  (parts b ps).data.toList = b.data.toList ++ Enc.parts ps

source_data (b : ByteArray) (s : Secret.Source) :
  (source b s).data.toList = b.data.toList ++ Enc.source s

secret_data (b : ByteArray) (s : Secret) :
  (secret b s).data.toList = b.data.toList ++ Enc.secret s

optSecret_data (b : ByteArray) (s : Option Secret) :
  (optSecret b s).data.toList = b.data.toList ++ Enc.optSecret s

requestBody_data (b : ByteArray) (r : Request) :
  (requestBody b r).data.toList = b.data.toList ++ Enc.requestBody r

subCmd_data (b : ByteArray) (c : SubCmd) :
  (subCmd b c).data.toList = b.data.toList ++ Enc.subCmd c

wake_data (b : ByteArray) (w : Option Nat) :
  (wake b w).data.toList = b.data.toList ++ Enc.wake w

effect_data (b : ByteArray) (e : Effect) :
  (effect b e).data.toList = b.data.toList ++ Enc.effect e

foldl_data {α : Type} (put : ByteArray → α → ByteArray) (e : α → List UInt8)
  (h : ∀ (b : ByteArray) (x : α), (put b x).data.toList = b.data.toList ++ e x)
  (xs : List α) (b : ByteArray) :
  (List.foldl put b xs).data.toList = b.data.toList ++ List.flatMap e xs

list_data {α : Type} (put : ByteArray → α → ByteArray) (len : α → Nat)
  (e : α → List UInt8)
  (h : ∀ (b : ByteArray) (x : α), (put b x).data.toList = b.data.toList ++ e x)
  (hl : ∀ (x : α), len x = (e x).length) (b : ByteArray) (xs : Array α) :
  (list put len b xs).data.toList = b.data.toList ++ Enc.list e xs.toList

canvas_data (b : ByteArray) (c : Canvas) :
  (canvas b c).data.toList = b.data.toList ++ Enc.canvas c

menuRecord_data (b : ByteArray) (m : MenuRecord) :
  (menuRecord b m).data.toList = b.data.toList ++ Enc.menuRecord m

status_data (b : ByteArray) (s : StatusFrame) :
  (status b s).data.toList = b.data.toList ++ Enc.status s

surface_data (b : ByteArray) (s : SurfaceFrame) :
  (surface b s).data.toList = b.data.toList ++ Enc.surface s

frame_data (f : Frame) : (frame f).data.toList = Enc.frame f

encodeFrame_eq_put : encodeFrame = Wire.Put.frame

decodeFrame_encodeFrame (f : Frame) (h : Wire.fitsFrame f = true)
  (hs : (encodeFrame f).size < 4294967296) : decodeFrame (encodeFrame f) = some f