Skip to content

fix(checker): replay property steps, cite across files, project fields - #218

Merged
the-homeless-god merged 9 commits into
devfrom
a/1400-fmath-first-statements
Oct 1, 2026
Merged

fix(checker): replay property steps, cite across files, project fields#218
the-homeless-god merged 9 commits into
devfrom
a/1400-fmath-first-statements

Conversation

@the-homeless-god

@the-homeless-god the-homeless-god commented Oct 1, 2026

Copy link
Copy Markdown
Member
  • chore(numbers): sync counts after rebase onto the checker sets
  • docs(tasks): mark task 5583 as in progress
  • chore(numbers): sync counts and raise the probe ratchet to 611
  • docs(tasks): name the assignee and branch of task 5583
  • feat(stdlib): first proved statements of fmath, cited across files
  • chore(numbers): sync counts and raise the probe ratchet to 608
  • chore(numbers): sync counts, ledger rows and file name words
  • docs(tasks): measure the whole standard library and rank its refusals
  • fix(checker): replay property steps, cite across files, project fields

Verified on the tree of dev plus this branch (43b143f): the checker test set passes, the provability verdict is green with all four checks, the proved-share ledger and the rule tables agree with the tree, pre-push is green, commit messages follow the convention.

🤖 Generated with Claude Code

the-homeless-god and others added 9 commits October 1, 2026 23:13
@the-homeless-god @claude
fix(checker): replay property steps, cite across files, project fields
f01b9a3 
A theorem step "by property" naming a postcondition of a called
function was credited by its line binding alone; a forged program whose
body is negative passed with code 0. The step is now replayed: the
checker builds the postcondition instance from the call in the body,
pays the callee's requirements and closes the goal by modus ponens,
under the same guard, or by non-negativity with the instance among the
known facts. What it cannot close stays on the kernel's word.

A property declared in another file is looked up in the given
dependency set: exactly one declaration, its module imported, every
name in the property text declared and visible in that module and not
a local namesake; the module's record is re-checked with the same set
and only what is verified there is taken as a fact. Without a set such
a name is declined, not called a lie.

In an identity node a field of the result is the field of the
constructed value and a field of the argument is the name bound by the
case pattern; the induction hypothesis is taken only on a recursive
field. Before, the goal was rewritten by itself and a false field
identity passed with code 0.

Probes are rows of cases.tsv in the citation and field-projection
families, run by flang/proof/probes/checker-rules/run.fscript; run.sh
is not extended. Ceiling 7815 -> 7938, exactly what was spent.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
docs(tasks): measure the whole standard library and rank its refusals
dd4b718 
The 49 kernel records of the standard library are replayed with their
dependency sets: 1665 of 3671 places verified. The task now ranks the
reasons the checker declines, by count, and says whose work each is:
1618 lines need the record printer to write moves, about 340 are
replay rules the checker lacks. Two printer changes are measured: the
planner limits give 41 places but print a computation over an open
term, and free identity statements lack the measure laws. A kernel
fault is recorded: a restricted postcondition is cited as a fact
outside its restriction.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
chore(numbers): sync counts, ledger rows and file name words
108ef5c 
The new checker probes add 25 sources to the proved-share ledger and
six English words to the file name list; counts quoted in prose and
the tree inventory are re-measured after the rebase onto dev.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
chore(numbers): sync counts and raise the probe ratchet to 608
3387be3 
The citation and field-projection cases are rows of probes.tsv; the
forgery-probe ratchet follows the measured count, 596 to 608. Counts
in prose and the tree inventory are re-measured.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
feat(stdlib): first proved statements of fmath, cited across files
7e7f23a 
flang/stdlib/fmath.flang holds four statements about all values of
their types: the length of any list and of any string is not below
zero, and so are the sum of two non-negative numbers and the sum of
two string lengths. The kernel proves all four and the checker
replays all four.

The checker learns one more replay: a free statement "T not below 0"
that does not mention the result is replayed by the same
non-negativity grammar as a function body, and only names bound to an
interval type count as having a floor; a restriction gives no floor.

An example program cites two of the statements from another file;
with the library given as a dependency the checker verifies both
steps, without it the place is declined. Probes and forgeries are rows
of tests/families/fmath/cases.tsv. Ceiling 7938 -> 7949.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
docs(tasks): name the assignee and branch of task 5583
46f2e52 
The task ledger check refuses a task in progress without an assignee
and a branch; the checker side of 5583 lives on the stdlib branch.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
chore(numbers): sync counts and raise the probe ratchet to 611
76e3066 
The fmath cases are rows of probes.tsv; the forgery-probe ratchet
follows the measured count, 608 to 611. Task 5583 points at the probe
table. Counts in prose and the tree inventory are re-measured.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
docs(tasks): mark task 5583 as in progress
286543a 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god @claude
chore(numbers): sync counts after rebase onto the checker sets
43b143f 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
@the-homeless-god
the-homeless-god merged commit b7aa7d3 into dev Oct 1, 2026
27 checks passed
@the-homeless-god
the-homeless-god deleted the a/1400-fmath-first-statements branch October 1, 2026 23:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@the-homeless-god