Conversation
341 declined to hand-write Lean models, reasoning that a faithful model
might make its theorem false and that a red build would then be
indistinguishable from a transcription error. An audit of the existing
models found the same thing from the other side.
`specs/tri/utils/args.t27` declares `fn parse(allocator: std.mem.Allocator)`
-- one parameter. Its model declares three, the dotted path split on its
dots, and the env was given `("Std", [("value", .u32)])` to match: a name
in zero of the 650 specs and exactly once in the Lean file.
The fabrication is load-bearing. `Ty.isLowerableFuel` rejects a `.struct`
with empty fields, so a faithful model is not lowerable and the theorem
is false. `icarus-lowerable` on that spec prints `not_lowerable`, and
`t27c parse` shows one parameter with the dotted path intact, so the
split is not mirroring the AST either.
16 models carry the split. Fifteen assert `= false`, where a wrong model
changes nothing. The one asserting `= true` is the one where the
fabrication decides the answer.
An unfaithful model is worse than an empty one: the 114 empty models
announce themselves, and this one lists four correctly-named functions
in spec order and looks checked.
Refs #2893
gHashTag
enabled auto-merge (squash)
August 29, 2026 21:48
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
One section from #2893.
§341 declined to hand-write four Lean models, reasoning that a faithful model might make its theorem false, and that a red build would then be indistinguishable from a transcription error. An audit of the existing models found the same thing from the other side, and it is sharper than the argument.
specs/tri/utils/args.t27declaresfn parse(allocator: std.mem.Allocator)— one parameter. Its Lean model declares three:The dotted type path was split on its dots. And the env was given a struct to match —
("Std", [("value", .u32)])— a name that appears in zero of the 650 specs and exactly once in the Lean file.That fabrication is what makes the theorem provable.
Ty.isLowerableFuelrejects a.structwhose fields are empty, so a faithful model — one parameter of the undeclared typestd.mem.Allocator— is not lowerable and the theorem isfalse. The compiler agrees:icarus-lowerableprintsnot_lowerable. Andt27c parseshows one parameter with the dotted path intact, so the split is not mirroring the AST either.The same split appears in 16 models. Fifteen assert
= false, where a wrong model changes nothing. The one asserting= trueis the one where the fabrication decides the answer.An unfaithful model is worse than an empty one. The 114 empty models announce themselves —
functions := []says the theorem is about nothing. This one lists four functions, all named correctly, in spec order, with tests populated. It looks checked.And the risk §341 declined to take was real, in the direction it predicted: not I might transcribe it wrong and CI would tell me, but somebody already did, and no instrument has told anybody, because nothing builds these proofs.
Refs #2893