[humuhumu33]

Resolves #263 (draft). Targets release/v0.5.

The three lemmas, as shipped

They are theorems of the native runtime module LexLeanRuntime.Laws, registered in language/runtime-1.2/laws.toml as laws a language-1.2 law proof applies by name. No raw Lean is involved (§16.12). Each conclusion is an implication from a bound on the input. Each closed side condition is a premise that a prior theorem discharges.

theorem splitExact_fits (s d : String) (m : UInt32) (n : Nat)
    (hd : LexLeanRuntime.equal d "" = false) (hn : n < m.toNat) :
    LexLeanRuntime.length (LexLeanRuntime.utf8Encode s) ≤ n →
      (match LexLeanRuntime.splitExact s d m with
        | none => false
        | some _ => true) = true

theorem utf8Decode_length (b : ByteArray) (s : String) (n : Nat) :
    LexLeanRuntime.utf8Decode b = some s → LexLeanRuntime.length b ≤ n →
      LexLeanRuntime.length (LexLeanRuntime.utf8Encode s) ≤ n

theorem checkedAdd_fits (a b n : UInt32) (hn : n.toNat + b.toNat < 4294967296) :
    a ≤ n →
      (match LexLeanRuntime.checkedAdd a b with
        | none => false
        | some _ => true) = true

Law name	Lean	Axioms
split_exact_fits	LexLeanLaws.splitExact_fits	Classical.choice, Quot.sound, propext
utf8_decode_length	LexLeanLaws.utf8Decode_length	Classical.choice, Quot.sound, propext
checked_add_fits	LexLeanLaws.checkedAdd_fits	Quot.sound, propext

The first two observe Classical.choice because the runtime definitions of split_exact and utf8_decode pin it.

The piece count is proved from splitOnAux_length_le: the loop of String.splitOn emits at most the string's UTF-8 byte length plus one pieces. The proof is a recursion on the loop's own termination measure.

Reading of the issue's second lemma: the issue says "the UTF-8 byte length is bounded by the encoded length". It ships as "a string decoded from b has a UTF-8 byte length of at most length b". This is the step from the request's bytes to the decoded text that both prism-code guards need.

The mirror module

examples/fold-laws/src/Guards.lex.tex mirrors prism-code's three guards and proves each branch unreachable. Each proof is one law application:

theorem{
  name: too_many_lines_unreachable,
  parameters: [text : String],
  statement: (((prim length (prim utf8_encode text : Bytes) : Nat) <= 4096) -> ((match (prim split_exact text "\n" (4097 : UInt32) : (Option (List String)))
    | Option.none => false
    | Option.some pieces => true) = true)),
  proof: law{
    name: split_exact_fits,
    arguments: [text, "\n", (4097 : UInt32), 4096],
    premises: [newline_separates, lines_fit]
  },
  axioms: [Classical.choice, Quot.sound, propext]
}

theorem{
  name: line_overflow_unreachable,
  parameters: [line : UInt32],
  statement: ((line <= (4097 : UInt32)) -> ((match (prim checked_add line (1 : UInt32) : (Option UInt32))
    | Option.none => false
    | Option.some next => true) = true)),
  proof: law{
    name: checked_add_fits,
    arguments: [line, (1 : UInt32), (4097 : UInt32)],
    premises: [counter_fits]
  },
  axioms: [Quot.sound, propext]
}

theorem{
  name: response_too_large_unreachable,
  parameters: [request : Bytes, text : String],
  statement: (((prim utf8_decode request : (Option String)) = (ctor Option.some [String] text)) -> (((prim length request : Nat) <= 16384) -> ((prim length (prim utf8_encode text : Bytes) : Nat) <= 16384))),
  proof: law{name: utf8_decode_length, arguments: [request, text, 16384]},
  axioms: [Classical.choice, Quot.sound, propext]
}

request_text_fits gives the same bound at 4096. It is the step from an admitted request to the text that too_many_lines_unreachable takes. lexlean verify src/Guards.lex.tex passes under Lean 4.32.1: verified 1 module; attestation cef84e9408639d951f225171ead32845ab926e74cb2c8edbde53fb8ed118bfd3.

Rows

• PF-24 (new, proofs, §16, §17.12): the runtime bounds, the mirror, and both refusals. Register 443 → 444. README's PF-01..PF-24 row and its count are updated.
• PF-22 (case only, statement unchanged): the fold-law rows stay within Quot.sound and propext. The bound rows are pinned by PF-24 instead.

Plants

They are recorded with their real output in VERIFICATION.md.

