Skip to content

Memory encoding#102

Merged
mira-alford merged 42 commits intomainfrom
memory-encoding
Apr 1, 2026
Merged

Memory encoding#102
mira-alford merged 42 commits intomainfrom
memory-encoding

Conversation

@mira-alford
Copy link
Copy Markdown
Collaborator

@mira-alford mira-alford commented Mar 25, 2026

Initial memory encoding transform/spec experiment. Split encoding is working for basic memory safety (though lacks gammas for now). Some IL examples included for malloc/free.

More importantly for review this includes some fixes to the boogie generation for bugs that came up and the refactor to field read/writes to support custom sorts.

@mira-alford mira-alford requested a review from agle March 25, 2026 05:55
@mira-alford
Copy link
Copy Markdown
Collaborator Author

Interesting... that failing test passes locally.

@katrinafyi
Copy link
Copy Markdown
Collaborator

macos diff has different error output, i'd just uhh pipe 2>/dev/null ig

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

Unfamiliar with cramtest, but something like this @katrinafyi ?

Copy link
Copy Markdown
Owner

@agle agle left a comment

Choose a reason for hiding this comment

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

A doc comment or possibly a well-documented example in a cram test would be good to help understand the signature and expected behaviour of the generated memory encoding contracts.

@mira-alford mira-alford merged commit 5ef15f0 into main Apr 1, 2026
9 checks passed
@mira-alford mira-alford deleted the memory-encoding branch April 1, 2026 05:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants