Support transparent procedures by keyboardDrummer · Pull Request #1215 · strata-org/Strata

keyboardDrummer · 2026-05-26T11:51:18Z

DO NOT MERGE - because the base is not main2

Depends on

Formatting and debugging improvements #1115

Base PR for:

Enable calling procedures in contracts keyboardDrummer/Strata#28

Changes

Replace a panic in SMTUtils with a .error
Change handling of free postconditions in Core so they do not generate trivial VCs. This is useful in this PR because this PR is adding new usages of free postconditions and this way existing tests don't get additional "passing" VCs. A side-effect of this change is that existing tests have fewer reported passing VCs.
Improve usage of source locations in the lifting phase, which improves diagnostics
For procedure without a source body, use free postconditions instead of assuming the non-free postconditions in a generated body.
Add the transparency pass. for each non-functional Core procedure, generate a function with the same signature and name suffixed with $asFunction. If a Core procedure is marked as transparent, attempt to generate a functional body for the $asFunction, where assertions are erased and all calls are to functional versions. Tie the functional version to the procedure using a free postcondition.
Refactored CoreGroupingAndOrdering to compute SCC ordering for functions and procedures separately. This is required because TransparencyPass creates a new AST type, UnorderedCoreWithLaurelTypes, where functions and procedures are already separated.

Testing

Updated T20_TransparentBody to account for new feature. In a follow-up we will have many more tests, because we'll convert all functions in tests to procedures.
Added T20_TransparentBodyError to capture some not supported cases

…y pass

…y-pass-only

…trata into transparency-pass-only

joscoh

What happens with transparent recursive procedures? Does it produce a recursive function? If so, what arguments are given for the termination checker, and what happens if the generated function is nonterminating?

joscoh · 2026-05-28T13:44:23Z

-    let mut allDiagnostics := passDiags ++ translateState.diagnostics
+      runTranslateM initState (translateLaurelToCore options program coreWithLaurelTypes)
+    -- Because of the duplication between functions and procedures, this translation is liable to create duplicate diagnostics
+    -- User errors should be checked in an earlier phase, and all dumb translation errors are Strata bugs


What does this mean?

joscoh · 2026-05-28T13:46:28Z

-  let tyVarName := s!"$__ty_unused_{id}"
-  let coreType := LTy.forAll [tyVarName] (.ftvar tyVarName)
+  let ty ← translateType (computeExprType model expr)
+  let coreType := LTy.forAll [] ty


How do you know the type is never polymorphic?

joscoh · 2026-05-28T14:03:02Z

+    - `proof = false` → use unsafe selectors (add `!` suffix) -/
+private def adjustSelectorName (name : String) : String :=
+  -- Only adjust destructor names (contain ".." but are not testers)
+  match name.splitOn ".." with


Minor, but I would prefer having isDestructorName and isTesterName functions in TypeFactory.lean that do this check, to ensure that there aren't silent changes in Core naming that break this.

joscoh · 2026-05-28T14:05:05Z

+
+/-- Build a free postcondition equating the procedure's output to its functional version.
+    For a procedure `foo(a, b) returns (r)`, produces:
+      `r == foo$asFunction(a, b)` -/


IIUC, this pass constructs functions intended to be equivalent to the corresponding procedure and then assumes the equivalence. Is it possible to prove the equivalence instead?

joscoh

It would also be good to see a test where a transparent procedure calls another transparent procedure, with the corresponding function calls

joscoh · 2026-05-28T14:41:45Z

+  { proc with name := funcName, isFunctional := true, body := body, preconditions := [] }
+
+/-- Check whether a function copy has a body (i.e. the procedure was transparent). -/
+private def functionHasBody (proc : Procedure) : Bool :=


Is this function ever called?

joscoh · 2026-05-28T14:42:38Z

