Skip to content

test(kr-7): generator index must be positive (no sigma 0, no negative)#25

Merged
hyperpolymath merged 1 commit into
mainfrom
tests/kr-7-generator-index-positive
Jun 1, 2026
Merged

test(kr-7): generator index must be positive (no sigma 0, no negative)#25
hyperpolymath merged 1 commit into
mainfrom
tests/kr-7-generator-index-positive

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Implements KR-7 from PROOF-NARRATIVE.md §3 (added in PR #23):

sigma N, sigma_inv N, cup N, cap N are accepted iff N >= 1.

The canonical parser in KRLAdapter.jl already raises a "zero index" error for sigma 0, and negative indices fall outside the lexer's positive-Int recognition. This PR adds a smoke-test assertion that no committed example contains either pattern.

What's added

tests/smoke/grammar_smoke.sh check 4b — for each .krl example:

  • Grep for <gen> 0 (whitespace-separated zero index). Fail if present.
  • Grep for <gen> -<digits> (negative index). Fail if present.
  • Report a positive check when the file contains no violation.

Verification

Locally:

Run Result
Original 4 examples 20 passing checks (was 16; +1 KR-7 pass per file × 4 files)
Synthetic let bad = (sigma 0); close bad; Correctly fails with generator with zero index violates KR-7 (sigma 0)

What this does NOT do

This is a smoke check, not a parser-correctness proof. The full KR-7 discharge requires a parser-level property test (deferred — see TEST-NEEDS.md TG-K3 entry added in PR #23). The smoke version catches accidental commits of malformed examples and stays in the existing lexical-level CI lane.

Cross-references

Test plan

  • Original examples pass (20/20 checks, was 16/16).
  • Synthetic violation caught.
  • GPG-signed commit.
  • Edited file passes the global pre-commit Owner check (shell script — license header preserved).
  • Auto-merge with squash + branch delete.

🤖 Generated with Claude Code

…ve index)

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>
@hyperpolymath hyperpolymath enabled auto-merge (squash) June 1, 2026 12:23
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Jun 1, 2026

🔍 Hypatia Security Scan

Findings: 71 issues detected

Severity Count
🔴 Critical 4
🟠 High 7
🟡 Medium 60

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dependabot-automerge.yml",
    "type": "missing_timeout_minutes",
    "file": "dependabot-automerge.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit ac390d1 into main Jun 1, 2026
22 of 23 checks passed
@hyperpolymath hyperpolymath deleted the tests/kr-7-generator-index-positive branch June 1, 2026 12:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant