Commit ac390d1
test(kr-7): generator-index must be positive (no
KR-7 from PROOF-NARRATIVE.md §3: `sigma N`, `sigma_inv N`, `cup N`,
`cap N` must be accepted iff N >= 1.
The canonical parser in `KRLAdapter.jl` raises a "zero index" error
for `sigma 0` etc., and negative indices are outside the lexer's
positive-Int recognition. The smoke test now asserts that no
committed example contains such a pattern.
Added check 4b in tests/smoke/grammar_smoke.sh:
- Grep examples for `<gen> 0` — fail if present.
- Grep examples for `<gen> -<digits>` — fail if present.
- Report pass for examples with no violation.
This is a positive smoke check, not a parser-correctness proof; full
KR-7 discharge requires a parser-level property test (deferred to
follow-up — see PROOF-NEEDS.md TG-K3 entry). The smoke version
catches accidental commits of malformed examples and stays in the
existing lexical-level CI lane.
Verified locally:
- Original 4 examples: 20 passing checks (was 16; added 1 KR-7
pass per file × 4 files).
- Synthetic example `let bad = (sigma 0); close bad;` correctly
fails with "generator with zero index violates KR-7 (sigma 0)".
Cross-references:
- PROOF-NARRATIVE.md KR-7 (added in PR #23)
- ASSUMPTIONS.md A-KR-2.1
- TEST-NEEDS.md TG-K3 (added in PR #23)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>sigma 0, no negative index) (#25)1 parent 5759584 commit ac390d1
1 file changed
Lines changed: 20 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
118 | 118 | | |
119 | 119 | | |
120 | 120 | | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
| 126 | + | |
| 127 | + | |
| 128 | + | |
| 129 | + | |
| 130 | + | |
| 131 | + | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
| 137 | + | |
| 138 | + | |
| 139 | + | |
| 140 | + | |
121 | 141 | | |
122 | 142 | | |
123 | 143 | | |
| |||
0 commit comments