+    : UnorderedCoreWithLaurelTypes × SemanticModel :=
+  let fnProgram := unorderedCoreToProgram uc additionalTypes
+  let fnResolveResult := resolve fnProgram existingModel
+  (fromResolvedProgram fnResolveResult.program, fnResolveResult.model)


This silently drops any errors encountered from resolution. Is this intentional?

joscoh · 2026-05-28T14:43:20Z

+        ⟨.StaticCall funcCallee args, e.source⟩
+      else
+        let newName := adjustSelectorName callee.text
+        ⟨ .StaticCall newName args, e.source⟩


This drops any metadata associated with the callee (e.g. source location).

joscoh · 2026-05-28T14:45:43Z

+  mapStmtExpr (fun e =>
+    match e.val with
+    | .StaticCall callee args =>
+      if asFunctionNames.contains callee.text then


A HashSet would be more efficient, but for small programs this is OK

MikaelMayer

🤖🔍 Overall this is a well-structured PR that introduces a clean intermediate representation (UnorderedCoreWithLaurelTypes) and a transparency pass that generates functional versions of procedures. The pipeline extension is logical and the test coverage is reasonable.

Positive notes:

The stripAssertAssume / rewriteCallsToFunctional / mkFreePostcondition decomposition is clean and easy to follow.
The change from .assert to .assume for free postconditions in ProcedureEval.lean is correct — free postconditions should not generate proof obligations.
Replacing panic! with .error in SMTUtils.lean is a good improvement.

See inline comments for issues found.

MikaelMayer · 2026-05-28T14:53:30Z

    match proc.body with
    | .Opaque postconds _ _ | .Abstract postconds =>
-        translateChecks postconds "postcondition"
+        translateChecks postconds s!"postcondition{(bodyStmts.getD []).length}" bodyStmts.isNone


🤖🔍 The label s!"postcondition{(bodyStmts.getD []).length}" encodes the body statement count into the label base (e.g. "postcondition5"). This produces labels like postcondition5_0, postcondition5_1 for multiple postconditions. This seems like a workaround to avoid label collisions — could you add a comment explaining why the body length is embedded in the label name?

MikaelMayer · 2026-05-28T14:53:30Z

@@ -770,6 +770,7 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program)
        emitDiagnostic $ diagnosticFromSource proc.name.source


🤖🔍 This "Instance procedure ... is not yet supported" diagnostic is now emitted in two places: here and in Resolution.lean (the new loop at the top of resolve). This duplication is likely why .eraseDups was added to the pipeline. Consider removing one of the two emission sites rather than relying on deduplication downstream.

MikaelMayer · 2026-05-28T14:53:30Z

+      runTranslateM initState (translateLaurelToCore options program coreWithLaurelTypes)
+    -- Because of the duplication between functions and procedures, this translation is liable to create duplicate diagnostics
+    -- User errors should be checked in an earlier phase, and all dumb translation errors are Strata bugs
+    let mut allDiagnostics: List DiagnosticModel := passDiags ++ translateState.diagnostics.eraseDups;


🤖🔍 Using .eraseDups to suppress duplicate diagnostics is a symptom, not a fix. The root cause is that the same diagnostic (e.g. "Instance procedure ... not yet supported") is emitted in both Resolution.lean and LaurelToCoreTranslator.lean. Fixing the duplication at the source would be cleaner than filtering after the fact.

MikaelMayer · 2026-05-28T14:53:30Z

+    -- Skip functions until we introduce a contract pass,
+    -- which enables lifting procedure calls from contracts
+    p.isFunctional)
+  let asFunctionNames := notSkipped.map (fun p => p.name.text)


🤖🔍 mkFreePostcondition returns LiteralBool true when proc.outputs is not a singleton. This means procedures with zero or multiple outputs silently get no free postcondition tying them to their functional version. The zero-output case is fine (no return value to equate), but the multi-output case could be supported with a conjunction of equalities. Is this intentional or a TODO?

