Workaround for unconditionally failing conditional constraints#276
Workaround for unconditionally failing conditional constraints#276
Conversation
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
bytes->field also has a conditional assert issue Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
all now revert to the old, shorter code when test = 1, since the workarounds aren't needed when test = 1. Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
downcast-unsigned is handled by flatten-datatype Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Plugin Test Summary 1 files 3 suites 1s ⏱️ Results for commit c8db17e. ♻️ This comment has been updated with latest results. |
Compactc E2E Test Summary2 841 tests 2 841 ✅ 5m 40s ⏱️ Results for commit c8db17e. ♻️ This comment has been updated with latest results. |
… out to be false also isolated the single use of constrain_type by new-var! to the call site where it is used to check witness return values Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
now using workaround for field->bytes only when len <= max-field the zkir-v2 generator handles downcast-unsigned at a higher level so that the copy isn't inserted when the input is a variable, thereby reducing the added burden of some of the workarounds. added some NBs regarding workarounds so they are marked fixed and that they should be removed later. Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
…s with bits in those productions. this is important because we don't and shouldn't have to verify that the value is non-false where we actually use it. Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
so we can avoid div-mod-power-of-two for the latter Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
Signed-off-by: Kent Dybvig <18339284+dybvig@users.noreply.github.com>
kmillikin
left a comment
kmillikin
left a comment
There was a problem hiding this comment.
Some initial comments.
| (constrain-type (with-output-language (Lflattened Primitive-Type) | ||
| `(tfield ,nat)) | ||
| triv)) | ||
| (if (id? triv) |
There was a problem hiding this comment.
This pass is really hard to reason about!
Isn't triv here always a memory index (a ZKIR instruction output number)? I also don't immediately see why this instruction ignores test.
| (print-gate "private_input" `[guard ,test])) | ||
| (new-var! var type)) | ||
| (let ([index (new-var! var)]) | ||
| ; NB: the public inputs are 0 if a conditionally executed witness |
| (new-var! var type)) | ||
| (let ([index (new-var! var)]) | ||
| ; NB: the public inputs are 0 if a conditionally executed witness | ||
| ; call is not executed, and at present constrain_type is always |
There was a problem hiding this comment.
constrain_type ==> constrain-type
| `(tfield ,nat)) | ||
| triv) | ||
| (print-gate "copy" `[var ,triv])] | ||
| ; NB: flatten-datatypes now implements a workaround that ensures |
There was a problem hiding this comment.
Aha! This comment belongs up in the implementation in Statement!
| (fold-left | ||
| (lambda (instr* var-name primitive-type) | ||
| ; NB: the public inputs are 0 if a conditionally executed witness | ||
| ; call is not executed, and at present constrain_type is always |
There was a problem hiding this comment.
constrain_type ==> emit-constraints-for
| (with-output-language (Lflattened Statement) | ||
| (list `(= ,var-name (bytes->field ,src ,test ,len ,triv1 ,triv2))))) | ||
| (if (eqv? test 1) | ||
| (let-values ([(triv1 triv2) (apply values (list-tail triv* n))]) |
There was a problem hiding this comment.
Can we hoist the let-values and with-output-language out of the arms of the conditional? I find it easier to follow if the body doesn't run away to the right.
There was a problem hiding this comment.
It took me too long to figure out that this was extracting the last two elements of triv* (I think?). It probably needs a comment!
| [t5 (make-temp-id src 't5)] | ||
| [t6 (make-temp-id src 't6)] | ||
| [t7 (make-temp-id src 't7)]) | ||
| (let-values ([(q r) (div-and-mod (max-field) (expt 256 (field-bytes)))]) |
There was a problem hiding this comment.
I also found this very cryptic. It took a long look to recognize that (1) (expt 256 (field-bytes)) is what I think of as (expt 2 (* 8 (field-bytes))) and (2) then it took me a minute to realize that (field-bytes) is the number of full bytes in a the maximum field value, not necessarily the number of full bytes needed to represent the maximum field value (I think?).
So it probably also needs a comment to say what q and r are, or just painfully explicit names.
| `(= ,t1 (< ,(unsigned-bits) ,triv1 ,q)) | ||
| `(= ,t2 (== ,triv1 ,q)) | ||
| `(= ,t3 (< ,(unsigned-bits) ,r ,triv2)) | ||
| `(= ,t4 (select ,t3 0 ,t2)) |
There was a problem hiding this comment.
I think this is t4 = !t3 && t2 but it's hard to see and it's not obvious that's what's intended. Then that would be (r >= triv2) && (triv1 == q). Can we include a little bit of C-style pseudocode so the reader can understand what's intended?
2 participants
Addresses Issue 226 with temporary compiler workarounds. See the issue and the change-log entry for details.