Better isolation of non-determinism in Core by MikaelMayer · Pull Request #617 · strata-org/Strata

MikaelMayer · 2026-03-19T19:13:00Z

Summary

Completes the isolation of non-determinism in the Strata Core dialect by extending ExprOrNondet from commands (init/set) to statement-level constructs (ite/loop).

Problem

The previous commits on this branch replaced Option/havoc with ExprOrNondet in Cmd, but Stmt.ite and Stmt.loop still used P.Expr for their conditions/guards. This meant non-deterministic branching and looping could only be expressed indirectly.

Solution

Changed Stmt.ite and Stmt.loop to use ExprOrNondet P for their condition/guard fields. When the condition is .nondet, the branch or loop iteration is chosen arbitrarily.

Key changes:

Stmt.ite condition and Stmt.loop guard now accept ExprOrNondet P
Big-step semantics: added ite_nondet_true_sem/ite_nondet_false_sem constructors
Small-step semantics: added nondet variants for ite and loop steps
DetToNondet transform handles nondet conditions (no assume needed)
LoopElim transform handles nondet guards (no guard negation needed)
All frontends wrap deterministic conditions with .det
All backends handle ExprOrNondet in condition positions
Correctness proofs updated for new semantic cases

Testing

All existing tests pass (except a pre-existing failure in StrataTest/DDM/Integration/Java/TestGen.lean due to a sorry in StatementWF.lean on main).

Fixes #612

Strata/Backends/CBMC/CoreToCBMC.lean

StrataTest/Transform/ProcedureInlining.lean

StrataTest/Languages/Core/Tests/StatementTypeTests.lean

Strata/Transform/StructuredToUnstructured.lean

.github/CODEOWNERS

Examples/NondetCond.core.st

Replace Option/havoc with ExprOrNondet in Cmd, and extend ExprOrNondet to Stmt.ite and Stmt.loop conditions. This unifies non-determinism handling across commands and control flow. Changes: - Add ExprOrNondet type for deterministic-or-nondet expressions - Merge set/havoc into single set command with ExprOrNondet RHS - Use ExprOrNondet for ite/loop conditions in Stmt - Add DDM syntax: if (*) and while (*) for nondet conditions - Introduce fresh nondet booleans in PE and StructuredToUnstructured - Update all downstream code, semantics, transforms, backends, tests - Add boolTy to HasNot for declaring fresh boolean variables

…m-in-c

Update test file to use ExprOrNondet (.det/.nondet) instead of Option (some/none) for Cmd and ExprOrNondet for Stmt conditions. Add boolTy to HasNot instance.

.kiro/agents/autopilot-worker.json

MikaelMayer

Thorough and well-structured PR that extends ExprOrNondet from commands to statement-level constructs (ite/loop). The design is clean: the ExprOrNondet type, its .map helper, and the HasNot.boolTy field are good abstractions. Semantics (big-step and small-step), correctness proofs, and all frontends/backends are updated consistently. New tests cover type-checking and evaluation of nondet conditions.

A few observations below, mostly about minor code duplication and one design question about the nondet loop elimination ignoring the measure parameter.

Strata/Languages/Core/DDMTransform/Translate.lean

Strata/Languages/Core/StatementType.lean

Strata/Languages/C_Simp/Verify.lean

Strata/Transform/LoopElim.lean

Strata/Languages/Core/StatementEval.lean

Strata/Languages/C_Simp/Verify.lean

- Extract isBstarArg helper in Translate.lean to reduce duplication - Use ExprOrNondet.map in StatementType.lean and C_Simp/Verify.lean - Add comment explaining why measure is ignored for nondet loops