MikaelMayer · 2026-05-28T14:53:31Z

      for diag in unmatchedDiagnostics do
        IO.println s!"  - Line {diag.start.line}, Col {diag.start.column}-{diag.ending.column}: {diag.message}"
+
+    if unmatchedExpectations.length == 0 && unmatchedDiagnostics.length == 0 then


🤖🔍 This branch fires when diagnostics.size != expectedErrors.length but both unmatchedExpectations and unmatchedDiagnostics are empty — which means there are duplicate diagnostics matching the same expectations. The message "Duplicate diagnostics: {repr diagnostics}" dumps the full repr which could be very noisy. Consider printing just the count or the duplicate entries.

MikaelMayer · 2026-05-28T14:53:31Z

+
+/--
+Transparency pass: translate a Laurel program to the UnorderedCoreWithLaurelTypes IR.
+


🤖🔍 transparencyPass always adds a free postcondition to transparent procedures (via addFreePostcondition), which promotes their .Transparent body to .Opaque. This means the original transparent body is now wrapped in an Opaque with an implementation — so the procedure is no longer "transparent" in the Laurel sense after this pass. This is fine architecturally (the function copy carries the transparent semantics), but the docstring on addFreePostcondition could note that this promotion is the expected behavior for transparent procedures.

atomb · 2026-05-28T15:19:39Z

To optimize for reusability, I'd be happier to have a procedure -> function transformation exist at the Core level rather than the Laurel level. It will likely be useful for front-end languages that don't go through Laurel, too.

keyboardDrummer added 8 commits May 26, 2026 10:04

Introduce transparency pass

f246686

Refactoring

9e4ee85

Remove pack multiple outputs pass

7408103

Add error file

4e8fa8b

Update tests

2d19629

Add sources to lift phase

c9fd151

Update tests and improve errors

19987e8

Update comment

24c3983

keyboardDrummer changed the title ~~Transparency pass only~~ Support transparent procedures May 26, 2026

keyboardDrummer mentioned this pull request May 26, 2026

Enable calling procedures in contracts keyboardDrummer/Strata#28

Draft

keyboardDrummer changed the base branch from formatting-and-debugging-improvements to main May 26, 2026 12:38

keyboardDrummer changed the base branch from main to main2 May 26, 2026 12:39

Trigger CI

86962e4

github-actions Bot added Laurel Python Core labels May 26, 2026

keyboardDrummer changed the base branch from main2 to formatting-and-debugging-improvements May 27, 2026 10:19

keyboardDrummer added 3 commits May 27, 2026 10:50

Replace panic with safe access

d192346

Move proof skipping logic from LaurelToCore translator to transparenc…

7a04e66

…y pass

Small refactoring

a45f8f0

keyboardDrummer marked this pull request as ready for review May 28, 2026 09:34

keyboardDrummer requested a review from a team as a code owner May 28, 2026 09:34

Merge branch 'formatting-and-debugging-improvements' into transparenc…

96b2686

…y-pass-only

github-actions Bot added Waiting-For-Review and removed Python labels May 28, 2026

keyboardDrummer added 4 commits May 28, 2026 09:37

Cleanup

d0fdd35

Merge branch 'transparency-pass-only' of github.com:keyboardDrummer/S…

2e0d7e1

…trata into transparency-pass-only

Add missing bindings for PrimitiveOp

2e94fc5

Improve comment

200e828

github-actions Bot added the Python label May 28, 2026

joscoh reviewed May 28, 2026

View reviewed changes

MikaelMayer reviewed May 28, 2026

View reviewed changes

github-actions Bot added the Git conflicts label May 28, 2026

		@@ -770,6 +770,7 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program)
		emitDiagnostic $ diagnosticFromSource proc.name.source


		/--
		Transparency pass: translate a Laurel program to the UnorderedCoreWithLaurelTypes IR.

Conversation

keyboardDrummer commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Testing

Uh oh!

joscoh left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joscoh left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

atomb commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

keyboardDrummer commented May 26, 2026 •

edited

Loading