fix!: more missing boolean constraints in calldata, calldata hashing, sha256 mem PILs#19367
Conversation
dbanks12
requested review from
IlyasRidhuan,
Maddiaa0,
fcarreiro and
jeanmon
as code owners
dbanks12
requested review from
MirandaWood
and removed request for
IlyasRidhuan,
Maddiaa0 and
fcarreiro
dbanks12
force-pushed
the
db/more-bools
branch
from
b3b0f35 to
771c6d3
Compare
| //////////////////////////////////////////////// | ||
| pol commit start; | ||
| pol commit start; // @boolean | ||
| start * (1 - start) = 0; | ||
| start * (1 - sel) = 0; |
There was a problem hiding this comment.
I couldn't convince myself that this was secure without the explicit boolean constraint. For this instance and others, I think we should consider... is it really worth omitting explicit boolean constraints? If it makes it easier to reason about, what is the real cost?
There was a problem hiding this comment.
Actually it is not necessary but I would add the following explanations:
start * (1 - sel) = 0; means that start != 0 ==> sel == 1 or equivalently sel == 0 ==> start == 0
And from #[START_AFTER_LAST], we have sel == 1 ==> start is boolean.
Together, we have the guarantee that start is boolean.
There was a problem hiding this comment.
I wonder if it's really worth leaving such things "implicitly" constrained. What might be the cost of constraining EVERY boolean explicitly? These things are quite hard to read about and we're going to have comments all over like "this is implicitly constrained to be boolean because of X, Y, Z" that will probably add time to audits
MirandaWood
left a comment
MirandaWood
left a comment
There was a problem hiding this comment.
Nice! I think for calldata we assumed some of these weren't necessary (calldata.pil is essentially just hints, and is looked up into by a usually constrained local sel, and calldata_hashing looks up the posiedon trace via sel for every active row). But as you say it's much easier to reason about when we're explicit! 🚀
dbanks12
force-pushed
the
db/more-bools
branch
from
771c6d3 to
c1d3546
Compare
BEGIN_COMMIT_OVERRIDE feat(avm)!: optionally use TS logger in C++ simulation (#19305) chore(avm): bytecode caching comments chore(avm): disable VK hash checking in tests fix(avm)!: instr_fetching soundness bug (#19381) fix(avm): dont catch wide exceptions (#19388) refactor(avm): Refactor get contract instance fuzzer backfill (#19387) feat(avm): mutate enqueued calls (#19315) chore(avm): migrate to BB asserts (#19395) fix!: more missing boolean constraints in calldata, calldata hashing, sha256 mem PILs (#19367) feat(avm): defensively assert cd hashes (#19346) chore: annotate booleans in PIL, and add some missing boolean constraints (#19371) fix!: missing boolean constraints on zero checks targets (#19401) fix!: context did not constrain returndata size to 0 at start, and had a misnamed relation (#19404) END_COMMIT_OVERRIDE
3 participants
Found by claude