…m-in-c Resolve conflicts between ExprOrNondet changes (PR #612) and Hoare triple / DetToNondet correctness with loops (PR #660). Key merge decisions: - Keep ExprOrNondet (.det/.nondet) from our branch - Adopt main's Env record (ρ) style and Bool failure flag in EvalCmd - Add nondet ite/loop cases to all new proofs from main - Add loop_sim_nondet for nondet loop correctness proof

Add a .nondet guard branch mirroring LoopElim.lean: havoc assigned vars, assert/assume entry invariants, run body with invariant maintenance, and use .ite .nondet. The catch-all now only matches .det guards without a measure, with a more specific error message.

Examples/NondetCond.core.st

Introduce a CondBool category with condDet (parenthesized bool) and condNondet (*) variants, so nondet conditions parse as 'if * { ... }' and 'while * { ... }' without parentheses. Deterministic conditions retain their parenthesized form 'if (expr) { ... }'. Remove the bstar bool function, now superseded by condNondet.

Strata/Languages/C_Simp/Verify.lean

…m-in-c

Fix none -> .nondet in LaurelToCoreTranslator for init statements introduced by main merge.

…m-in-c

MikaelMayer · 2026-03-28T02:58:52Z

Strata/Languages/C_Simp/Verify.lean

        .assume s!"invariant_{i}" (translate_expr inv) {}

      .ite (.det (translate_expr guard_expr)) ([first_iter_facts, arbitrary_iter_facts, havocd, not_guard] ++ invariant_assumes) [] {}
+    | .det guard_expr, .none, _ =>


This is super nice but that case was not supported in main, was it? If so I would like to see a test that demonstrates this rewriting of core to core, and that the test be human readable.

For all cases

Added StrataTest/Languages/C_Simp/Examples/LoopElimTests.lean with human-readable #guard_msgs tests for the two new loop elimination cases:

Deterministic guard without measure (.det guard_expr, .none, _): Uses a C_Simp program parsed via #strata with a while loop that has an invariant but no decreases clause. The to_core output shows the loop elimination without any measure-related obligations.

Nondet guard (.nondet, _, _): Constructs a C_Simp.Program programmatically (since C_Simp's parser always produces deterministic guards) and passes it through to_core. The output shows the nondet loop elimination with if * { ... } and the entry invariant assert/assume pattern.

The existing LoopTrivial.lean and LoopSimple.lean already cover the .det guard_expr, .some measure, _ case.

…m-in-c

MikaelMayer commented Mar 19, 2026

View reviewed changes

Strata/Backends/CBMC/CoreToCBMC.lean Show resolved Hide resolved

StrataTest/Transform/ProcedureInlining.lean Show resolved Hide resolved

MikaelMayer commented Mar 19, 2026

View reviewed changes

StrataTest/Languages/Core/Tests/StatementTypeTests.lean Show resolved Hide resolved

MikaelMayer commented Mar 24, 2026

View reviewed changes

Strata/Transform/StructuredToUnstructured.lean Outdated Show resolved Hide resolved

MikaelMayer commented Mar 24, 2026

View reviewed changes

.github/CODEOWNERS Show resolved Hide resolved

MikaelMayer changed the title ~~[Strata] Better isolation of non-determinism in Core~~ Better isolation of non-determinism in Core Mar 24, 2026

MikaelMayer commented Mar 24, 2026

View reviewed changes

Examples/NondetCond.core.st Show resolved Hide resolved

MikaelMayer force-pushed the issue-612-better-isolation-of-non-determinism-in-c branch from c79a486 to 3ce8e92 Compare March 26, 2026 15:14

MikaelMayer added 2 commits March 26, 2026 16:26

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

8a06a84

…m-in-c

fix: update CFGToCProverGOTO tests for ExprOrNondet changes

9b42cd6

Update test file to use ExprOrNondet (.det/.nondet) instead of Option (some/none) for Cmd and ExprOrNondet for Stmt conditions. Add boolTy to HasNot instance.

MikaelMayer commented Mar 26, 2026

View reviewed changes

.kiro/agents/autopilot-worker.json Outdated Show resolved Hide resolved

fix: remove .kiro agent files that should not have been committed

2743af0

MikaelMayer commented Mar 26, 2026

View reviewed changes

MikaelMayer added 4 commits March 26, 2026 21:12

refactor: address review comments on PR #617

b1b8fd4

- Extract isBstarArg helper in Translate.lean to reduce duplication - Use ExprOrNondet.map in StatementType.lean and C_Simp/Verify.lean - Add comment explaining why measure is ignored for nondet loops

ci: trigger Build workflow

d168c5a

MikaelMayer commented Mar 27, 2026

View reviewed changes

Examples/NondetCond.core.st Outdated Show resolved Hide resolved

MikaelMayer commented Mar 27, 2026

View reviewed changes

Strata/Languages/C_Simp/Verify.lean Outdated Show resolved Hide resolved

MikaelMayer added 10 commits March 27, 2026 16:27

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

e7e1347

…m-in-c

fix: update ExprOrNondet usage in merged Laurel code

1e5f296

Fix none -> .nondet in LaurelToCoreTranslator for init statements introduced by main merge.

fix: support loop elimination for deterministic guards without measure

582afff

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

b92db6f

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

ff1db0a

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

51b9bd5

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

59fd0c9

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

c9b3cae

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

89010a8

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

e2820dd

…m-in-c

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

3c8bb00

…m-in-c

MikaelMayer commented Mar 28, 2026

View reviewed changes

MikaelMayer added 2 commits March 28, 2026 03:07

Add loop elimination tests for det-no-measure and nondet guard cases

8df0b1d

Merge branch 'main' into issue-612-better-isolation-of-non-determinis…

e5b5cd5

…m-in-c

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Better isolation of non-determinism in Core#617

Better isolation of non-determinism in Core#617
MikaelMayer wants to merge 22 commits intomainfrom
issue-612-better-isolation-of-non-determinism-in-c

MikaelMayer commented Mar 19, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MikaelMayer left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MikaelMayer Mar 28, 2026

Uh oh!

MikaelMayer Mar 28, 2026

Uh oh!

MikaelMayer Mar 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

MikaelMayer commented Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Problem

Solution

Testing

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MikaelMayer Mar 28, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer Mar 28, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer Mar 28, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

MikaelMayer commented Mar 19, 2026 •

edited

Loading