Cairn.Frame.Dump
lean/Cairn/Frame/Dump.lean
A canonical text dump of frames and events (docs/frame.md, "Canonical dump"). The Swift
decoder's tests print the same format and compare it line for line with Lean's, and it is a
readable form for the debug socket. Strings print printable ASCII as itself and every other
Unicode scalar, " and \ as \u{HEX}.
Secrets a person typed never print. A secure field's text is bullets before it reaches a frame
(Cairn.Text.SecureField.view), so its draws and text input print one \u{2022} per scalar and
its accessibility node no value (secure_frame: a dump depends on a secure field's text only
through its length). A request marked redact prints its URL, headers and body as
<redacted N bytes>, N their UTF-8 and byte lengths together.
Imports Cairn.Frame.Events, Cairn.Frame.Build, Cairn.Text.Field
Definitions 30
hexDigits (n : Nat) : String
str (s : String) : String
rect (r : Rect) : String
color (c : Color) : String
ref (c : ControlRef) : String
opt {α : Type} (f : α → String) : Option α → String
range (p : Nat × Nat) : String
bit (b : Bool) : String
draw : Draw → String
ax (n : AxNode) : String
textInput : Option TextInput → String
bytes (b : ByteArray) : String
Bytes as x and two lowercase hex digits each.
headers (hs : List (String × String)) : String
part : Part → String
secret (s : Secret) : String
redactedBytes (u : String) (hs : List (String × String)) (b : ByteArray) : Nat
The bytes a redacted request hides: its URL, header names and values, and body.
request : Request → String
effect : Effect → String
subCmd : SubCmd → String
reply : Reply → String
canvas (c : Canvas) : String
shortcut (s : Shortcut) : String
status (s : StatusFrame) : String
surface (s : SurfaceFrame) : String
frame (f : Frame) : String
One line per item, each ending in a newline.
subEvent : SubEvent → String
event : Event → String
events (es : Array Event) : String
occurs (needle s : String) : Bool
Whether needle occurs in s.
Theorems 2
secure_frame (render : FieldView → Frame) {f g : Text.SecureField} (h : f.Agree g) (focused : Bool) : frame (render (f.view focused)) = frame (render (g.view focused))
No secure text in a dump. However a frame is built from a secure field's view, its dump
is the same for any two fields that agree on everything but which scalars were typed
(Text.SecureField.Agree): the dump carries the text's length and nothing else of it.
secure_canvas (render : FieldView → Canvas) {f g : Text.SecureField} (h : f.Agree g) (focused : Bool) : canvas (render (f.view focused)) = canvas (render (g.view focused))
The same for a single canvas, as the debug socket and the decoder tests print it.