Skip to content
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

VeyMont: stratified permissions #1210

Merged
merged 92 commits into from
Jul 18, 2024
Merged

VeyMont: stratified permissions #1210

merged 92 commits into from
Jul 18, 2024

Conversation

bobismijnnaam
Copy link
Contributor

@bobismijnnaam bobismijnnaam commented May 31, 2024 •
edited
Loading

Checklist:

  • The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc.

PR description

  • Support for stratified permissions
  • Make case studies pass
    • TTT
    • TTTmsg
    • TTTlast
  • Implement postponed error reporting functionality
  • Re-enabled all te tests that are disabled because of missing support

Fixes #840.

@bobismijnnaam
Starting on support for stratified permissions
50b6e30
@bobismijnnaam
Basic test case works well. Next up, handling channel invariant
d0d37a8
@bobismijnnaam
Communicates are now encoded using assignment and inhales/exhales for…
80a0925 
… the channel invariant
@bobismijnnaam
Move inequality checking to the inequality pass. Include sender, rece…
0893fec 
…iver, msg in channel invariant.
@bobismijnnaam
Make sure chorperms are also encoded in when nested in endpoint exprs
bf8c010
@bobismijnnaam
Add expInfo for fun and profit. Also make sure read functions are use…
18d2fb8 
…d to read fields after EncodePermissionStratification
@bobismijnnaam
Evaluate chor assign value first, then actually assign to assign loca…
98c0daf 
…tion
@bobismijnnaam
Add veymont fm 2024 paper case studies to veymont folder. add test th…
f4ce4b7 
…at checks for reference.bib in publications folder.
@bobismijnnaam
Move permission generation to the front
f001d2e
@bobismijnnaam
Add base cases for eval, assert when stratifying permissions
17ebd65
@bobismijnnaam
Refactor endpoint to not point to constructor, but to have an expr wi…
127e431 
…th a constructorinvocation. Adjust passes for that. Make EncodeCurrentTHread compatible with choreographies. Move veymont passes to after inlineapplicable.
@bobismijnnaam
Have chor expressions unfold a whole bunch of fields
7de9885
@bobismijnnaam
chor expression hack seems to work, but I need it for nested classes …
d42c5e5 
…as well!
@bobismijnnaam
chor expression now unfolds all permissions of endpoints that occur i…
db3c19f 
…n the expression
@bobismijnnaam
Some changes
3ef77dd
@bobismijnnaam
Make sure trivial lets are inlined so we can still have some assurean…
1535cc3 
…ces about endpoint names literally apperaing in an expression, and not aliased
@bobismijnnaam
Make chor a bit more efficient, it is only really needed on instance …
b34456e 
…functions
@bobismijnnaam
Start outlining specialization for functions
3ec3fd1
@bobismijnnaam
Start working on specialization
4b1094b
@bobismijnnaam
First draft of function specialization support
cf4acb8
@bobismijnnaam
Started on specialization propagation
b68438c
@bobismijnnaam
Stratification seems to work for functions. Now for methods...
a7b3790
@bobismijnnaam
Before rewriting functions/methods to just applicables
2baba3b
@bobismijnnaam
Method specialization seems to work. Now onwards to verifying 0-TTT...
01dbab6
@bobismijnnaam
Add precendece to some expressions. Generate permissions also in chan…
cc24f90 
…nel_invariant
@bobismijnnaam
commenting out channel invariant
0ff712c
@bobismijnnaam
REmove permissions from channel invariant
335638d
@bobismijnnaam
Dirty dirty dirty hack. At least plenty of comments this time to help…
3d5fc01 
… me later
@bobismijnnaam
Almost there...
ba14e89
@bobismijnnaam
Verifies while ignoring branch unanimity!
bc24633
@bobismijnnaam bobismijnnaam marked this pull request as ready for review July 12, 2024 09:25
@bobismijnnaam
Make endpoint inequality generation accomodate the emtpy choreography
8e07ffd
@bobismijnnaam
Refactor EncodePermissionStratification to use the new predicate nodes
2747ef4
@bobismijnnaam
Refactor error reporting for unfolding predicates
8e6a12f
@bobismijnnaam
Merge branch 'dev' into veymont-stratified-permissions
4a1c21e
@bobismijnnaam
Change fold fix
8d7b0d8
@bobismijnnaam
Unfold using write instead of value inside chor expressions
76789e7
@bobismijnnaam
Merge branch 'dev' into veymont-stratified-permissions
432f9a5
@bobismijnnaam
Manage and fix the last few tests
fd5125b
@bobismijnnaam
Double stack size for CI
daaf6a7
@bobismijnnaam
Add blames for channel invariant. Add tests. Fix swap.pvl.
faaf0b1
@bobismijnnaam
Add error message for missing magic wand chunk. Fix TreeWandSilver te…
d545ef6 
…sts.
@bobismijnnaam
Remove tool requirement in rendered cases of wiki generation script
fa0f8a6
@bobismijnnaam
Clean up old todos
38e333c
@bobismijnnaam
Revert todo in TTT case study
04d414a
@bobismijnnaam
Refactor unfold to have no error reason, except when it is inline
9cef36a
@bobismijnnaam
Comment about temporary files
3047e20
@bobismijnnaam
Delete known problems for issue 840, veymont test cases with missing …
8b5f5de 
…annotations. Test cases without a contract on the choreography were not kept.
@bobismijnnaam
Sort all leftover veymont and javabip related impl traits
45f10c2
@bobismijnnaam
Shorten import
0c8c4d4
@bobismijnnaam bobismijnnaam merged commit c4a1921 into dev Jul 18, 2024
16 of 19 checks passed
@bobismijnnaam bobismijnnaam deleted the veymont-stratified-permissions branch July 18, 2024 08:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Veymont examples all lack permissions to verify. Adding the permissions in the necessary places is non-trivial
1 participant
@bobismijnnaam