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: lightweight permissions #1244

Merged
merged 31 commits into from
Sep 25, 2024
Merged

VeyMont: lightweight permissions #1244

merged 31 commits into from
Sep 25, 2024

Conversation

bobismijnnaam
Copy link
Contributor

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

This PR implements a more lightweight model of stratified permission which simplifies the implementation, allows proper functioning of \chor without ad-hoc hacks, and hopefully speeds up verification.

@bobismijnnaam
First draft implementation of lightweight stratified permissions
0a006a8
@bobismijnnaam
Add back error reporting
34f4648
@bobismijnnaam
Disallow nesting endpointExpr and chor
820d5cb
@bobismijnnaam
Simplify use of chor, now that stratified permissions can be used tra…
d130995 
…nsparently
@bobismijnnaam
Fix election-3.pvl
6d50c9e
@bobismijnnaam
Fix 2pc-3
a1052c7
@bobismijnnaam
Fix TicTacToe example
d8cdc8e
@bobismijnnaam
Fix leaderelectring.pvl
31f4795
@bobismijnnaam
Fix FM2023VeyMontSpec
53e267c
@bobismijnnaam
Fix chor/endpointexpr checking errors in TTTlast. Unfortunately, now …
4db37ed 
…it's slow...
@bobismijnnaam
Refactor makeWrappedPerm a bit to have one argument less
983d887
@bobismijnnaam
Extend gitignore, make veymont error clearer
388394f
@bobismijnnaam
Previous commit also extends function specialization approacht to pre…
2e6c681 
…dicates. This works, except in combination with \chor expressions
@bobismijnnaam
Checkpoint before refactoring applicable specialization to not separa…
fc7e90e 
…te by endpoint
@bobismijnnaam
Refactor EncodePermissionStratification to only rely on the specializ…
6bdcd89 
…ing field. This way only one specialized choreographic version is made of each required method/function/predicate.
@bobismijnnaam
Last bit to support predicates as well
7becf37
@bobismijnnaam
Seems to work on TTTlast! Now for validating it...!
9ad65b1
@bobismijnnaam
Fix last few remaining tests
d788953
@bobismijnnaam
Start on finalizing tests for predicate support, but get stuck on a p…
8fa8959 
…arsing error
@bobismijnnaam
Add tests that show shortcoming of stratified predicate encoding
c55eee5
@bobismijnnaam
Add docs about incompleteness in encodePermissionStratification
18f8633
@bobismijnnaam
Remove no longer necessary comments & assumes
7747d8f
@bobismijnnaam
Put unfolding within spec block for java pretty printing
6b41f24
@bobismijnnaam
Add exhalemode 2 to TTTlast, and also crank up the timeout a bit just…
129ab82 
… to be sure.
@bobismijnnaam
Disable test that omer says is unstable, and can be fixed with just e…
700834f 
…ngineering work
@bobismijnnaam
Remove leftover comment in TTTlast/Player.pvl. Make indented rhs of o…
0c0fce9 
…perator only apply to implies, and not to all other rassoc operators
@bobismijnnaam
Move MatrixTransposeWithF to known-problems
e5c6a55
@bobismijnnaam
Remove outdated code & comment
50896dd
@bobismijnnaam
Remove outdated code & comment
6b2af51
@bobismijnnaam
Enable plain assignment within choreographies by default with a warning
648ee61
@bobismijnnaam bobismijnnaam merged commit cd30c48 into dev Sep 25, 2024
19 checks passed
@bobismijnnaam bobismijnnaam deleted the veymont-lightweight-permissions branch September 25, 2024 14:41
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.
1 participant
@bobismijnnaam