Extend pool-based quantifier instantiation to axioms; add diagnostic … - #3
Merged
Conversation
…flags
QI / axioms:
Axioms with {:pool ...} or {:add_to_pool ...} annotations now participate
in pool-based quantifier instantiation. Previously only assume/assert
commands fed the pool machinery, so axiom quantifiers with pool hints
silently did nothing. Lifted-lambda definition axioms stay on the
BindLambdaFunction path to avoid double-instantiation. Per-impl gating
adds PoolHintChecker.HasPoolAxioms so QI is skipped cleanly when an
impl has no sources and no non-lambda pool axioms.
/poolTrace:
Per-impl trace emitted as each implementation runs: pool contents
(pretty-printed via VCExprPrinter), per-quantifier instantiation
counts (keyed by qid), and the count of candidates dropped by
pool-type mismatch. Writes are serialized against parallel-split
races via a static lock on Options.OutputWriter.
/poolSummary:
One-shot audit emitted at verification start: axiom counts (total /
pool-bearing / lambda-definition / plain); quantifier counts (total
/ pool-bearing / polymorphic / plain); per-pool producer/consumer
locations with (!! no producers) / (!! no consumers) warnings for
orphans. Plain axioms and quantifiers are listed exhaustively so
users can grep/sort them when deciding where to add pool hints.
Walks program.Axioms unioned with program.Functions.DefinitionAxioms.
/jsonOutput:<file>:
Structured per-implementation verification results via System.Text.Json
(no new dependencies). Filename "-" routes through Options.OutputWriter
for library-embedding friendliness. Outcome lowercased to match XML.
Handles AssertCounterexample, CallCounterexample (precondition
violations), and ReturnCounterexample (postcondition violations) with
correct location and message for each.
Tests:
Test/inst/axiom.bpl -- pool instantiation via axioms
Test/inst/poolTrace.bpl -- /poolTrace golden output
Test/inst/poolSummary.bpl -- /poolSummary golden output
Test/commandline/jsonOutput.bpl -- /jsonOutput schema check
Full lit suite: 55 pre-existing failures, unchanged by this work.
NUnit: 85 pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The prior patch walked program.Axioms, but Checker.Setup only calls
ctx.AddAxiom on split.PrunedDeclarations. When a user has a hideable
axiom and hides it (via `hide *;` / `hide F;`), pruning removes it
from the prover context. The axiom-antecedent path, however, still
translated the axiom's expression and fed pool-based ground instances
into the VC, smuggling the hidden axiom back in.
This is mathematically sound (the axiom is still a true statement of
the user's theory) but defeats `{:hideable}` / `reveal` as a sanity-
check mechanism — the user asks "is this assertion provable WITHOUT
axiom F?" and the old code silently answered "yes" by using F anyway.
Fix: thread the pruned axiom list (same set Checker.Setup uses) from
Split.cs through Instantiate and into Execute / HasPoolAxioms. Lambda-
definition axioms are still filtered via program.Functions to keep
that classification independent of what any particular split prunes.
Test/inst/axiomPoolHidden.bpl: hideable axiom with a pool hint; hide *
procedure expects failure, revealed procedure expects success. Verified
against the pre-fix baseline that both procedures previously verified
(proving the bug was real) and that post-fix only the revealed one does.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Before: pool-based instantiation of an assume-antecedent forall replaced
the quantifier with its ground instances when /keepQuantifier=false, but
the same flag applied to a pool-bearing axiom only affected what went
into the VC antecedent -- the axiom was *also* unconditionally installed
into the prover context via ctx.AddAxiom, so the full forall survived
and could still fire via E-matching. /keepQuantifier therefore meant
different things for assumes vs. axioms.
Fix: in Checker.Setup, a pool-bearing non-lambda-definition axiom is
skipped from ctx.AddAxiom when /keepQuantifier=false. The axiom then
lives only as its pool-instantiated ground forms in the VC antecedent,
matching the assume path. With /keepQuantifier=true the axiom goes into
the prover context as before.
Users who want both pool hints *and* E-matching on the same axiom should
use /keepQuantifier (or split the axiom -- one annotated version for the
pool, one plain for E-matching). This is a (behavior-changing) trade-off
made explicit: marking an axiom {:pool ...} is now a positive decision
to drive instantiation through pools, not a freebie on top of
E-matching.
Test/inst/axiomPoolKeepQuantifier.bpl: impl that needs the axiom via
E-matching (no pool source). Expected to fail by default and succeed
under /keepQuantifier, demonstrating the symmetric semantics.
Help text for /keepQuantifier updated to document the axiom side.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.
…flags
QI / axioms:
Axioms with {:pool ...} or {:add_to_pool ...} annotations now participate
in pool-based quantifier instantiation. Previously only assume/assert
commands fed the pool machinery, so axiom quantifiers with pool hints
silently did nothing. Lifted-lambda definition axioms stay on the
BindLambdaFunction path to avoid double-instantiation. Per-impl gating
adds PoolHintChecker.HasPoolAxioms so QI is skipped cleanly when an
impl has no sources and no non-lambda pool axioms.
/poolTrace:
Per-impl trace emitted as each implementation runs: pool contents
(pretty-printed via VCExprPrinter), per-quantifier instantiation
counts (keyed by qid), and the count of candidates dropped by
pool-type mismatch. Writes are serialized against parallel-split
races via a static lock on Options.OutputWriter.
/poolSummary:
One-shot audit emitted at verification start: axiom counts (total /
pool-bearing / lambda-definition / plain); quantifier counts (total
/ pool-bearing / polymorphic / plain); per-pool producer/consumer
locations with (!! no producers) / (!! no consumers) warnings for
orphans. Plain axioms and quantifiers are listed exhaustively so
users can grep/sort them when deciding where to add pool hints.
Walks program.Axioms unioned with program.Functions.DefinitionAxioms.
/jsonOutput::
Structured per-implementation verification results via System.Text.Json
(no new dependencies). Filename "-" routes through Options.OutputWriter
for library-embedding friendliness. Outcome lowercased to match XML.
Handles AssertCounterexample, CallCounterexample (precondition
violations), and ReturnCounterexample (postcondition violations) with
correct location and message for each.
Tests:
Test/inst/axiom.bpl -- pool instantiation via axioms
Test/inst/poolTrace.bpl -- /poolTrace golden output
Test/inst/poolSummary.bpl -- /poolSummary golden output
Test/commandline/jsonOutput.bpl -- /jsonOutput schema check
Full lit suite: 55 pre-existing failures, unchanged by this work.
NUnit: 85 pass.