feat: AVM parsing tag validation by jeanmon · Pull Request #12936 · AztecProtocol/aztec-packages

jeanmon · 2025-03-21T15:17:56Z

BEFORE

instr_fetching_acc                   8.56 us     8.56 us     81280
instr_fetching_interactions_acc      5.24 us     5.23 us    132904

AFTER this PR (version with committed column)

instr_fetching_acc                   8.79 us     8.79 us     79677
instr_fetching_interactions_acc      5.74 us     5.74 us    122150

barretenberg/cpp/pil/vm2/instr_fetching.pil

fcarreiro · 2025-03-24T10:41:19Z

barretenberg/cpp/pil/vm2/instr_fetching.pil

I think this file got complex enough that it needs an explainer comment.
I was thinking something like

what this is trying to constrain (without error handling)

step by step explanation of the error "cascading" (eg the interdependencies)

something along the lines of...

The job of this trace is to constrain that the instruction fetching of a bytecode at a given pc is done correctly. That is, that the raw bytes are correctly translated into operands for the fetched opcode. In terms of columns and tables this means <....>

This trace also crucially handles errors. The possible kinds of errors are (from the enum maybe):
ERR_XXX: when xxxx
ERR_YYY: when yyyy

The errors and "deserialization" logic are interdependent, so the relations and lookups are cascaded to induce "temporality". The interrelationships are as follows

first we check if the pc is inside the range of the bytecode (the bytecode is assumed to exist in the bytecode retrieval table and to be non-empty)

then we check if the remaining length........ [or is it done in the same temporality group?]

the lookup is only done when...

we also check the tag but for that we need to correctly have deserialized all the operands so....

I think the above would also help me in reviewing whether the error handling is correct

I restructured. Hopefully it is now more clear.

fcarreiro · 2025-03-24T10:44:41Z

barretenberg/cpp/pil/vm2/instr_fetching.pil

+pol commit sel_has_tag; // With current instruction specs, tag can appear at op2 (SET_XXX) or op3 (CAST_8, CAST_16)
+pol commit sel_tag_is_op2; // (sel_tag_is_op2 == 0 && sel_has_tag == 1) ==> op3 is a tag


Oh man this is so ad-hoc. I'll think if I have any better ideas...

Yep, but that is the best I came with in terms of minimizing columns and relations complexity.

barretenberg/cpp/src/barretenberg/vm2/common/instruction_spec.hpp

fcarreiro

(I almost approved before finding the partial instruction issue)

[the text was: ] I find the PIL file very difficult to follow. I'm convinced of every individual error handling case if I don't think about the connection between them. However, the chaining and guarding is not something I'd be able to defend in court.

I think we'll eventually have to find a standardized way to present a trace with error handling. I mentioned some ideas but it's not clear what would end up being the best.

barretenberg/cpp/pil/vm2/precomputed.pil

barretenberg/cpp/pil/vm2/instr_fetching.pil

fcarreiro · 2025-03-24T21:10:02Z

barretenberg/cpp/pil/vm2/instr_fetching.pil

+// not possible for a malicious prover to toggle any single error when no error should occur.
+// We also prevent from a malicious prover attempting to omit any error.
+// It is sufficient to analyse each error relation by assuming that all the previous ones were
+// not toggled.
+// All this can be derived by logical equivalence: a v (¬a ^ b) <==> a v b
+// Let us denote Ei the error at i). Then:
+//
+// E1 v (¬E1 v E2) v ((¬E1 ^ ¬E2) v E3) v ((¬E1 ^ ¬E2 ^ ¬E3) v E4))) <==>
+//     (E1 v E2)   v (¬(E1 v E2) v E3)  v (¬(E1 v E2 v E3) v E4))) <==>
+//          E1 v E2 v E3                v (¬(E1 v E2 v E3) v E4))) <==>
+// E1 v E2 v E3 v E4
+//
+// This shows that error handling can be proven sound by veryfying that the following predicated
+// are correctly set:
+// E1
+// ¬E1 v E2
+// (¬E1 ^ ¬E2) v E3
+// (¬E1 ^ ¬E2 ^ ¬E3) v E4
+//


I'm a logician, and followed the equivalences, but did not understand what you are trying to prove. It's too general and IMHO not useful to have here.

