-
Notifications
You must be signed in to change notification settings - Fork 20
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
Write stack multiset check constraints in AirScript #272
base: andrew-stack-general-constraints
Are you sure you want to change the base?
Write stack multiset check constraints in AirScript #272
Conversation
e48e04b
to
fdc45a1
Compare
constraints/miden-vm/stack.air
Outdated
ev u32and_bus_constraint([stack_top[16]], [b_chip]): | ||
# and_req_val represents bitwise operation request value. | ||
let and_req_val = $alpha[0] + | ||
$alpha[1] * BITWISE_AND + | ||
$alpha[2] * stack_top[0] + | ||
$alpha[3] * stack_top[1] + | ||
$alpha[4] * stack_top[0]' | ||
|
||
# Enforce u32and bus constraint. | ||
enf b_chip' * and_req_val = b_chip |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think we can write bus constraints this way. This captures only one half of the constraint (the request part) but we need to capture both parts (request and response) in the same constraint.
What we should probably do is to create a separate file for each bus and describe bus constraints there fully.
0f3097d
to
445393e
Compare
f2a39c2
to
146c947
Compare
fdc45a1
to
793e0a6
Compare
Partially addressing: #203
This PR adds multiset check constraints for stack operations and removes keywords from evaluator function declaration.