model-testing harness + dict, module constants, multi-variant fields
Adds a soundness harness for the trusted models and three coverage features.
Model library + differential testing.
The FFI-leaf / primitive models (gleam.Int, gleam.List type aliases; gleam.int /
gleam.string / gleam.uri / gleam.dict functions) were per-file injected string
blocks that were only type-checked when a generated file happened to use them.
They now live in one `Proofs/GleamModels.lean` library that `glean prove`
materializes and every generated module imports (`add_models_import` inserts the
import after the engine's own imports). So all models are lake-checked once, and
`Proofs/ModelChecks.lean` `#guard`s them against Gleam's semantics at build time.
This immediately caught two real soundness bugs:
- integer div/rem used Lean's `/`/`%`, which are Euclidean, but Gleam truncates
toward zero (`-7 / 2 = -3`); switched to `Int.tdiv`/`Int.tmod`.
- `string.drop_start` used `s.drop`, which returns `String.Slice` in Lean 4.29,
not `String` (this model had never once been type-checked); added `.toString`.
gleam/dict.
`Dict(k, v)` is `@external`, so it's modeled as a Lean assoc list `List (k × v)`,
wired as an intrinsic with get/size/has_key. The dynamic tier (dynamic/decode/
json) is deliberately left as stubs: it's runtime type inspection for the
unextractable eval half (pruned from proof cones), and modeling it would grow the
trusted surface for no proving benefit.
Module constants.
A `const` reference carries its literal value inline, so it's inlined at each use
(no separate def / reachability). `lower_guard_constant` generalized to
`lower_constant`, handling Int/Float/String/Bool/Tuple/List and nesting.
Multi-variant field access.
`s.field` on a 2+ constructor type has no THIR projection form, so it desugars to
a `match` binding the shared field per constructor and returning it (new
`Ctx::adt_type_ctors` type→constructors registry). The single-constructor
projection path is unchanged.
edouard.paris