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.

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

VeyMont: channel invariant, stratified expression containers #1209

Merged
merged 14 commits into from
May 31, 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 adds support for the channel invariant with partial verification support, and refactors+generalizes how stratified expressions are handled in VeyMont. This is basic work required so I can then start working on implementing stratified permissions.

	Getting close

	Not sure what I broke. Code generation code looks nice now tho

	Channel invariant handling seems complete enough for now

	Split up ChorStatement into ChorStatement and EndpointStatement

	Add generalized choreographic expression nodes

	Add boilerplate cases for endpointstatement, chorstatement

	Next: change types in splitchorguards

	Start on using plain branches instead of chorbranch

	Make some progress on SplitChorGuards

And then also formatting!
@bobismijnnaam bobismijnnaam force-pushed the veymont-channelinv-exprs branch from a1ed4a5 to 20f87d9 Compare May 29, 2024 09:50
@bobismijnnaam bobismijnnaam marked this pull request as ready for review May 31, 2024 09:31
@bobismijnnaam bobismijnnaam merged commit 8fdabe4 into dev May 31, 2024
16 of 19 checks passed
@bobismijnnaam bobismijnnaam deleted the veymont-channelinv-exprs branch May 31, 2024 13:53
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.

1 participant