Cairn.Text.Host
lean/Cairn/Text/Host.lean
Core Text metrics from the host, as a TextMetrics.
The host shapes each (font, string) once with Core Text and reports, in whole logical points,
the font's ascent and descent and the caret offset at every Unicode scalar boundary; the
renderer draws glyphs from the very same shaped line (docs/render.md). Lean receives the numbers
as bytes through cairn_lean_text_metrics (lean/c/text_host.c), decodes them, and normalises
them so TextMetrics.host satisfies TextMetrics.Valid by proof, whatever the host sends:
host_valid below. What stays trusted is only that the numbers match what is painted (an
assume, docs/trusted.md).
Linking: the extern symbols live in text_host.o, which Lake links into every executable and
puts in libcairn_Cairn.a. The C function it calls, cairn_text_metrics, is defined weakly
there (returning "no host"), so bench, audit and Lean tests link without the Swift host and
get TextMetrics.mono numbers; the Swift host's strong definition wins when it is linked.
hostLinked () says which one is in use. Never evaluate these at elaboration time (#eval,
#guard): the interpreter has no native implementation to call.
Imports Cairn.Font
Definitions 13
raw (family size weight : UInt32) (style : UInt8) (tracking : UInt32) (s : String) : ByteArray
[ascent, descent, offset_0, …, offset_n] as little-endian int32s (4 * (n + 3) bytes,
n = s.length), or empty when no host is linked.
hostLinked : Unit → Bool
Whether the Swift host's metrics are linked (otherwise raw is always empty).
sat (n : Nat) : UInt32
Font fields cross as UInt32, saturating: a size of 2^40 means "huge", not 2^40 mod 2^32.
The host clamps sizes to 1–1024 and weights to 100–900 itself.
satI (n : Int) : Int
Signed fields (tracking) saturate to the int32 range and cross as its two's complement.
satI32 (n : Int) : UInt32
styleByte (f : Font) : UInt8
The style byte: bit 0 italic, bit 1 tabular digits, bits 2–3 the width's code.
rawFor (f : Font) (s : String) : ByteArray
word (b : ByteArray) (i : Nat) : Int
The ith little-endian int32 of b; bytes past the end read as 0. (b[j]?, not
b.data.getD j: compiled, ByteArray.data copies the whole array, which made decoding a
string's offsets quadratic.)
climb (lo : Int) : List Int → List Int
Running maximum from lo: each entry is at least lo and at least the one before it.
normalise (n : Nat) (b : ByteArray) (fallback : Nat → Int) : Array Int
Offsets from the host's words (or from fallback when the reply has the wrong size):
entry 0 forced to 0, the rest made nondecreasing and nonnegative. For a well-behaved host this
is the identity, and the Swift tests check that it is.
host : TextMetrics
Core Text's metrics, from the host. Falls back to mono when no host is linked.
putI32 (b : ByteArray) (v : Int) : ByteArray
Little-endian int32 bytes of v (two's complement, truncated to 32 bits).
hostCheck (family size weight : UInt32) (style : UInt8) (tracking : UInt32) (s : String) : ByteArray
For the host's end-to-end test (host/Tests/CairnRenderLeanTests): what layout would see for
this font and string through TextMetrics.host, as int32s
[linked, ascent, descent, offset_0, …, offset_n].
Theorems 8
length_climb (lo : Int) (xs : List Int) : (climb lo xs).length = xs.length
le_of_mem_climb (lo : Int) (xs : List Int) (y : Int) : y ∈ climb lo xs → lo ≤ y
pairwise_climb (lo : Int) (xs : List Int) : List.Pairwise (fun x1 x2 => x1 ≤ x2) (climb lo xs)
pairwise_normalised (xs : List Int) :
List.Pairwise (fun x1 x2 => x1 ≤ x2) (0 :: climb 0 xs)
size_normalise (n : Nat) (b : ByteArray) (fb : Nat → Int) : (normalise n b fb).size = n + 1
normalise_zero (n : Nat) (b : ByteArray) (fb : Nat → Int) : (normalise n b fb)[0]? = some 0
normalise_mono (n : Nat) (b : ByteArray) (fb : Nat → Int) (i j : Nat) (hi : i < (normalise n b fb).size) (hj : j < (normalise n b fb).size) (hij : i ≤ j) : (normalise n b fb)[i] ≤ (normalise n b fb)[j]
host_valid : host.Valid
The host's metrics satisfy everything layout assumes, whatever the host returns.