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

Rust catch-up #273

Merged
merged 44 commits into from
Dec 12, 2023
Merged

Rust catch-up #273

merged 44 commits into from
Dec 12, 2023

Conversation

giltho
Copy link
Contributor

@giltho giltho commented Nov 30, 2023 •
edited
Loading

Many things here:

  1. Adds the magic wand operator the Asrt.t, and the Package operations, which creates a magic wand from the current state.
  2. Implements aggregate unification plans (or master unification plans), revamping a big part of UP.ml
  3. Adds implication to the formula language, which can be encoded as such to z3
  4. Replace get/set/rem by consumers and consumers, fixes Consumers and producers shouldn't be actions #225
  5. Adds support for list_repeat operator

Not everything should be merged possibly, let's trim some useless prints etc

giltho added 30 commits September 18, 2023 16:12
@giltho
Add wands to the ast
a26499e 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
Add a wands set to the pstate
e16539d 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
defunctorize things that are only ever instantiated to be symbolic
8529612 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
some fixes
fd33c3c 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
Can produce and consume wands
c761e6a 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
basic support for wands in WISL
2f4682e 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
Add package to the syntax, start implementing
378f605 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
magic wand is implemented!
554d71d 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
add parsing for magic wands
9bf791e 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
adds non-empty check for packaging wands
45ae7b1 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
use consumer and producers insteda of get/set/rem
9fe2abe 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
Add splitting mechanism, can't implement its usage in unifier yet
7fd5af4 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
license date update
6372dba 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
implement master unification plans
222d53e 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
splitting mechanism for wand footprint consumption is working!
c7e1d98 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
package lcmd improve printing
9e20973 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
some extensions
156aaff 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
removing batteries, updating printbox yada yada yada
e77478f 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
remove printbox_text dependency of core
9dc4877 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
extract_head passes in Gillian-Rust
e6fdd11 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
fix pretty printing of apply_lem
af7fd5b 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
attempt at something
a9b728c 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
Revert "attempt at something"
76f5078 
This reverts commit a9b728c.
@giltho
add shl infix for Expr
7527ec9 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
forgot to expose
25770db 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
add utility
ba3e52b 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
slight optim of div
f1e3bca 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
helpers
a2035b2 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
temp hack
fec5e32 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
adds implication to the language of formulae
5e61d77 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
giltho added 11 commits November 1, 2023 14:31
@giltho
udpate z3
6730699 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
Revert "udpate z3"
5ec44f2 
This reverts commit 6730699.
@giltho
specialized simpl
99a20b4
@giltho
add support for repeat operation
e02dcd9 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
expose Expr.list_repeat
387d910 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
debug
45a62e2 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
can learn last element of a list also
b668d81 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho
first step of merge, now kanillian upgrade
5ac6222
@giltho
second step of merge, kanillian but only the trivial part
8a12af8
@giltho
done
0476e2a
@giltho
esy-gmp fix
1cfebe5
@giltho
Copy link
Contributor Author

giltho commented Dec 12, 2023 •
edited
Loading

@NatKarmios This can now be reviewed and debugger can be tested independently of the CI passing if it's because of the z3 flakiness

@giltho
fix normalisation of pure expressions
74860c3 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
@giltho giltho requested a review from NatKarmios December 12, 2023 13:58
NatKarmios
NatKarmios reviewed Dec 12, 2023
View reviewed changes
Copy link
Contributor

@NatKarmios NatKarmios left a comment

Choose a reason for hiding this comment

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

LGTM. Just checking debugger still works.

NatKarmios
NatKarmios approved these changes Dec 12, 2023
View reviewed changes
Copy link
Contributor

@NatKarmios NatKarmios left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Yup, debugger looks good

@giltho giltho merged commit c7bbb9e into master Dec 12, 2023
9 checks passed
@giltho giltho deleted the magic-wand branch December 12, 2023 23:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NatKarmios NatKarmios NatKarmios approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Consumers and producers shouldn't be actions
2 participants
@giltho @NatKarmios