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: reinstate old tests & case studies #1114

Merged
merged 59 commits into from
Jan 19, 2024
Merged

VeyMont: reinstate old tests & case studies #1114

merged 59 commits into from
Jan 19, 2024

Conversation

bobismijnnaam
Copy link
Contributor

@bobismijnnaam bobismijnnaam commented Nov 23, 2023 •
edited
Loading

This PR:

  • Reinstates tests from the old VeyMont implementation, as well as from the VeyMont tool paper.
  • Implements functionality in veymont such that communicate statements require their participants to be distinct.
  • Assign statements in seq_progs now cause an error, unless this is disables using a dev flag.

@bobismijnnaam bobismijnnaam changed the title Veymont: reinstate old tests & case studies VeyMont: reinstate old tests & case studies Nov 23, 2023
@bobismijnnaam bobismijnnaam changed the base branch from dev to veymont-full-permission-generation November 23, 2023 13:22
@bobismijnnaam bobismijnnaam force-pushed the veymont-full-permission-generation branch from d0da552 to f80844f Compare November 24, 2023 12:06
@bobismijnnaam
Split up veymont swap into an actual swap and one which just tests a …
a90ba76 
…bunch of stuff
@bobismijnnaam
Move veymont tests around. Add blame for checking precondition of run…
e1e15a8 
…. And tests. Fix the test (veymont-various.pvl) that uncovered this.
@bobismijnnaam
Implement endpoint construction blames.
9b58491 
Implement blames for when endpoint construction inevitably fails. In
addition, add functionality to FilterSpecIgnore s.t. it errors if a
declaration is filtered which is actually in use.
@bobismijnnaam
Apply patches for disabling assign and communicate checks
05b9864
@bobismijnnaam bobismijnnaam force-pushed the veymont-reinstate-old-tests branch from 6a3f16e to 05b9864 Compare November 24, 2023 14:20
Base automatically changed from veymont-full-permission-generation to dev November 24, 2023 14:32
@bobismijnnaam bobismijnnaam mentioned this pull request Dec 7, 2023
Closed
@bobismijnnaam
Make leaderelectstar pass
68a6f89
@bobismijnnaam
Make paperScissorsRock pass
34d081e
@bobismijnnaam
make parallelWhile pass
566dc5b
@bobismijnnaam
Whyyy
2430e03
@bobismijnnaam
Hotfix to fix concurrency bug when progress printing
91fdd59
@bobismijnnaam
Clean up old files
f357233
@bobismijnnaam
Start working on getting spectral-norm working
a3c89bc
@bobismijnnaam
Make Symbexlogger deterministically ordered
9219d7f
@bobismijnnaam
Ensure division by zero error is reported on the dividing node, and n…
11f483b 
…ot in the divisor node
@bobismijnnaam
Include decider/prover asserts in profile. Ensure branch conditions a…
ef0be8b 
…re not reversed in profile.
@bobismijnnaam
Bump silicon commit to include fixes from PR from Marco Eilers
13272d0
@bobismijnnaam
Add back implication that was gone
a98d342
@bobismijnnaam
Bump silicon commit to include marco's qp cache fix. Fix
46cb647 
spectral-norm.pvl.  Add flags to test suite. Add some feedback from
Marco to veymont-tictactoemn.pvl.
@bobismijnnaam
Remove old version without let
b0a58f6
@bobismijnnaam
Make sure only lets within a quantifier are inlined if a trigger over…
3b18464 
… such a let escapes the quantifier body
@bobismijnnaam
Enable veymont-tictactoemn.pvl
6a57034
@bobismijnnaam
add --assumeInjectivityOnInhale
623851f
@bobismijnnaam
Typo
ae1dd5e
@bobismijnnaam
Hopefully ttt-mn is fast enough now!
706ff43
@bobismijnnaam
Increase assert timeout on tictactoemn. Ignore seq port of file
64464fe
@bobismijnnaam
Swap out veymont-tictactoemn.pvl for veymont-tictactoemn-seq.pvl
eaeaf75
@bobismijnnaam
Merge branch 'dev' into veymont-reinstate-old-tests
9fa232c 
Conflicts resolved:
- @family/@scope etc. annotations were added to Node.scala, and I also
  changed some definitions that requires those new annotations.
- I improved division error reporting in ColToSilver, and had to adapt
  that to the new division ast nodes.
- LangSpecificToCol had some imports changed.
@bobismijnnaam bobismijnnaam marked this pull request as ready for review January 17, 2024 10:32
@pieter-bos pieter-bos merged commit 079027e into dev Jan 19, 2024
1 check failed
@pieter-bos pieter-bos deleted the veymont-reinstate-old-tests branch January 19, 2024 14:53
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.
2 participants
@bobismijnnaam @pieter-bos