Add SMACK pre/post-processing pipeline for reproducible .core.st inputs - #2
Open
PROgram52bc wants to merge 19 commits into
Open
Add SMACK pre/post-processing pipeline for reproducible .core.st inputs#2PROgram52bc wants to merge 19 commits into
PROgram52bc wants to merge 19 commits into
Conversation
added 4 commits
August 5, 2026 13:36
BoogieToStrata already documents its `--smack` mode, but the steps that
bracket it — turning a C source into a translator-ready `.bpl` and cleaning
up the emitted Core — lived outside this repository, so SMACK-generated
benchmark inputs could not be reproduced from their sources here.
This adds a self-contained `smack-pipeline/` directory:
- Dockerfile SMACK container image (linux/amd64).
- smack_to_core.py driver: .c -> SMACK -> .bpl -> strip ->
BoogieToStrata --smack -> .core.st -> fix.
- strip_smack_prelude.py removes SMACK prelude procedure bodies
(unstructured multi-target gotos the translator
cannot ingest) and inlines __VERIFIER_assume.
- fix_core_st.py sorts function definitions and renames
parameters that shadow type names.
- README.md pipeline overview, prerequisites, per-stage usage.
C sources are not included; the driver points at any .c directory. Generated
artifacts are git-ignored. Verification is out of scope — that lives in the
main Strata package.
Three small, self-contained examples under smack-pipeline/examples/, each
demonstrating one pipeline stage on a hand-written (SMACK-shaped) .bpl, with the
intermediate and final artifacts committed so the transformation is visible:
- assume_inline — strip_smack_prelude inlines call __VERIFIER_assume(x)
to assume (x != $0).
- prelude_strip — strip_smack_prelude drops a multi-target-goto prelude body
(__SMACK_and32) to a bodyless declaration; user code kept.
- func_reorder — fix_core_st topologically sorts function definitions so a
callee precedes its caller (.raw.core.st vs .core.st).
check_examples.py regenerates each through strip -> BoogieToStrata --smack -> fix
and diffs against the committed outputs, so the examples double as a regression
test for the utilities. Requires only the .NET 8 SDK (no SMACK/container — the
inputs are hand-written .bpl).
The Dockerfile cloned SMACK unpinned, so the generated .bpl drifted with SMACK's frontend — defeating the point of a reproducible input pipeline. Newer SMACK releases emit control flow the translator does not yet reduce (a two-target goto whose arms are not obvious inverses), so a fresh clone can fail translation even when an older clone succeeded. Pin via SMACK_REF (default v2.10.0) and document the version-compatibility caveat in the README: if a freshly generated .bpl fails on such a goto, set SMACK_REF to the release that produced the reference corpus and rebuild.
…n-good triple The CI cloned Strata-CLI from `main` and let Lake resolve its dependencies to `main` on Strata / Strata-Python / Strata-DDM. Strata-CLI's own push CI has been failing since ~mid-July: its StrataMainLib.lean does not compile against current Strata's API (drifted identifiers, argument names, and field-projection targets). Our build inherited that upstream breakage, failing at `[512/519] Building StrataMainLib` on every run. Fix: check out Strata-CLI at its last commit whose push build was green (c8e488a2cc, 2026-06-25), then rewrite its lakefile revs to the sibling Strata / Strata-Python / Strata-DDM commits from that same window. An awk state machine keys the rewrite on the [[require]] block's exact name so "Strata" does not also match "StrataPython" / "StrataDDM". Verified locally on macOS Lean 4.29.1: a fresh clone at c8e488a2cc with the lakefile revs rewritten to this triple builds `strata` end-to-end (519/519 jobs, 161MB binary produced, zero errors). This unpins when upstream Strata-CLI's own push builds go green again.
PROgram52bc
marked this pull request as ready for review
August 5, 2026 22:48
atomb
requested changes
Aug 6, 2026
| # Strata/Strata-DDM/Strata-Python happen to be at HEAD today — the | ||
| # upstream API has drifted and StrataMainLib no longer compiles | ||
| # against `main`. Pin the CLI commit and rewrite its lakefile revs to | ||
| # the sibling commits that formed the last CI-verified-green build. |
Contributor
There was a problem hiding this comment.
Let's leave this PR open until those build issues are fixed (which should be soon). Then we can remove this complex workaround.
Contributor
There was a problem hiding this comment.
I think those issues are resolved now, and this PR should work without changes to this file.
Move the two fixes fix_core_st.py did as .core.st post-processing into the translator, so the emitted Core needs no cleanup (addresses review feedback: "better to fix BoogieToStrata to avoid these issues in the first place"). - Topological sort of the function section (StrataGenerator): a function whose inline body calls another is emitted after its callee, removing forward references. FunctionCallCollector gathers a body's callees; ToposortFunctions runs Kahn's algorithm, preserving declaration order on ties and cycles. - Type-name / parameter shadowing: a local binding (function/procedure formal or quantifier bound variable) whose name equals a program type name is emitted with a `p_` prefix. The rename is applied in NameOf at every binding and reference site, so — unlike the function-section-only Python pass — it also reaches the definition axiom Boogie lifts an inline body into, whose forall binder and references are distinct bound variables sharing the parameter name. Tests: FunctionForwardReference.bpl pins callee-before-caller ordering; ParamTypeNameShadow.bpl pins the rename reaching both the signature and the axiom. All 47 non-verifier integration tests pass.
With BoogieToStrata sorting functions in dependency order and renaming type-shadowing parameters itself, the .core.st post-processing pass is redundant. Delete fix_core_st.py and drop the fix stage from the pipeline: - smack_to_core.py / check_examples.py: pipeline is now strip -> translate; the driver writes <stem>.core.st directly (no _fixed suffix). - Alphabetical tie-break added to the function toposort so independent functions keep the deterministic layout the pipeline expected. Regenerated the committed example .core.st; dropped func_reorder.raw.core.st (there is no longer a raw-vs-fixed distinction). New test FunctionAlphabeticalOrder.bpl pins the tie-break (dependency order still wins over alphabetical). - README / examples/README: updated diagrams, contents, and the func_reorder writeup to describe the translator-native ordering. All 49 non-verifier integration tests pass; check_examples.py matches 3/3.
A `free ensures` on a procedure that also has an implementation is a
Boogie summary meant to abstract the body when the callee is not inlined.
SMACK's equivalence harness emits such a summary pinning the reffile
output to the otherfile uninterpreted function
(`free ensures $return == _uf_otherfile...($args)`) alongside an
`{:inline 1}` implementation. Boogie honors the inline attribute and
compares the real (differing) bodies, refuting inequivalent programs.
The translator drops the inline attribute (VisitQKeyValue is a no-op), so
under `--call-policy bodyOrContract` Strata assumes the free-ensures
summary instead of evaluating the body. In an equivalence miter both
sides then collapse to the same otherfile UF over the same arguments, so
the equivalence check passes vacuously, falsely certifying inequivalent
(.Neq) programs as equal.
Restore Boogie's semantics by suppressing free-ensures summaries for
body-bearing procedures: Strata verifies against the emitted body.
Checked (non-free) ensures, including the miter equivalence obligation,
are kept; genuine bodyless uninterpreted stubs keep their summaries.
Verified against 21 previously-false-certified EQ files: none clean-pass
after the fix (real body evaluation yields FAIL matching Boogie, or an
honest unknown/timeout) instead of the prior vacuous pass.
The Core DDM grammar spells bitvector types as `bv W{n}` (a `bv` type
applied to a width type) rather than the atomic `bv{n}`, and has no infix
arithmetic: every bitvector operation is a width-specialized prefix call
(`bv{w}.add`, `bv{w}.sLt`, ...) and real arithmetic/comparison are prefix
calls (`real.add`, `real.ge`, ...). The generator previously emitted the
atomic type spelling and synthesized infix operator bodies for SMT-builtin
functions, which the grammar rejects.
- Bitvector type positions now emit `bv W{bits}` (the `bv{n}(v)` literal and
`bvconcat{..}`/`bvextract{..}` builtin spellings are unchanged).
- SMT bitvector builtins map to width-specialized prefix ops taken from the
operand width (e.g. bvadd -> `bv{w}.add`, bvslt -> `bv{w}.sLt`,
bvudiv -> `bv{w}.uDiv`).
- Real arithmetic/comparison in function bodies emit prefix `real.*`
(add/sub/mul/div, lt/le/gt/ge); real equality stays infix `==`/`!=`
(the grammar's polymorphic equality).
Verified: re-translated corpus cores parse, translate, and verify on the
Core evaluator; the previously-failing `Undeclared type or category bv8`
and infix-operator parse errors are gone.
atomb
requested changes
Aug 10, 2026
atomb
left a comment
atomb
left a comment
Contributor
There was a problem hiding this comment.
I think this mostly looks great. The requested changes are minor. In addition to those, though, one of the integration tests is failing.
| // post-processing pipeline expected. `zebra` is declared before `alpha`; with | ||
| // no dependency to constrain them, the emitted Core must list `alpha` first. | ||
| function zebra(x: int): int { x + 1 } | ||
| function alpha(x: int): int { x + 2 } |
Contributor
There was a problem hiding this comment.
🤖 says:
This test doesn't actually distinguish dependency order from alphabetical. caller → callee, and callee < caller alphabetically, so a sort that ignored dependency edges entirely would also emit callee first and pass. The docstring on IndependentFunctionsEmittedAlphabetically points here for "dependency order still wins over alphabetical," but nothing currently proves that.
The implementation is correct (I traced ToposortFunctions — Kahn's only promotes a node once its deps are emitted, then breaks ties alphabetically), so this is purely a coverage gap. Please add a discriminating case where the two orders disagree, e.g.:
function {:inline} alpha(x: int): int { zebra(x) + 1 }
function {:inline} zebra(x: int): int { x * 2 }Correct output is zebra before alpha; an edge-ignoring alphabetical sort would wrongly put alpha first. That's the assertion that actually locks in the behavior.
| # Pin SMACK so the generated Boogie is reproducible. A floating clone drifts with | ||
| # SMACK's frontend: newer releases emit control flow (e.g. two-target gotos that | ||
| # are not obvious inverses) that the translator does not yet reduce. | ||
| ENV SMACK_REF=v2.10.0 |
Contributor
There was a problem hiding this comment.
🤖 says:
SMACK_REF is an ENV, but the README still tells users to override it with --build-arg. docker/finch build --build-arg only overrides an ARG, so the documented override is silently ignored. Either:
ARG SMACK_REF=v2.10.0
ENV SMACK_REF=${SMACK_REF}or reword the README to "edit the file, or pass -e SMACK_REF=... at run time" (and finish the SMACK_REF=<tag-or-commit> example).
The generator emits the current Core bitvector syntax — parametric `bv W{n}`
types and width-specialized prefix ops (`bv64.add`, `bv64.uShr`, ...). The CI
Strata pin predated that grammar: it only accepted atomic `bv{n}` types and
polymorphic infix operators (`+`, `>>`, `==`), so every translated bitvector
core failed to parse (surfacing on `bv9`, the one test exercising concat and
shift).
Bump the pinned Strata / Strata-DDM / Strata-Python triple (and the Strata-CLI
commit) to the sibling revisions from the last CI-verified-green Strata-CLI
build that carries the named-operator grammar. The lakefile-rewrite mechanism is
unchanged.
…le ARG - Add DependencyOrderBeatsAlphabetical: `alpha` (inline) calls `zebra`, so the emitter must place `zebra` first even though `alpha` sorts first alphabetically. Discriminates dependency-ordered emission from a plain alphabetical sort, which the existing independent-pair and callee<caller tests did not (both orderings coincided there). - func_reorder.bpl: rewrite the stale header comment — it referenced the deleted fix_core_st.py and claimed source-order emission; the translator now emits in dependency order. - Dockerfile: make SMACK_REF an ARG feeding the ENV so `--build-arg SMACK_REF=` works as the README documents; tighten the README override example.
… deadlock The .NET Process pattern of WaitForExit() before ReadToEnd() can deadlock (or produce empty output via SIGPIPE) when the child writes enough to stderr to fill the OS pipe buffer. The newer Strata verifier emits whnf-heartbeat PANIC messages to stderr during prove, which likely overflow the ~64KB Linux pipe buffer, causing the child to be killed before writing stdout. Read both streams first, then wait. Also surfaces verifier stderr and exit code in the xUnit test output so failures carry the actual diagnostic.
The Core grammar spells integer comparison as prefix named operators
(`int.lt`/`int.le`/`int.gt`/`int.ge`, applied `int.lt(a, b)`), not infix
`</<=/>/>=`. The generator still emitted infix, so every translated Core with an
integer comparison failed to parse ("unexpected token '<'; expected ')'"),
which surfaced once the pinned Strata moved to the named-operator grammar.
Mirror the existing real-prefix handling: when a BinaryOperator's operands are
`int`, emit the `int.*` prefix call. Real comparison keeps `real.*`; bitvector
comparison is unaffected (it arrives as an SMACK builtin, handled separately).
…/mod
Extends the prior integer-comparison fix: the Core grammar spells integer
arithmetic as prefix named operators too (int.add/sub/mul/div/mod), not infix
+/-/*/div/mod. The generator still emitted infix, so translated Core with integer
arithmetic failed to parse ("unexpected token '*'; expected ')'", etc.).
Fold the arithmetic opcodes into the same operand-type-driven int-prefix switch
used for comparison. A full-corpus scan confirms no infix int/real operator
remains in any generated .core.st.
Completes the infix→prefix migration for the named-operator grammar. Unary negation was still emitted as `-(x)`, which the Core grammar rejects (its unary neg is prefix `int.neg(a)` / `real.neg(a)`). Boolean `!` is unchanged (the grammar keeps prefix `!`). Detected by operand type, matching the binary path. Full-corpus scan: no infix int/real operator and no bare `-(` remain in any generated .core.st.
- SmackAssertProducesSingleMergedSpecBlock now asserts the prefixed `int.gt(p_0, int.neg(1))` form (was infix `p_0 > -(1)`), matching the named-operator grammar. - Log the verifier's full stdout in the test output (delimited) so golden regeneration and future verdict-drift diagnosis don't require local access to the Lean verifier binary.
The named-operator Strata renames loop-invariant proof-obligation labels (`entry_invariant_0_0` -> `insertLoopInvAssert_entry_invariant_loop_0_0`, and likewise for the maintain-invariant goals). Verdicts, positions, counts, and the summary are unchanged (all goals still pass); only the goal labels differ. Regenerated from the pinned verifier's actual output.
A global that a procedure reads under old(...) in a retained free-ensures needs
a pre-state, which the emitted Core exposes only on an inout parameter; and a
caller must pass a global inout whenever any transitive callee takes it inout,
else the emitted call passes a read-only parameter as inout (the verifier then
reports "modifies variables it is not allowed to") or references a pre-state
that does not exist ("cannot find fvar").
InoutGlobalNames now unions a procedure's own modifies + old-referenced globals
with the closure over its transitive callees (CalledProcedureCollector builds
the direct-call graph; a visited set guards mutual recursion). Both the
procedure header and every call site share this predicate, so parameter and
argument modes agree at every level.
Verified against the re-translated equivalence corpus: the prior
type-checking-error verdicts on affected cores are gone; they now type-check and
proceed to real verification.
…ctions
EmitHeapFunctionsForType emitted `f: StrataField <type>` unparenthesized. When
the field type is itself an application — e.g. a bitvector `bv W32` — the
grammar parses `StrataField bv W32` as StrataField applied to two arguments and
rejects it ("bv expects 1 arguments" / "Unexpected argument to StrataField").
Wrap the field type: `StrataField (bv W32)`. Type synonyms (single tokens) were
unaffected, which is why only bitvector-typed heap fields (StrataHeapSelect_bv32
et al.) failed to parse.
atomb
approved these changes
Aug 14, 2026
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
2 participants
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.
What
Adds a self-contained
smack-pipeline/directory with the pre/post-processing utilities that bracket BoogieToStrata's--smackmode, so SMACK-generated benchmark inputs are reproducible from their C sources.The translator already handles
--smack, but the surrounding steps —.c → SMACK → .bpl, prelude stripping before translation, and Core cleanup after — lived outside this repo. Without them, the.core.stinputs used for SMACK benchmarking can't be regenerated here.Pipeline
Contents
Dockerfilelinux/amd64).smack_to_core.py.c→_fixed.core.st);--skip-smackto translate pre-existing.bpl.strip_smack_prelude.py__VERIFIER_assume.fix_core_st.pyREADME.mdprograms/.gitignoreScope / notes
.cdirectory._fixed.core.st; runningstrata verifylives in the main Strata package.Testing
dotnet build Source/BoogieToStrata.csproj— green.--skip-smack) on a SMACK-style.bpl:strip → BoogieToStrata --smack → fixproduces valid Strata Core, including the--smacksyntheticrequires (p != 0)injection onassert_.<type>stubs.Dockerfilebuild +smack --no-verify -bpl) is unchanged from the working pipeline but not re-exercised in this environment.Opened as a draft for maintainer review of placement/naming before finalizing.