Add OverapproxiatesUpto/OverapproximatesWhen/OverapproximatesAggressivelyWhen#1325
Draft
aqjune-aws wants to merge 1 commit into
Draft
Add OverapproxiatesUpto/OverapproximatesWhen/OverapproximatesAggressivelyWhen#1325aqjune-aws wants to merge 1 commit into
aqjune-aws wants to merge 1 commit into
Conversation
Contributor
Author
|
Hey, this PR is too large. Can we split it into smaller ones? |
Contributor
Author
aqjune-aws
added a commit
that referenced
this pull request
Jun 5, 2026
… check Reworks the small-step semantics of the Imperative dialect (Strata.DL.Imperative) and Core (Strata.Languages.Core) to fix a scoping bug and add a missing measure check. Subset of the changes from PR #1325 — the `OverapproximatesWhen`/`OverapproximatesAggressively`/`InitEnvWF` work is deferred to a follow-up PR. * Evaluator scoping (FIX of a scoping bug — function declarations leaked out of their enclosing block): Inner function declarations (`step_funcDecl`) extend the evaluator (`Env.eval`) with the new function, and previously, that extension persisted past the enclosing block — i.e. a `funcDecl` inside a block was visible to code AFTER the block exited. This is wrong: by the language's variable-scoping rules, a `funcDecl`'s scope is its enclosing block, exactly parallel to `init`. The fix: * `Config.block` now carries a snapshot of the parent evaluator (`e_parent`) in addition to the parent store (`σ_parent`): `Config.block label σ_parent e_parent inner` (was 3-arg). * On `step_block_done` / `step_block_exit_match` / `step_block_exit_mismatch` the result config's `eval` is RESTORED to `e_parent`, so a `funcDecl` introduced inside the block is NOT visible after exit. * The same `Config.block` wrapper is used by `step_ite_*` and `step_loop_*` to scope `ite` branches and loop bodies, so this fix automatically covers `funcDecl`s leaking out of `if`/`else` branches and loop bodies as well. * Implement the missing measure check of a loop in small-step semantics: * `step_loop_enter` / `step_loop_exit` / `step_loop_nondet_*` set `hasMeasureFailure` / `hasInvFailure` flags from the measure / invariants, and OR them into `Env.hasFailure`. * `Stmt.loop` carries an `Option (String × P.Expr)` measure (label + expr) rather than `Option P.Expr`; the label feeds into the assertion-label collection (so a verifier can identify the synthetic measure assertion). * New HasFvars / HasOps / HasOpsImp typeclasses: * `HasFvars` returns ALL free variables in an expression. * `HasOps` (`P.Expr → List P.Ident`) returns operator/function names referenced in an expression, parallel to `HasFvars` for variables. * `HasOpsImp` lifts that to commands (`Cmd.getOps`, `Cmds.getOps`). * Refactoring of HasBool / HasBoolOps: * `HasBool` now extends `HasVal` and bundles `boolIsVal` (former `HasBoolVal` is folded in). * Boolean operations split out into `HasBoolOps` (extends `HasBool`): not, and, imp. * `Strata/DL/Imperative/StmtProps.lean` (new): theorems that depend only on `Stmt.lean` (currently `Stmt.funcDeclNames_eq_nil_of_noFuncDecl` and `Block.funcDeclNames_eq_nil_of_noFuncDecl`). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Contributor
Author
|
#1337 will factor out (1) Updates / fixes in Imperative small-step semantics |
Contributor
Author
|
This pull request will be moved to the internal repository of Strata after migration. |
aqjune-aws
force-pushed
the
jlee/sem-updates
branch
3 times, most recently
from
e820081 to
1e514c3
Compare
aqjune-aws
changed the title
aqjune-aws
force-pushed
the
jlee/sem-updates
branch
2 times, most recently
from
be91096 to
c600d79
Compare
aqjune-aws
force-pushed
the
jlee/sem-updates
branch
2 times, most recently
from
d6fc11e to
a1b8bf8
Compare
kondylidou
pushed a commit
to kondylidou/Strata
that referenced
this pull request
Jun 12, 2026
…1337) Reworks the small-step semantics of Imperative to dix a scoping bug regarding internal function declaration. Subset of the changes from PR strata-org#1325 — the `OverapproximatesWhen`/`OverapproximatesAggressively`/`InitEnvWF` work is deferred to a follow-up PR. * Evaluator scoping (FIX of a scoping bug — function declarations leaked out of their enclosing block): Inner function declarations (`step_funcDecl`) extend the evaluator (`Env.eval`) with the new function, and previously, that extension persisted past the enclosing block — i.e. a `funcDecl` inside a block was visible to code AFTER the block exited. This is wrong: by the language's variable-scoping rules, a `funcDecl`'s scope is its enclosing block, exactly parallel to `init`. The fix: * `Config.block` now carries a snapshot of the parent evaluator (`e_parent`) in addition to the parent store (`σ_parent`): `Config.block label σ_parent e_parent inner` (was 3-arg). * On `step_block_done` / `step_block_exit_match` / `step_block_exit_mismatch` the result config's `eval` is RESTORED to `e_parent`, so a `funcDecl` introduced inside the block is NOT visible after exit. * New HasFvars / HasOps / HasOpsImp typeclasses: * `HasFvars` returns ALL free variables in an expression. * `HasOps` (`P.Expr → List P.Ident`) returns operator/function names referenced in an expression, parallel to `HasFvars` for variables. * `HasOpsImp` lifts that to commands (`Cmd.getOps`, `Cmds.getOps`). * Refactoring of HasBool / HasBoolOps: * `HasBool` now extends `HasVal` and bundles `boolIsVal` (former `HasBoolVal` is folded in). * Boolean operations split out into `HasBoolOps` (extends `HasBool`): not, and, imp. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
shigoel
pushed a commit
that referenced
this pull request
Jun 15, 2026
Reworks the small-step semantics of Imperative to dix a scoping bug regarding internal function declaration. Subset of the changes from PR #1325 — the `OverapproximatesWhen`/`OverapproximatesAggressively`/`InitEnvWF` work is deferred to a follow-up PR. * Evaluator scoping (FIX of a scoping bug — function declarations leaked out of their enclosing block): Inner function declarations (`step_funcDecl`) extend the evaluator (`Env.eval`) with the new function, and previously, that extension persisted past the enclosing block — i.e. a `funcDecl` inside a block was visible to code AFTER the block exited. This is wrong: by the language's variable-scoping rules, a `funcDecl`'s scope is its enclosing block, exactly parallel to `init`. The fix: * `Config.block` now carries a snapshot of the parent evaluator (`e_parent`) in addition to the parent store (`σ_parent`): `Config.block label σ_parent e_parent inner` (was 3-arg). * On `step_block_done` / `step_block_exit_match` / `step_block_exit_mismatch` the result config's `eval` is RESTORED to `e_parent`, so a `funcDecl` introduced inside the block is NOT visible after exit. * New HasFvars / HasOps / HasOpsImp typeclasses: * `HasFvars` returns ALL free variables in an expression. * `HasOps` (`P.Expr → List P.Ident`) returns operator/function names referenced in an expression, parallel to `HasFvars` for variables. * `HasOpsImp` lifts that to commands (`Cmd.getOps`, `Cmds.getOps`). * Refactoring of HasBool / HasBoolOps: * `HasBool` now extends `HasVal` and bundles `boolIsVal` (former `HasBoolVal` is folded in). * Boolean operations split out into `HasBoolOps` (extends `HasBool`): not, and, imp. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
shigoel
pushed a commit
that referenced
this pull request
Jun 16, 2026
Reworks the small-step semantics of Imperative to dix a scoping bug regarding internal function declaration. Subset of the changes from PR #1325 — the `OverapproximatesWhen`/`OverapproximatesAggressively`/`InitEnvWF` work is deferred to a follow-up PR. * Evaluator scoping (FIX of a scoping bug — function declarations leaked out of their enclosing block): Inner function declarations (`step_funcDecl`) extend the evaluator (`Env.eval`) with the new function, and previously, that extension persisted past the enclosing block — i.e. a `funcDecl` inside a block was visible to code AFTER the block exited. This is wrong: by the language's variable-scoping rules, a `funcDecl`'s scope is its enclosing block, exactly parallel to `init`. The fix: * `Config.block` now carries a snapshot of the parent evaluator (`e_parent`) in addition to the parent store (`σ_parent`): `Config.block label σ_parent e_parent inner` (was 3-arg). * On `step_block_done` / `step_block_exit_match` / `step_block_exit_mismatch` the result config's `eval` is RESTORED to `e_parent`, so a `funcDecl` introduced inside the block is NOT visible after exit. * New HasFvars / HasOps / HasOpsImp typeclasses: * `HasFvars` returns ALL free variables in an expression. * `HasOps` (`P.Expr → List P.Ident`) returns operator/function names referenced in an expression, parallel to `HasFvars` for variables. * `HasOpsImp` lifts that to commands (`Cmd.getOps`, `Cmds.getOps`). * Refactoring of HasBool / HasBoolOps: * `HasBool` now extends `HasVal` and bundles `boolIsVal` (former `HasBoolVal` is folded in). * Boolean operations split out into `HasBoolOps` (extends `HasBool`): not, and, imp. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
shigoel
pushed a commit
that referenced
this pull request
Jun 16, 2026
Reworks the small-step semantics of Imperative to dix a scoping bug regarding internal function declaration. Subset of the changes from PR #1325 — the `OverapproximatesWhen`/`OverapproximatesAggressively`/`InitEnvWF` work is deferred to a follow-up PR. * Evaluator scoping (FIX of a scoping bug — function declarations leaked out of their enclosing block): Inner function declarations (`step_funcDecl`) extend the evaluator (`Env.eval`) with the new function, and previously, that extension persisted past the enclosing block — i.e. a `funcDecl` inside a block was visible to code AFTER the block exited. This is wrong: by the language's variable-scoping rules, a `funcDecl`'s scope is its enclosing block, exactly parallel to `init`. The fix: * `Config.block` now carries a snapshot of the parent evaluator (`e_parent`) in addition to the parent store (`σ_parent`): `Config.block label σ_parent e_parent inner` (was 3-arg). * On `step_block_done` / `step_block_exit_match` / `step_block_exit_mismatch` the result config's `eval` is RESTORED to `e_parent`, so a `funcDecl` introduced inside the block is NOT visible after exit. * New HasFvars / HasOps / HasOpsImp typeclasses: * `HasFvars` returns ALL free variables in an expression. * `HasOps` (`P.Expr → List P.Ident`) returns operator/function names referenced in an expression, parallel to `HasFvars` for variables. * `HasOpsImp` lifts that to commands (`Cmd.getOps`, `Cmds.getOps`). * Refactoring of HasBool / HasBoolOps: * `HasBool` now extends `HasVal` and bundles `boolIsVal` (former `HasBoolVal` is folded in). * Boolean operations split out into `HasBoolOps` (extends `HasBool`): not, and, imp. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
joehendrix
pushed a commit
that referenced
this pull request
Jun 16, 2026
Reworks the small-step semantics of Imperative to dix a scoping bug regarding internal function declaration. Subset of the changes from PR #1325 — the `OverapproximatesWhen`/`OverapproximatesAggressively`/`InitEnvWF` work is deferred to a follow-up PR. * Evaluator scoping (FIX of a scoping bug — function declarations leaked out of their enclosing block): Inner function declarations (`step_funcDecl`) extend the evaluator (`Env.eval`) with the new function, and previously, that extension persisted past the enclosing block — i.e. a `funcDecl` inside a block was visible to code AFTER the block exited. This is wrong: by the language's variable-scoping rules, a `funcDecl`'s scope is its enclosing block, exactly parallel to `init`. The fix: * `Config.block` now carries a snapshot of the parent evaluator (`e_parent`) in addition to the parent store (`σ_parent`): `Config.block label σ_parent e_parent inner` (was 3-arg). * On `step_block_done` / `step_block_exit_match` / `step_block_exit_mismatch` the result config's `eval` is RESTORED to `e_parent`, so a `funcDecl` introduced inside the block is NOT visible after exit. * New HasFvars / HasOps / HasOpsImp typeclasses: * `HasFvars` returns ALL free variables in an expression. * `HasOps` (`P.Expr → List P.Ident`) returns operator/function names referenced in an expression, parallel to `HasFvars` for variables. * `HasOpsImp` lifts that to commands (`Cmd.getOps`, `Cmds.getOps`). * Refactoring of HasBool / HasBoolOps: * `HasBool` now extends `HasVal` and bundles `boolIsVal` (former `HasBoolVal` is folded in). * Boolean operations split out into `HasBoolOps` (extends `HasBool`): not, and, imp. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
…matesUpto(When) and WF of program state
* `OverapproximatesUpto(When)`: an extension of `Overapproximates` in the sense that it takes the mapping relation between program states of the input and output program.
* `OverapproxiamtesUptoWhen` additionally takes the precondition on the input program.
* `OverapproximatesWhen` / `OverapproximatesAggressivelyWhen`:
* Precondition-bearing variants: take a `pre : L₁.StmtT → Prop` that the
initial source statement must satisfy.
* Original `Overapproximates` / `OverapproximatesAggressively` are now
`*When`-wrappers with `pre := fun _ => True`.
* `*.toWhen` and `*When.strengthen` provided in SpecificationProps.
* `OverapproximatesAggressively`: a new variant that allows spurious assertion
failures — the target is allowed to terminate with `hasFailure = true`
instead of matching the source's terminal/exiting env exactly.
* `Overapproximates` is extended to also preserve `CanFail` and the
`initEnvWF` of the target; the `prefixIdents` discipline tracks fresh
identifier prefixes that downstream transforms reserve.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
aqjune-aws
force-pushed
the
jlee/sem-updates
branch
from
a1b8bf8 to
fb2d06c
Compare
aqjune-aws
changed the title
github-actions
Bot
added
dependencies
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.
Updates in specification of transformations to support several missing features needed by loop elimination correctness.
A new
OverapproximatesAggressivelythat allows spurious assertion failures even when executions started from the exactly same initial program state. :)TsatisfiesOverapproximatesAggressively, it also satisfiesOverapproximates.A new
OverapproximatesUpto(When): an extension ofOverapproximatesin the sense that it takes the mapping relation between program states of the input and output program.OverapproxiamtesUptoWhenadditionally takes the precondition on the input program.New
OverapproximatesWhen/OverapproximatesAggressivelyWhen:pre : Stmt → Propthat the input program (which is an imperative statement) must satisfy.Overapproximates/OverapproximatesAggressivelyare now*When-wrappers withpre := fun _ => True.*.toWhenand*When.strengthenprovided in SpecificationProps.InitEnvWF: a structure capturing well-formedness of the initial program state (Env).defUseWellFormed/Block.defUseWellFormed: a static check that every use of a variable references a previously-defined variable, and every use of an operator references a previously-funcDecl'd name.Reflection-based
factoryDeclaredpredicate replacing the prior hard-codedfactoryFuncNameslist (derived fromWFFactoryArray).