Cairn.Fuzz.Metrics
lean/Cairn/Fuzz/Metrics.lean
Random text metrics, valid by construction
Layout and text theorems quantify over every TextMetrics that is Valid, so the fuzzer
shouldn't test with the mono stand-in only. random seed gives each font its own widths:
each scalar's width is a hash of the seed, the font and the scalar, between 30% and 90% of the
font size (wider for CJK and emoji), and 0 for combining marks and zero-width joiners;
offsets are their prefix sums. Ascent and descent are random fractions of the size.
random_valid proves every such metrics Valid.
Imports Cairn.Fuzz.Rng, Cairn.Font, Cairn.Layout.Proofs
Inductive types 1
MetricsChoice : Type
The metrics a sequence runs with: random from a seed, or the mono stand-in.
mono : MetricsChoice
random (seed : UInt64) : MetricsChoice
Definitions 9
sums (acc : Int) : List Nat → List Int
Prefix sums from acc: one more entry than widths, starting at acc, never decreasing.
zeroWidth (c : Char) : Bool
Scalars that take no width: combining marks, variation selectors, joiners.
wide (c : Char) : Bool
Wide scalars: CJK and emoji.
fontKey (f : Font) : UInt64
charWidth (seed : UInt64) (f : Font) (c : Char) : Nat
fraction (seed : UInt64) (f : Font) (salt : UInt64) (lo hi : Nat) : Nat
randomMetrics (seed : UInt64) : TextMetrics
Random metrics from a seed.
metrics : MetricsChoice → TextMetrics
gen : Gen MetricsChoice
One sequence in eight uses mono.
Theorems 5
sums_length (acc : Int) (ws : List Nat) : (sums acc ws).length = ws.length + 1
sums_ge (ws : List Nat) (acc : Int) (i : Nat) (h : i < (sums acc ws).length) : acc ≤ (sums acc ws)[i]
sums_mono (ws : List Nat) (acc : Int) (i j : Nat) (hi : i < (sums acc ws).length) (hj : j < (sums acc ws).length) : i ≤ j → (sums acc ws)[i] ≤ (sums acc ws)[j]
random_valid (seed : UInt64) : (randomMetrics seed).Valid
valid (c : MetricsChoice) : c.metrics.Valid
Instances 2
instReprMetricsChoice : Repr MetricsChoice
instInhabitedMetricsChoice : Inhabited MetricsChoice