I didn't really request a proof of soundness and completeness, but if I did want a prove I'd just expect an analysis for each of the error selectors and showing that (1) if 1 then error happens; (2) if error happens then should be 1. That doesn't seem to obviously derive from these formulas.

No need to give a proof, but in my opinion this section confuses.

"If 1 then error happens" is not really clear when a previous error occured. That is why I was proving that it is fine to condition that the previous errors did not occur. This was the whole goal of the "logical" demo. I removed it anyway.

barretenberg/cpp/pil/vm2/instr_fetching.pil

barretenberg/cpp/src/barretenberg/vm2/simulation/lib/serialization.cpp

barretenberg/cpp/src/barretenberg/vm2/simulation/bytecode_manager.cpp

barretenberg/cpp/src/barretenberg/vm2/simulation/lib/serialization.cpp

barretenberg/cpp/src/barretenberg/vm2/simulation/lib/serialization.test.cpp

a tag

BEFORE ``` instr_fetching_acc 8.56 us 8.56 us 81280 instr_fetching_interactions_acc 5.24 us 5.23 us 132904 ``` AFTER this PR (version with committed column) ``` instr_fetching_acc 8.79 us 8.79 us 79677 instr_fetching_interactions_acc 5.74 us 5.74 us 122150 ```

🤖 I have created a new Aztec Packages release --- ## [0.82.3](v0.82.2...v0.82.3) (2025-03-27) ### Features * `msgpack` encoding for `Program` and `WitnessStack` ([#12841](#12841)) ([1e58eb1](1e58eb1)) * 64 bit log type id, 64 bit log metadata ([#12956](#12956)) ([20d734a](20d734a)) * AVM parsing tag validation ([#12936](#12936)) ([56b1f0d](56b1f0d)) * **avm:** add calldata & returndata to context ([#13008](#13008)) ([f03b2e5](f03b2e5)) * **avm:** merkle db hints (part 1) ([#12922](#12922)) ([34ec9e8](34ec9e8)) * **avm:** merkle hints (part 2) ([#13077](#13077)) ([fbbc6c7](fbbc6c7)) * **avm:** vm2 initial context ([#12972](#12972)) ([e2b1361](e2b1361)) * benchmark avm simulator ([#12985](#12985)) ([00fae1b](00fae1b)) * client flows benchmarks ([#13007](#13007)) ([9bf7568](9bf7568)) * gas benchmark for "normal usage" ([#13073](#13073)) ([4eb1156](4eb1156)) * Implement merkle writes in the merkle check gadget ([#13050](#13050)) ([c94fe50](c94fe50)) * LogEncryption trait ([#12942](#12942)) ([0b7e564](0b7e564)) * Node snapshot sync ([#12927](#12927)) ([afde851](afde851)), closes [#12926](#12926) * **p2p:** capture all gossipsub metrics ([#12930](#12930)) ([cc940cb](cc940cb)) * Prover node snapshot sync ([#13097](#13097)) ([1e77efb](1e77efb)) * staking asset handler ([#12968](#12968)) ([af48184](af48184)), closes [#12932](#12932) * stream crs data to disk ([#12996](#12996)) ([d016e4d](d016e4d)), closes [#12948](#12948) * track failed tests. add flake. ([f4936d7](f4936d7)) * Track test history. ([#13037](#13037)) ([036bb32](036bb32)) * track total tx fee ([#12601](#12601)) ([9612a4e](9612a4e)) * Validators sentinel ([#12818](#12818)) ([770695c](770695c)) ### Bug Fixes * added #[derive(Eq)] to EcdsaPublicKeyNote ([#12966](#12966)) ([0c21c74](0c21c74)) * Allow use of local blob sink client ([#13025](#13025)) ([ba8d654](ba8d654)) * **avm:** semicolons are hard ([#12999](#12999)) ([8871c83](8871c83)) * bootstrap network and sponsored fpc devnet ([#13044](#13044)) ([8a47d8b](8a47d8b)) * Bump tsc target ([#13052](#13052)) ([985e83b](985e83b)) * cycle_group fuzzer ([#12921](#12921)) ([69f426e](69f426e)) * **docs:** Fix import errors in aztec.js tutorial ([#12969](#12969)) ([856208a](856208a)) * **docs:** Load token artifact from the compiled source in the sample dapp tutorial ([#12802](#12802)) ([0838084](0838084)), closes [#12810](#12810) * **docs:** Update sponsored fpc docs to use 82.2 syntax ([#13054](#13054)) ([e5d425b](e5d425b)) * **e2e:** p2p ([#13002](#13002)) ([1ece539](1ece539)) * extend e2e 2 pxes timeout. strip color codes for error_regex. ([73820e4](73820e4)) * flake ([6cc9e81](6cc9e81)) * fuzzer on staking asset handler constructor test ([#13101](#13101)) ([d936285](d936285)) * invalid getCommittee function ([#13072](#13072)) ([327341f](327341f)) * mac publish should use clang 18 like x-compiler, and use it ([#12983](#12983)) ([7b83c45](7b83c45)) * make circuit parsing deterministic ([#11772](#11772)) ([76ef873](76ef873)) * parse away trailing slash from consensus host ([#12577](#12577)) ([6701806](6701806)) * prerelease versions should be pushed to install.aztec.network ([#13086](#13086)) ([c4e6039](c4e6039)) * smoke ([#13060](#13060)) ([7756b15](7756b15)) * some flake additions ([58638f1](58638f1)) * sponsored fpc arg parsed correctly ([#12976](#12976)) ([#12977](#12977)) ([a85f530](a85f530)) * starting the sandbox with no pxe should still deploy initial test accounts ([#13047](#13047)) ([d92d895](d92d895)) * Syntax error when running tests via jest after tsc build ([#13051](#13051)) ([f972db9](f972db9)) * Use the correct image in aztec start ([#13058](#13058)) ([06285cd](06285cd)) * yolo fix ([91e2f4b](91e2f4b)) * yolo fix nightly ([b3b3259](b3b3259)) * yolo fix obvious thing to track fails. ([2fee630](2fee630)) * yolo flakes ([e3b030a](e3b030a)) * yolo set -x ([bfd3205](bfd3205)) * yolo we suspect the halt is making tests fail that would have passed ([04e3fa2](04e3fa2)) ### Miscellaneous * `getIndexedTaggingSecretAsSender` oracle cleanup ([#13015](#13015)) ([8e71e55](8e71e55)) * Add a script to generate cpp files for AVM2 ([#13091](#13091)) ([7bb43a9](7bb43a9)) * add default native proving for cli wallet ([#12855](#12855)) ([c0f773c](c0f773c)) * add default native proving for cli wallet retry ([#13028](#13028)) ([b2f4785](b2f4785)) * Alpha testnet into master ([#13033](#13033)) ([d98fdbd](d98fdbd)) * AVM TS - move tag validation outside of instruction constructors ([#13038](#13038)) ([45548ab](45548ab)), closes [#12934](#12934) * **avm:** final codegen nuking ([#13089](#13089)) ([9c82f3f](9c82f3f)) * **avm:** remove codegen (all but flavor) ([#13079](#13079)) ([e1f2bdd](e1f2bdd)) * **bb:** minor acir buf C++ improvements ([#13042](#13042)) ([1ebd044](1ebd044)) * boxes dep cleanup ([#12979](#12979)) ([6540b7c](6540b7c)) * **ci:** less catch all e2e_p2p flakes ([#12737](#12737)) ([2134634](2134634)) * comprehensive cleanup of translator flavor and use inheritance properly in flavors ([#13041](#13041)) ([dc5f78f](dc5f78f)) * compress storage footprint ([#12871](#12871)) ([58c110f](58c110f)) * display warning when installing bb versions < 0.82.0 ([#13027](#13027)) ([7247fe7](7247fe7)) * **docs:** Update docs on fees and various other updates ([#12929](#12929)) ([1dec907](1dec907)) * dump dmesg/net/cpu/mem usage at end of ci run ([#12967](#12967)) ([8877792](8877792)) * fix governance util issue ([#13043](#13043)) ([d768d26](d768d26)) * redundant if in affine from projective constructor ([#13045](#13045)) ([3a7ba2d](3a7ba2d)) * remove addition of dummy ops in mock circuit producer ([#13003](#13003)) ([a64d1dc](a64d1dc)) * remove dummy ops in decider pk ([#13049](#13049)) ([da6d021](da6d021)) * replace relative paths to noir-protocol-circuits ([e1b88f6](e1b88f6)) * replace relative paths to noir-protocol-circuits ([849b4b0](849b4b0)) * replace relative paths to noir-protocol-circuits ([18a02d6](18a02d6)) * Revert "chore: add default native proving for cli wallet ([#12855](#12855))" ([#13013](#13013)) ([98e2576](98e2576)) * Speed up and deflake sentinel test ([#13078](#13078)) ([27f1eca](27f1eca)) * **testnet:** making consensus host mandatory input ([#12716](#12716)) ([d47c74a](d47c74a)) * towards no more mock op_queues ([#12984](#12984)) ([fefffa7](fefffa7)) * update bb version for noir 1.0.0-beta.0+ ([#13026](#13026)) ([dd68074](dd68074)) * update CODEOWNERS to reflect new sync method ([#12998](#12998)) ([a3d1915](a3d1915)) ### Documentation * Add fees to cli reference ([#12884](#12884)) ([4a0fd58](4a0fd58)) --- This PR was generated with [Release Please](https://github.com/googleapis/release-please). See [documentation](https://github.com/googleapis/release-please#release-please).

