Repository navigation
Conversation
…d parser (M0) Adds formal/, a Lake project (Lean 4.35.0 + Mathlib v4.35.0, isolated behind Dace/Prelude.lean) that will hold the formal semantics of SDFGs and schedule trees. This first milestone contains: - Dace/Core/Expr: the symbolic expression language (idealized integers, IEEE floats treated opaquely, opaque function applications, data reads) with evaluation. - Dace/Core/Subset: ranges/subsets mirroring dace.subsets with point enumeration and basic lemmas. - Dace/Core/Parse: parser and printer for DaCe's Python-syntax expression strings. - Dace/Decisions.md: the semantic decision register. - scripts/check_axioms.sh and a formal-ci workflow (build, sorry/axiom checks, Mathlib import isolation). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
- formal/tools/corpus_programs.py and dump_corpus.py: a set of small DaCe programs covering maps, WCR, strided ranges, dynamic map ranges, loops with branches, while loops, nested calls, views, transients and library nodes, dumped as SDFG JSON into formal/tests/corpus (incl. a MapTiling and an expanded-Reduce variant). - Parser: accept serialized '$'-prefixed symbols, SymExpr(exact, approx) wrappers (new Expr.approx node), floor/ceiling, and assignment statements; values gain exact rationals for SymPy division. - tests/ParseCorpus.lean parses every expression string of the corpus (89/89). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…R, logs and parallel merge - Core/Data: DataDesc for arrays, scalars, streams, views, references, structures and container arrays (flat repository), structural equivalence. - Core/Memlet: memlets normalized to src/dst subsets; WcrOp with built-in reductions detected structurally from the parsed lambda, custom lambdas kept as expressions (D26). - Core/Memory: location paths, alias environment for views/references, FIFO queues for streams; read/write lemmas. - Core/Wcr: concrete WCR application and the Lawful (commutative/associative) hypothesis (D24). - Core/Merge: access logs of parallel executions, conflict detection and merge onto the initial memory; permutation lemmas for writes, WCR contributions, alias bindings and queue effects. - Core/Tasklet, Core/Interp: tasklets as uninterpreted functions of their connector values; the Interp bundle of all open parameters. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
- SDFG/Syntax: flat rendering of DaCe's classes (nodes with connectors and scope_entry, memlet/dependency edges, states, LoopRegion, ConditionalBlock, break/continue/return, regions, nested SDFGs with symbol mappings, Reduce library-node properties). - SDFG/Json: importer for dace.serialize output with memlet normalization to src/dst subsets, full-range completion of one-sided copies (D9), flattened structure members (D21), WCR lambdas parsed structurally. - tests/ImportCorpus.lean imports all 15 corpus SDFGs. - WcrOp.ofLambda? accepts DaCe's parenthesized lambdas; check_axioms.sh no longer writes to /dev/stderr. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
- SDFG/Scope: routing vs leaf edges, memlet trees (prev/next closure, leaves, root), scope children/chains, weakly connected components, topological-order check and a deterministic Kahn order. - SDFG/WF: decidable transcription of validation.py's structural rules (connectors, dangling/multi edges, entry-exit pairing, scope crossing, memlet data/dimensions/rooting, empty-memlet placement, acyclicity, interstate assignment rules, conditional else placement, array/symbol disjointness) and the nested-SDFG connector contract; errors vs warnings. - tests/StructureCorpus.lean: all 15 corpus SDFGs are well-formed; every state has a valid topological order and access-rooted memlet trees. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…extensions Statement-level interpreter for Python tasklets (assignments, augmented assignments, subscripts into pointer connectors, stream pop/push, math library and dtype casts) providing Interp.executable; parser gains the Python conditional expression and qualified calls. All 27 corpus tasklets parse. Decision D28. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
scripts/difftest.py records inputs and DaCe-computed expected outputs for every corpus SDFG (loaded from JSON, compiled and run) and checks `lake exe dace-interp` against them with dtype-aware tolerances. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Mutual inductive execution relations over the flat state graph and the control-flow hierarchy: leaf copies, tasklets and library nodes, Reduce, views and references, maps with per-iteration logs merged commutatively, consume scopes, nested SDFG invocations through aliased connectors, loop regions, conditional blocks and nondeterministic interstate choice. Consume conditions are parsed at import. Decisions D29-D44. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…on the corpus SDFG/Interp.lean mirrors every execution relation one function per relation (deterministic refinements: Kahn order, first true edge, PE 0); Tools/Interp.lean runs the executable interpretation on recorded inputs and prints round-trippable JSON. Tasklets now see the symbol valuation (D46); region start blocks resolved at import (D45). All 15 corpus programs match DaCe. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…tputs (D47) Log.seq keeps a read of a location the same execution already updated with WCR, so merge reports a race when another execution also contributes to it. Code nodes with a dynamic WCR out-memlet (atomic capture returning the old value) are flagged as not modeled rather than silently misread. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ation-proof-594500
Soundness.lean proves SDFG.run_sound: every outcome of the fuel-based interpreter is derivable in the relational semantics, by one lemma per mirrored function and induction on fuel. The interpreter re-checks the computed topological order against the relation's premise (D43 note). Axioms: propext, Classical.choice, Quot.sound only. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
dace/sdfg/analysis/schedule_tree/serialize.py: to_json/from_json for all concrete schedule tree node types, reusing dace.serialize encodings for embedded memlets, descriptors and nodes, with round-trip tests over the coverage factories and the formal corpus. dump_corpus.py also writes <name>.stree.json/.stree.txt and strips machine-specific paths from the corpus (regenerated); difftest.py gains --ir stree. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ntics (M4 part 1) Dace/STree: one constructor per concrete schedule tree node type, importer for the serialize.py format, WF (elif/else chains, dynamic scope inputs immediately preceding their scope, labels and gotos), and a relational big-step semantics with sequential siblings, parallel map scopes, consume scopes, label-indexed goto resumption and sequential symbol assignments. Pretty-printer reproduces as_string on all 15 corpus trees. SDFG leaf functions factored into container-level cores shared by both semantics. Decisions D48-D58. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ss (M4 complete) STree/Interp.lean mirrors the tree execution relations; STree/Soundness.lean proves STree.run_sound (axioms: propext, Classical.choice, Quot.sound). dace-interp gains the stree IR kind sharing the sdfg driver. Differential test: 15/15 corpus trees and 15/15 corpus SDFGs match DaCe. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The exact-image fix for strided map propagation (58b5bfd) tightened the point-access special case's end bound to the last *visited* index (node_rlast) instead of the literal map end (node_re). This desynced it from Range.size()/num_elements(), which MapFission's border-array transients are sized with, since SymPy cannot always prove the two ceiling-based forms equal without extra sign assumptions on the step. Revert the point-access case to the literal node_re (matching its original, pre-existing behavior); only the general path (used by the contiguous-tile case) keeps the tightened end. Verified: tests/transformations/map_fission_test.py 29/29 passed (was 1 failed); full regression sweep (tests/sdfg, tests/schedule_tree, map_tiling_test) otherwise unchanged. Co-Authored-By: Claude <noreply@anthropic.com>
…tree fixes - validation.py: the src/dst element-count check now also accepts counts that are equal once the enclosing maps' step symbols are assumed positive (a well-formed map has a positive step), so exact strided images such as ceiling((s*ceiling(x/s)-s+1)/s) == ceiling(x/s) are no longer rejected against Range.size()-derived transients. - propagation.py: trim the point-access special case (no dead branch). - treenodes.py: a scope does not report the views it defines as outputs; a view binding moves no data (fixes a spurious state boundary around consume scopes). - copy_direction_test.py: unique program names per test so compiled builds are not shared between tests that build same-named SDFGs. - propagation_test.py: the non-matching clipped tile keeps its Min in inclusive form. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ile probes from stree tests A code node that reads an access node its own parallel-scope iteration contributed to through WCR may observe a partially reduced value. Emit a warning (private scope-lifetime transients and provably disjoint subsets excluded). The schedule-tree tests no longer probe for a compiler. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…tting it The workflow installs DaCe, dumps the corpus programs, records inputs and expected outputs with a fixed seed (difftest.py --seed, default 0 keeps the previous inputs), then runs the Lean corpus tests and both difftests. The Lean corpus tests now fail on errors (corpus path overridable with DACE_FORMAL_CORPUS). Shell and Lean files are checked out with LF. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…a hazard The IN_stream binding of a consume scope is the entry's own pop of the stream; pushes from the body back to it (work lists) are ordered by the queue. Order the binding before the scope so tree_to_sdfg no longer inserts a state boundary (and a nested SDFG inside maps). Accesses to the stream by other nodes are still checked. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…estination-side self copies - AssignNode no longer stores a redundant InterstateEdge; its read memlets are computed from the assigned value (old JSON with an edge still loads). - LibraryCall.own_properties() is the single source of the printed properties and is stored in the tree JSON. - A copy within one container whose memlet is written on the destination side ([0:5] -> A[5:10]) was converted with swapped ranges; normalize it to the source side (regression test in copy_direction_test.py). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…56, D57) The tree importer reads library-node properties as printed by DaCe (own_properties) for every library node; arrows of other_subset follow the memlet's source/destination. Empty memlets on tree code nodes are dropped and empty copies removed. New corpus program matmul_lib (SKIP in difftest: library node not modeled) and STreeJsonTest.lean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- New error class ErrReason.unsupported (valid DaCe, not modeled; not UB): fetch-and-add, reference set from a code node, dtype-reinterpreting views. Undefined library interpretations are UB (libraryUndefined), like taskletUndefined; dace-interp prints the error kind. - Copies execute only at the leaf memlet of their memlet tree: routing edges through scope exits no longer copy again, which overwrote stage-out copies of scope-private transients with pre-map values. - A transient is private to a scope only with Scope lifetime and when every mention (access nodes, code, ranges, interstate and control-flow expressions) lies inside it; both IRs use the same rule. - The consume chunk is a real transient Register container declared by both importers. - New corpus programs private_stage_out (regression) and consume_sum. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…a (R1.1) R0.4: scopeNodes, components, scopeChain, treeRoot and treeEdges are total (fuel-bounded closure) with membership/partition/topological-order specification lemmas in SDFG/ScopeSpec.lean; WF reports cyclic scope nesting. Behavior unchanged on WF inputs. R1.1: Core/MergeLemmas.lean proves seq associativity, conflict monotonicity, merge = application of the union, merge_perm (lawful WCR, conflict-free, queue-disjoint), merge_le for a key-order-preserving Log.Le, dropNames distributivity, and one-entry apply lemmas. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…s (R2.1-R2.3) - Core/Facts: sign predicates and relations of DaCe's symbol registry (symbol_repo.params), imported into SDFG.facts (D60). - Core/SymArith: integer polynomial normal form of expressions with opaque atoms (floor division, modulo, Min/Max/Abs) and their defining inequalities; toPoly?_sound, atomEnv_axioms. - Core/SymCert: Positivstellensatz-style certificates (linear and pairwise-product terms, case splits) with Cert.check_sound; facts to hypotheses (toHyps_sound). - Core/SymSearch: untrusted Fourier-Motzkin certificate search and Lean obligation emission (Query.toLeanFile). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Dace/Equiv: Prog with its precondition (lawful interpretation, facts, no initial aliases), observable containers (non-transient arrays, streams and structures plus __return*; scalars are inputs, D63), UB-style Refines/Equiv where malformed and unsupported give no claim (D64), with refl_iff_supported, trans, symm, conservative, and the fragment relations Sim, St.Rel, CSt.Rel. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
SeqExec records each node's own log delta; OrderedExec reports a race when two nodes that no path orders have conflicting deltas (D61, an unordered conflict is undefined behavior per synchronization.rst). The schedule tree stays sequential. WF rejects self-loops (D62, also covers cyclic scope nesting); total reachability with irreflexivity under WF. New corpus program unordered_writes (expected race on the SDFG side; difftest supports expected errors). No race on 154 npbench programs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…D66) - Element accesses outside the accessed container's shape are the UB error outOfBounds, except through allow_oob memlets; checked in the shared container cores, so both IRs agree. - Views and pointer inputs bind at the subset's lower bounds, so empty views are valid; Reduce over an empty input writes the identity. - The expression parser accepts DaCe's typed-symbol form symbol($N, dtype=...). - New corpus programs empty_view, oob_read (expected error), oob_allowed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Every execution relation of the SDFG and schedule-tree families is invariant under prefixing the incoming log (shift_iff), map iterations and consume tasks do not depend on the pre-scope log at all, and runs from related start states (St.Rel/CSt.Rel) have related outcomes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Core/SymSubset: point-membership lemmas for dimensions, ranges and subsets; sound nonneg?/pos?, disjoint?, subsetOf?, and iterDisjoint? (two distinct map iterations never touch a common linear offset, via index separation or offset ordering decided by certificates), plus iterObligations? returning undecided queries for kernel checking. Decides tiled (MapTiling and tile-index forms), strided and symbolic 2D accesses; actual races stay UNKNOWN. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Equiv/Congr: the semantics depends on the SDFG only through the arrays and the private-transient sets (ctx_congr); paths into the region tree with setBlockAt; Congr.block/blockEquiv: replacing a block by one whose runs are simulated (UB, equal error, or related ok outcome) from the same start state preserves Refines/Equiv, given equal transient mention counts and a supported original. Demos: empty states are equivalent; a state equals the state followed by an empty state. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
R1.6: footprinted-action discipline (SDFG/Footprinted), frame lemmas and coherence (a run depends on memory only at its reads and ends in its log applied, SDFG/Frame, fragment SeqPure), adjacent swaps of non-conflicting nodes, and order independence: an ok outcome yields ok, race-free runs along every topological order with an equivalent result; component merge equals sequential execution in any order (Equiv/Order). Full uniqueness (det) over nested iteration orders remains. R2.6: static footprints of nodes, scopes and components (SDFG/Footprint) and soundness: every location logged by a map iteration, a node's delta or a component is a point of a leaf memlet's subset under extended map bindings (IterExec.footprint, SeqExec.fp_trace, CompsExec.fp_logs). Pointer-output writes are covered only as any element (to be tightened). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A write through a pointer output connector must address a point of the memlet's subset; otherwise the execution is the new undefined behavior outsideSubset. Static footprints of code-node outputs are now exactly their subsets (the whole-container anyElem access is gone). Corpus regression write_outside. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
raceFree? g = true implies RaceFree g: no execution satisfying the program precondition ends in a race. Races only originate in merges of parallel logs and in the happens-before check (Dace/SDFG/Clean.lean proves every other semantic function race-free); the check bounds logs by static footprints and separates them by container, access kind, or iterDisjoint? for distinct map iterations (private transients excepted). dace-equiv racefree prints RACE-FREE/UNKNOWN per SDFG; tests/RaceFreeCorpus.lean pins the corpus verdicts. New corpus program map_same_write (a race in both IRs). Without a symbol repository the declared integer symbol types are the facts (D60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
raceFreeWith orc accepts undecided disjointness queries the oracle accepts; raceFreeWith_sound assumes them valid, raceFree? is the oracle accepting nothing. dace-equiv racefree --emit-obligations DIR writes the remaining queries (raceObligations) as closed Lean theorems over Z. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Replacing the body of a map scope by one whose iterations are simulated by the old body's refines the SDFG (Congr.scopeBody, Congr.scopeBodyEquiv, Congr.mapBody with State.withBody). The side condition is the decidable check sameOutside? (soundness: sameOutside?_spec): outer nodes see the same adjacent edges and memlet-tree endpoints, the body is entered only from the map entry and left only through the shared exit, outer reachability is kept, components and enclosing map scopes correspond. Topological orders of the new state transport to the old one (State.isTopologicalOrder_splice). tests/ScopeBodyCheck.lean runs the check on every corpus map. D60 records the owner's confirmation of type-derived symbol facts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
On the fragment seqPure? with convex map scopes (scopesOk?, a decidable check by reachability in the subgraph induced by the scope), one normal derivation of a node, sequence, scope body, map iteration list, component list or state makes every derivation from an equivalent state normal with an equivalent result (equal memory and values, logs equal up to commuting reorderings): NodeExec/SeqExec/OrderedExec/IterExec/CompsExec/StateExec.det and StateExec.no_err. The proof inducts over the other derivation and uses the frame lemmas, order independence and invariance of the happens-before check under equivalent deltas. tests/DetCheck.lean runs the hypotheses over the corpus (35 states, 27 in the fragment, all convex) and rejects a scope made non-convex. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Keys of SDFG code nodes, copies and map set-up (connector, container endpoint, subset, WCR, allow_oob) computed from the structural endpoints of the leaf edges, and of tree nodes from their normalized memlets; when they agree, the SDFG and tree leaf functions coincide on every state (execCode_eq, execReduce_eq, execCopiesInto_eq/execCopyT_eq, mapSetup_eq/mapSetupT_eq), in contexts with the same erased part. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…otprint) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
SegCorr ctx tc s o cs: the tree list cs is the image of the SDFG nodes o (copy nodes per copy edge into an access/exit node, tasklet and library nodes with equal keys, map scopes with the image of a topological order of the scope's direct children and equal private transients). SegCorr.sim: every tree run of the segment is matched by the sequential SDFG run of o from a state with the same memory and log: undefined behavior, the same error, or the same memory and log (iterations with a happens-before race are UB). Fragment SeqPure. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
States (StateCorr.sim: SeqPure, at most one component, coherence of the component run with the merged log), the chain of states joined by unconditional edges (ChainCorr.sim) and programs (ProgCorr.exec: every outcome of the tree is an outcome of the SDFG or the SDFG may be undefined; ProgCorr.refines: Refines t g for a supported SDFG). The checker corrCheck places the SDFG nodes greedily along the tree list and checks the order is topological; corrCheck_sound, corr?_exec, corr?_refines. Library nodes match by classpath and reduce properties (labels differ). dace-equiv stree <sdfg.json> <stree.json>; tests/EquivCorpus.lean: 14 corpus pairs certified, the rest UNKNOWN with reasons (outside SeqPure, control flow, differing descriptors). dump_corpus.py builds the tree from the SDFG as stored (in-memory edge order can differ from the file's, and the checker matches input memlets in edge order). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sim/SimE/BlockSimE/RegionSimE/LoopSimE/BodySimE/BranchSimE become Matched/MatchedE/..., the *.sim/*.simB/*.simE/*.simBody theorems *.matched/..., Equiv/CorrSim.lean becomes Equiv/CorrMatch.lean. Nothing in Equiv executes a program; the module documentation of Equiv/Frag now states the theory: matching is a (forward) simulation over big-step outcomes, matching in both directions relates outcome sets, which is weaker than bisimulation except on deterministic programs, and lists the choices the SDFG semantics leaves open. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…s move) Sim/SimE/BlockSimE/RegionSimE/LoopSimE/BodySimE/BranchSimE become Matched/MatchedE/..., the *.sim/*.simB/*.simE/*.simBody theorems *.matched/... (the previous commit only moved Equiv/CorrSim.lean to Equiv/CorrMatch.lean). Nothing in Equiv executes a program; the module documentation of Equiv/Frag states the theory: matching is a (forward) simulation over big-step outcomes, matching in both directions relates outcome sets, which is weaker than bisimulation except on deterministic programs, and lists the choices the SDFG semantics leaves open. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
doc/sdfg/ir.rst leaves the behavior undefined when more than one outgoing interstate edge is true; the model chose among them nondeterministically. Now a new RegionAt rule ends such a block in ambiguousTransition (UB), and a transition is taken only when exactly one edge is true (trueEdges = [ie]). DaCe's first-true-edge code and the schedule tree's stateif order refine it, and the SDFG control flow is deterministic: the remaining choices of the semantics are the node order in a state (irrelevant without races) and the processing element of a consume task. Interpreter, its soundness, the log-shift, congruence and race-check proofs follow. Corpus regression ambiguous_edges (SDFG: ambiguousTransition; tree compared by value). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Control flow is deterministic since several true interstate edges are undefined behavior (D2). Lift state determinism to blocks, regions, loops, conditional blocks and SDFG invocations: for a lawful WCR semantics, a program whose states all pass seqPure? and scopesOk? (SDFG.det?) has no other outcome once it has a normal one, in particular no race. 18 of 25 corpus programs pass the check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The SDFG / schedule-tree pair checker now covers regions whose blocks are joined by single unconditional edges, loop regions, conditional blocks (if/elif/else chains), break, continue and return (Equiv/CorrCtl.lean: RegCorr/BlockCorr/ElifCorr, their matching theorems and the checker regCheck/blockCheck/elifCheck with soundness proofs). Interstate assignments become the following AssignNodes. The tree runs them one by one, the SDFG simultaneously; they agree when, in the tree's order, no assigned symbol is read by a later right-hand side or by a descriptor (assigns_seq). The tree's order may be any permutation of the edge's, since the importer reads the assignment object in key order (applyAssigns_perm). Fixes: - both importers defaulted a missing update_before_condition to false; DaCe's default is True and serialization omits defaults, so inverted loops took the condition-first path - break/continue escaping the program now has the same malformed message in both semantics - ImportStreeCorpus strips trailing whitespace on both sides New corpus programs loop_control, early_return, do_while and do_while_cond_first pass the difftests on both IRs; 21 pairs certified. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Named regions correspond to a NamedRegionScope, plain and function-call regions are inlined into the enclosing list (as sdfg_to_tree does). The region theorem is now stated for a prefix of a tree list (RegCorr.matched with the rest of the list, BOut), and regCheck returns the rest. New corpus program regions; 22 pairs certified. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Split the sequential fragment: SeqPureP is SeqPure without the condition that map scopes have no private transients (SeqPure extends it with noPriv). Only the frame property needs that condition; coherence (the local view is the initial memory with the log applied) holds on SeqPureP and is proven directly (NodeExec/SeqExec/OrderedExec.steps, OrderedExec.coh). The pair checker now uses SeqPureP; both sides drop the same private sets (already checked per map). augassign_wcr and private_stage_out are certified; 24 pairs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The SDFG binds the dynamic inputs of a map one by one, reading each under the valuation extended by the previous ones; the tree reads them into pending symbols with DynScopeCopyNodes and binds them at the map scope. With distinct connectors that no descriptor and no input subset mentions (DynOk), both are dynReadAcc followed by setAll (bindDynamicInputs_eq, dscopies_run). SegCorr.map now takes the DynScopeCopyNodes in front of the map scope. The evaluation-congruence lemmas move to Equiv/EvalCongr (with subset and scalar-read congruence). spmv is certified; 25 pairs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… region exits An interstate edge's assignments apply only if the edge is taken, and its condition is evaluated in the old valuation: the assignments now sit inside the conditional (StateIfScope body, or an IfScope wrapping the rest of a structured chain). A block without a taken edge ends its enclosing region instead of the program: structured chains no longer emit a negated exit goto, and blocks of a general block without an unconditional out-edge jump to a minted end label instead of falling through to the next label. Adds regression tests and the corpus programs sink_states and loop_conditional_edge; updates tests that pinned the old tree shapes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
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.
No description provided.