Skip to content

Mutable fields #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
keyboardDrummer wants to merge 150 commits into
base: forJVerify
Choose a base branch
from
Draft

Mutable fields #3

keyboardDrummer wants to merge 150 commits into from

Conversation

@keyboardDrummer
Copy link
Owner

@keyboardDrummer keyboardDrummer commented Jan 16, 2026 •
edited
Loading

Depends on strata-org#308

Changes

  1. Translates Laurel procedures to Core functions when possible (expression body and no contract)
  2. Translates Laurel procedure contracts to Core procedure contracts
  3. Implement Laurel's field access operator for mutable field
  4. Support both types of return value syntax in Laurel
  5. Some support for parsing composite type definitions in Laurel
  6. Identify which Laurel procedures read or mutate the heap, and introduce the Heap as an in or out parameter accordingly

Testing

  • For 1-2, add T5_ProcedureCallsBoogie.lean
  • For 3-5, turn on T1_MutableFields.lean

@keyboardDrummer
Add Laurel grammar and transformation
f3bf3a5
@keyboardDrummer
refactoring
4589663
@keyboardDrummer
Fixes
037a7d1
@keyboardDrummer
Moved tests
1c9cfd1
@keyboardDrummer
Fix grammar test
3a3809c
@keyboardDrummer
Getting there
927b0bb
@keyboardDrummer
TestExamples test passes
faa49df
@keyboardDrummer
Refactoring
4481959
@keyboardDrummer
Fix
c600cf1
@keyboardDrummer
Revert AdvancedMaps changes
25df923
@keyboardDrummer
Add missing license headers
3c933e5
@keyboardDrummer
Revert RealBitVector
f182891
@keyboardDrummer
Tweaks
5bc8abd
@keyboardDrummer
Save state
fe2a831
@keyboardDrummer
Refactoring
2cd178c
@keyboardDrummer
Refactoring
12946cf
@keyboardDrummer
Cleanup
b12d781
@keyboardDrummer
Merge branch 'main' into laurelParsing
75cc85f
@keyboardDrummer
Fix Laurel/TestGrammar
84235b4
@keyboardDrummer
Merge branch 'laurelParsing' of github.com:keyboardDrummer/Strata int…
cffb991 
…o laurelParsing
@keyboardDrummer
Move Boogie examples
b2ae3dc
@keyboardDrummer
Rename
ea3438f
@keyboardDrummer
Merge remote-tracking branch 'origin' into laurelParsing
77aa05a
@keyboardDrummer
Move back Boogie examples
fbe4de5
@keyboardDrummer
Remove white line
e827d76
@keyboardDrummer
Moved examples
ff76419
@keyboardDrummer
Delete Examples.lean files since they're obsolete
ce236d8
@keyboardDrummer
Remove duplication
79fbeb9
@keyboardDrummer
Expand test
b0832e6
@keyboardDrummer
Do not use type and fn feature from DDM
2de306c
@keyboardDrummer
Merge branch 'laurelMoreStmtExpr' into laurelFundamentalsNotSupported
e283b22
@keyboardDrummer
Merge commit 'da9169e0597~1' into laurelFundamentalsNotSupported
fe86098
@keyboardDrummer
Merge commit 'da9169e0597' into laurelFundamentalsNotSupported
ed227ef
@keyboardDrummer
Merge remote-tracking branch 'origin/main' into laurelFundamentalsNot…
b694fae 
…Supported
@keyboardDrummer
Merge branch 'forJVerify' into laurelFundamentalsNotSupported
c5f9687
@keyboardDrummer
Cleanup
3d358ca
@keyboardDrummer
Draft work
086bf22
@keyboardDrummer
Merge branch 'forJVerify' into mutableFields
e6142e3
@keyboardDrummer
Some updates
61b305e
@keyboardDrummer
Updates
0a777e0
@keyboardDrummer
Fix translator
4ab53da
@keyboardDrummer
Start
25c36f5
@keyboardDrummer
Progress
6c964ad
@keyboardDrummer
Some changes
d539bec
@keyboardDrummer
Updates
e4df61f
@keyboardDrummer
Updates
dd16f98
@keyboardDrummer
T1_MutableFields passes, although it's partially commented out
b6cd5c1
@keyboardDrummer
Merge remote-tracking branch 'origin/main' into mutableFields
f4b1ab9
@keyboardDrummer
Merge remote-tracking branch 'fork/forJVerify' into mutableFields
ff3bb23
@keyboardDrummer
Merge remote-tracking branch 'fork/forJVerify' into mutableFields
3a16928
@keyboardDrummer
Add limited procedure calls test
d72523c
@keyboardDrummer
Improved test
2812fc0
@keyboardDrummer
T5_ProcedureCallsBoogie.lean passes now
89aa89a
@keyboardDrummer
Add comment
a9d5c60
@keyboardDrummer
Merge remote-tracking branch 'fork/forJVerify' into mutableFields
e76bd6d
@keyboardDrummer
Use removeIrrelevantAxioms
03a9c58
@keyboardDrummer
Fixes
221ca78
fabiomadge
fabiomadge reviewed Jan 19, 2026
View reviewed changes
StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsBoogie.lean
"

#guard_msgs(drop info, error) in
#eval! testInputWithOffset "T5_ProcedureCallsBoogie" program 20 processLaurelFile
Copy link

@fabiomadge fabiomadge Jan 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this be Core?

fabiomadge
fabiomadge reviewed Jan 19, 2026
View reviewed changes
Strata/Languages/Laurel/LaurelToCoreTranslator.lean
- It has no precondition (or just `true`)
- It has exactly one output parameter (the return type)
-/
def canBeBoogieFunction (proc : Procedure) : Bool :=
Copy link

@fabiomadge fabiomadge Jan 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this be core?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@fabiomadge fabiomadge fabiomadge left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@keyboardDrummer @fabiomadge @aqjune-aws @shigoel