feat(formal): close the atom-matching gap — antonyms, guard-implication closure, coverage gating#1
Merged
Conversation
…on closure, coverage gating One root cause behind the v0.1.0 field report: the formal tier only reasoned about atoms that already match, and every mismatch signal was capped below the error gate. These six changes widen what shares an atom (so the sound machinery sees more) and make the tool honest about what it could not check — without ever letting a fuzzy score touch a verdict. #1 Doc-committed antonym table + top-level `antonym add/remove/list` command. Mirrors the synonym glossary; folds seed + doc pairs through the existing signed union-find; validates polarity-consistency at write time so the check path stays throw-free. open/shut, grant/deny now reduce to same-atom-opposite- polarity and the SMT tier proves the conflict. (schema.antonyms defaults to [], backward-compatible; no SCHEMA_VERSION bump.) #2 Guard-implication closure (src/formal/guard-implication.ts). A bridge requirement ("while authenticated, be verified") is re-encoded as `bridgeId => (context => stateAsGuard)` and added to the whole-spec conjunction, so the solver computes the transitive closure and names the bridge in the unsat core. Sound: fixed state-establishment verb lexicon + exact-guard-match inert-drop; only re-expresses implications the doc asserts. #3 Numeric same-quantity matching via the committed glossary as a quantity-alias map — "keep valid for" ≡ "expire after" now land on one Real variable so the LIA/LRA tier fires. #4 `check --strict` / `--fail-on-unmatched <n>` gate coverage signals; new EXIT_INCONCLUSIVE (3) for an otherwise error-free run that verified nothing. #5 First-class `data.verified: true|false` — distinguishes "verified clean" from "nothing could be checked". Computed from a DECIDE-tier predicate, so a propose-only fuzzy finding never flips it or softens --strict. #6 Propose-only FND_OPPOSITION_CANDIDATE under --semantic: structural (same-object/different-verb) proposal suggesting `antonym add`, with an explicit synonym-trap warning offering `glossary add` as the alternative. Adversarial review (opus critic, two passes) confirmed #2 and #6 are sound — no constructible false FND_CONTRADICTION, no fuzzy score reaching a verdict — and drove two hardening fixes (the verified/strict split and the opposition message). 916 → 963 tests; biome, tsc, knip, AGENTS.md-drift, build all green. 3 new ERPAVal architecture lessons under .erpaval/solutions/.
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.
Closes the v0.1.0 field-report root cause: the formal tier only reasoned about atoms that already match, and every mismatch signal was capped below the error gate. Six changes widen what shares an atom and make the tool honest about what it could not check — never letting a fuzzy score touch a verdict.
What shipped
antonym add/remove/list— open/shut, grant/deny now provable (write-time polarity-consistency validation;schema.antonymsdefaults to[], no version bump).src/formal/guard-implication.ts) — a bridge requirement links a guard to an established state, so transitive conflicts become provable with the bridge named in the unsat core. Sound: fixed verb lexicon + exact-guard-match inert-drop.check --strict/--fail-on-unmatched <n>gate coverage signals → newEXIT_INCONCLUSIVE(3).data.verified: true|false(decide-tier predicate — a propose-only finding never flips it or softens--strict).FND_OPPOSITION_CANDIDATEunder--semantic, with a synonym-trap warning offeringglossary addas the alternative.Validation
FND_CONTRADICTION, no fuzzy score reaching a verdict. Drove two hardening fixes (verified/strict split, opposition message)..erpaval/solutions/.