jeanmon marked this pull request as ready for review March 21, 2025 15:21

jeanmon requested review from IlyasRidhuan, Maddiaa0 and fcarreiro as code owners March 21, 2025 15:21

jeanmon removed request for IlyasRidhuan and Maddiaa0 March 21, 2025 15:21

jeanmon force-pushed the jm/parsing-tag-validation branch from 0433c65 to ee66cc1 Compare March 24, 2025 10:30

jeanmon requested review from dbanks12 and sirasistant as code owners March 24, 2025 10:30

jeanmon removed request for dbanks12 and sirasistant March 24, 2025 10:39

fcarreiro requested changes Mar 24, 2025

View reviewed changes

jeanmon force-pushed the jm/parsing-tag-validation branch from ee66cc1 to 7d29b49 Compare March 24, 2025 17:10

jeanmon requested a review from fcarreiro March 24, 2025 17:15

fcarreiro reviewed Mar 24, 2025

View reviewed changes

jeanmon force-pushed the jm/parsing-tag-validation branch from 7d29b49 to 12ceb86 Compare March 25, 2025 15:32

jeanmon requested a review from fcarreiro March 25, 2025 15:32

fcarreiro approved these changes Mar 25, 2025

View reviewed changes

jeanmon force-pushed the jm/parsing-tag-validation branch from 12ceb86 to 14c4397 Compare March 25, 2025 17:21

jeanmon added 11 commits March 25, 2025 20:38

Add tag memory validation

84d12c8

Trace generation unit tests

e594793

Constraining unit tests

973b8f2

Enhance TS serialization.test.ts to exhaustively check all opcodes with

b1c3d4a

a tag

Add comments in pil

7e4047d

Commit column parsing_err_no_tag

d340a23

Addressing review feedback

0ac85df

Explanations for pil file

b3c6f4c

Addressing review feedback

0f2ea3c

rebase on master

7b927c7

Addressing review feedback

c4698a8

Addressing review feedback

eec8e29

jeanmon force-pushed the jm/parsing-tag-validation branch from 14c4397 to eec8e29 Compare March 25, 2025 20:38

jeanmon merged commit 56b1f0d into master Mar 26, 2025
7 checks passed

jeanmon deleted the jm/parsing-tag-validation branch March 26, 2025 07:43

AztecBot mentioned this pull request Mar 26, 2025

chore(master): release 0.82.3 #12980

Merged

		pol commit sel_has_tag; // With current instruction specs, tag can appear at op2 (SET_XXX) or op3 (CAST_8, CAST_16)
		pol commit sel_tag_is_op2; // (sel_tag_is_op2 == 0 && sel_has_tag == 1) ==> op3 is a tag

Conversation

jeanmon commented Mar 21, 2025 • edited by fcarreiro Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

fcarreiro Mar 24, 2025

Choose a reason for hiding this comment

Uh oh!

jeanmon Mar 25, 2025

Choose a reason for hiding this comment

Uh oh!

fcarreiro Mar 24, 2025

Choose a reason for hiding this comment

Uh oh!

jeanmon Mar 24, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

fcarreiro left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

fcarreiro Mar 24, 2025

Choose a reason for hiding this comment

Uh oh!

jeanmon Mar 25, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jeanmon commented Mar 21, 2025 •

edited by fcarreiro

Loading