Plant	Observed
(a) split_exact_fits weakened by one (premise n + 1 < m.toNat), re-exported and built into the compiler	lexlean verify refuses the mirror: LLV7002 … Application type mismatch: The argument lines_fit … but is expected to have type 4096 + 1 < UInt32.toNat 4097 at Guards.lex.tex:52
(b) the mirror cites split_exact_bound	error[LLT4001]: phase link: \split_exact_bound` is not a registered law`
(c) the piece-count lemma without + 1	Lean refuses it: omega could not prove the goal, then a type mismatch at ≤ s.utf8ByteSize
(d) each guard claims one more than its law gives (4097 bytes, line 4098, response 16383)	three LLV7002 type mismatches, at Guards.lex.tex:52, :74 and :96. conformance_pf_24 runs the same plant.

One design point for afflom

Lean's module system does not expose the bodies of String.splitOn and its loop. A generated native module therefore could not unfold the split. The regenerated Laws was refused at String.splitOnAux.eq_def with "unknown constant", and at splitOn_length_le because the kernel cannot unfold String.splitOn.

This PR adds one line to the decoder of core module 2 (LEAN_CORE_V2_IMPORTS). It imports Init.Data.String.Legacy in full, next to Lean.Meta.Constructions.SparseCasesOn, and SPEC §17.10 says so. The native module still imports only Init and the earlier runtime modules, so RT-01 holds.

The alternative is a runtime split_exact over an exposed split. That would change the runtime and its Rust correspondence, so I did not take it. Please say if you want it the other way.

A related limit: semantic proofs have no have. A chain such as "admitted request, then decoded text, then pieces" is therefore two theorems, not one.

Identity

laws.toml, Laws.lex.tex, and the decoder header are part of the language-1.2 compiler semantics. The 1.2 compiler-semantics ID moves from 5262e5b4… to 9fdf4d30…. Languages 1.0 and 1.1 are unchanged. Locks, goldens, calculus, production export, fixtures, and verification records were regenerated by the repository's writers, in a separate commit. Every sibling PR on release/v0.5 that moves the ID will conflict on those records. The fix is to rerun the writers after merging.

Run locally

• cargo xtask validate-model and validate-spec-links: 444 rows, clean (at the R3 commit).
• lexlean verify src/Guards.lex.tex on the fold-laws example: verified (attestation above).
• The writers check-golden, check-calculus, check-production-export, check-fixtures (each --write) and verify-examples --write without uor-atlas: 18 projects verified.
• conformance_pf_20..pf_24 and conformance_rt_01..rt_04: 9 passed, on the merged head.
• validate-model (444 ids, audits clean) and validate-spec-links on the merged head.
• Not run locally: the whole just vv (workspace clippy and tests, bdd, repro, deny) and the uor-atlas verify. A draft runs only the rest leg in CI.
• Every heavy job ran under the shared lock, inside a systemd-run --user scope capped at 10G (/user.slice/user-1000.slice/user@1000.service/app.slice/run-….scope).

🤖 Generated with Claude Code

[humuhumu33]

Merged release/v0.5 into this branch and regenerated what the merge moved. Head 4dd5ae54d contains the line at 34cfc1282 (#286, #287, #288, #289, #290). GitHub reports it mergeable; CI is re-running. Still a draft.

Commits on top of ae277f358:

• 176b21098 merges 66ae4b358. CHANGELOG and VERIFICATION keep both sides, the line's first.
• f2de3dd23 merges 34cfc1282. Same rule for CHANGELOG and VERIFICATION. README takes the line's text.
• 4dd5ae54d relocks spec/ and examples/performance-corpus and rewrites the golden, fixtures, calculus, production export and the corpus, compiler, stdlib and bootstrap verification records. The language-1.2 ID of this branch stays 9fdf4d30; the line's 5262e5b4 is gone from every non-Markdown file. SPEC.md is the projection of spec/src.

Numbers: PF-24 is still free on the line, so nothing is renumbered. The register is 448 (AU-14, RP-17, PC-01 and PC-02 landed). README's count says 448, its PF row ends at PF-24, and this PR's CHANGELOG entry says Register 448.

Run locally, all green on the final tree: validate-model, validate-spec-links, fmt, check-golden, check-fixtures, check-calculus, and rp_11, pc_01, pc_02, pf_20..24, rt_01. At 176b21098 the fold-laws Guards module also verified.

Not verified: the Atlas (uor-atlas) records are not regenerated. The Guards verify was not rerun on the final tree, nor were the other examples' verification records or just vv whole. check-production-export was written after the last merge but not rerun as a check.

[humuhumu33]

Merged into release/v0.5 at 80bf4bae9 (merge commit) on all 31 checks green with the line contained, under Ilya's merge-on-green rule and his explicit confirmation for this PR. Left open for afflom, as the description states: the decision on the length decoder's full import of the legacy string module, which moved the language-1.2 compiler-semantics ID (9fdf4d30 at the time of writing). #295 and #303 regenerate on top of it. Closing #263 by hand.