Add recursive functions to Strata Core#499

Merged

MikaelMayer merged 41 commits intomainfrom

Mar 5, 2026

Commits on Feb 24, 2026

Add recursive info to LFunc
Josh Cohen
committed

Commits on Feb 25, 2026

Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Add generation of axioms for recursive functions
Josh Cohen
committed
Add metadata and error handling
Josh Cohen
committed

Commits on Feb 26, 2026

Add SMT encoding (axioms) for recursive functions
Josh Cohen
committed
Add tests for SMT encoding, fix annotation issue
Josh Cohen
committed
Change to decreases expr, partial support in Translate
Josh Cohen
committed
Add DDM scopeSelf to support recursive functions
Josh Cohen
committed
Fix typechecker recursive issue
Josh Cohen
committed

Commits on Feb 27, 2026

Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Tests for recursive functions
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Combine Translate logic, ensure recfun supports preconditions
Josh Cohen
committed
Small change to test
Josh Cohen
committed
Simplify scopeSelf, add error checks for non-supported features
Josh Cohen
committed
Add comments to Env.addFactoryFunction
Josh Cohen
committed
Add documentation about @[scopeSelf]
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed

Commits on Feb 28, 2026

Fix errors from merge
Josh Cohen
committed
Update small-step semantics for ITE
Josh Cohen
committed
Fix comment with invariant
Josh Cohen
committed

Commits on Mar 2, 2026

Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Improve comments and error messages
Josh Cohen
committed
Fix tests
Josh Cohen
committed
Change "recursive" to "rec"
Josh Cohen
committed

Commits on Mar 3, 2026

Change decreases to @[cases] annotation on parameter
Josh Cohen
committed
Remove references to "decreasing"
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Update test output from safe destructors
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
MikaelMayer
authored

Commits on Mar 4, 2026

Fix test output
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed

Commits on Mar 5, 2026

Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Address review comments
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed
Add top-level info to RecursiveFunctions.md
Josh Cohen
committed
Remove boogie references in docs
Josh Cohen
committed
Fix concrete syntax in doc
Josh Cohen
committed
Merge branch 'main' into josh/rec-fun
Josh Cohen
committed