[humuhumu33]

#276, first member: SL-08, hexadecimal and decimal (LexLeanStd.Numeral) — draft

Refs #276 (plan in the claim), #92.

What it adds

stdlib/src/Numeral.lex.tex, five production roots for rust-std, each held to the compiler's own reading (stage 0), not to a crate:

Root	Oracle
decimal : Nat -> Bytes	u64::to_string
hexNat : Nat -> Bytes	format!("{:x}") of a u64
parseDecimal : Bytes -> Option Nat	none unless canonical_digits, then u64::from_str; past the width, an overflow on both sides
hex : Bytes -> Bytes	two lowercase digits per byte, as Sha256Digest::to_hex
parseHex : Bytes -> Option Bytes	none unless canonical_hex, then the digit pairs

The readers refuse exactly what the front end refuses: a leading zero, a sign, white space, an uppercase digit, an odd length.

The case, crates/conformance/src/cases/stdlib_numeral.rs, runs in this order:

1. Eligibility, with each root's declared effects equal to its realized effects.
2. The evaluator differential (600 runs per root), then the round trips parseDecimal (decimal n) = some n and parseHex (hex b) = some b.
3. The rustc differential (3,000 runs per root).
4. The plant: hexValue reads letters one too high.
5. The export under the pinned Lean against the committed packages.

The corpus mixes numbers across the u64 range with canonical, mutated and arbitrary text.

Register rows: model/ids.toml, SPEC §31 and a §17.22 paragraph, CONFORMANCE.md, the scenario, CHANGELOG, VERIFICATION.md (the plant record), and the count at 444 in README, SPEC, repository.rs and spec_links.rs. tests/production-export/stdlib/roots.json gains the five roots. The locks of stdlib, bootstrap and examples/helpdesk move with the new entrypoint.

Left to the regeneration

This PR moves identities: the stdlib project's source ID changes, so every stdlib package's sources field moves; the programs of Text and Sha256 do not change. The PR carries the hand-written part only. These are not committed and wait for your wave:

• stdlib/expected/** (build goldens and verify records);
• tests/production-export/stdlib/packages/**;
• the bootstrap and helpdesk records the locks move.

SL-05 is #253's Buffer on this line, and release/v0.5 already has SL-05..SL-07. This row is SL-08 to stay clear of both.

Local evidence (WSL, normative host, head e7f942c7c on release/v0.4 9796067)

• cargo fmt --all -- --check, cargo xtask validate-model (444 ids), cargo xtask validate-spec-links (444 rows), cargo test -p repo-conformance --test bdd (5 passed), cargo clippy -p repo-conformance -p xtask --all-targets --all-features -D warnings: green.
• stdlib: lexlean fmt --check, check, build green. All five roots are eligible, with declared effects equal to realized effects.
• With the stdlib export regenerated locally (all 14 roots certified under Lean 4.32.1, 6 min; not committed):
  • conformance_sl_08 passes in 296 s.
  • conformance_sl_01 and conformance_sl_02 pass in 423 s together.
• Without the regenerated export, the case stops at stack_bounds::observe ("stdlib/decimal is no package of the committed exports"), as expected until the regeneration.
• The plant: parseHex disagrees on 250 of 600 runs. A pair containing f reads as empty bytes because f becomes 16.

Not run locally: golden, examples and production-export (their records are the regeneration's), repro, deny, and the full workspace lint/test.

After it lands

The private copies of these functions move to this module, by each module's owner: decimal in CalculusCheck, RustValidate, AxiomOutput, PrimitiveScan and Buffer; hex in CalculusCheck, RustPrint, TokenAudit, PrimitiveScan and Sha256. Next under #276: Order (SL-09).

🤖 Generated with Claude Code