Future-proof Scalar conversion to bits#3293
Draft
Antonio95 wants to merge 4 commits into
Draft
Conversation
Contributor
There was a problem hiding this comment.
Pull request overview
This PR introduces end-of-synthesis safety checks to ensure circuit Scalar values are range-checked (via to_bits) even if higher-level circuit operations never trigger bit-conversion during synthesis, preventing future synthesis flows from accidentally producing unchecked scalars.
Changes:
- Track injected circuit
Scalars and automatically convert any still-unconverted ones to bits before circuit ejection in key synthesis flows. - Untrack
Scalars whento_bits_leis invoked (i.e., after the in-circuit range check occurs). - Add tests/bench updates to validate rejection behavior and ensure updated synthesis flows succeed.
Reviewed changes
Copilot reviewed 18 out of 18 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| synthesizer/src/vm/tests/test_v14/mod.rs | Adds a deployment-oriented regression test involving scalar usage. |
| synthesizer/process/src/trace/translation/assignment.rs | Calls convert_unconverted_values() before assignment ejection for translation circuits. |
| synthesizer/process/src/trace/inclusion/assignment.rs | Calls convert_unconverted_values() before assignment ejection for inclusion circuits. |
| synthesizer/process/src/trace/inclusion/assignment_v0.rs | Calls convert_unconverted_values() before assignment ejection for inclusion V0 circuits. |
| synthesizer/process/src/stack/execute.rs | Ensures pending tracked values are converted before ejecting circuit assignment. |
| synthesizer/process/src/stack/call/standard.rs | Ensures pending tracked values are converted before ejecting circuit R1CS for standard calls. |
| synthesizer/process/src/stack/call/dynamic.rs | Ensures pending tracked values are converted before ejecting circuit R1CS for dynamic calls. |
| synthesizer/benches/kary_merkle_tree.rs | Converts pending tracked values prior to bench circuit assignment ejection. |
| ledger/puzzle/epoch/src/synthesis/program/to_r1cs.rs | Converts pending tracked values prior to R1CS ejection in epoch program synthesis. |
| circuit/types/scalar/src/lib.rs | Tracks newly injected scalars and registers a deferred to_bits conversion closure. |
| circuit/types/scalar/src/helpers/to_bits.rs | Untracks scalars once to_bits_le has range-checked them. |
| circuit/environment/src/testnet_circuit.rs | Enforces empty “unconverted values” set on ejection; clears it on reset. |
| circuit/environment/src/helpers/linear_combination.rs | Widens LinearCombination::to_terms visibility to pub(crate) for tracking. |
| circuit/environment/src/helpers/assignment.rs | Adds a test ensuring ejection rejects circuits with unconverted scalars. |
| circuit/environment/src/environment.rs | Implements the unconverted-value tracking set + conversion/check/clear APIs. |
| circuit/environment/src/circuit.rs | Enforces empty “unconverted values” set on ejection; clears it on reset. |
| circuit/environment/src/canary_circuit.rs | Enforces empty “unconverted values” set on ejection; clears it on reset. |
| .circleci/config.yml | Adds a branch-name condition to run expensive merge-workflow jobs. |
| if set.is_empty() { | ||
| Ok(()) | ||
| } else { | ||
| Err(format!("{} unconverted value(s) remain(s) in the tracking set: {:#?}", set.len(), set.keys())) |
Comment on lines
+25
to
+32
| thread_local! { | ||
| /// Stores certain injected values which have not been converted to bits yet, alongside a | ||
| /// closure that converts each of them to bits. | ||
| // This gives higher-level crates the ability to track any values which must be converted to | ||
| // bits before the end of synthesis (e.g. Scalars, which are otherwise never range-checked) and | ||
| // convert them if they have not been. | ||
| static UNCONVERTED_VALUES: RefCell<BTreeMap<u64, Box<dyn FnOnce()>>> = RefCell::new(BTreeMap::new()); | ||
| } |
Comment on lines
+426
to
+448
| match (eject_assignment, inject_unconverted_scalar) { | ||
| // Ejection must fail when an injected scalar was never converted to bits. | ||
| (true, true) => { | ||
| let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(AleoV0::eject_assignment_and_reset)); | ||
| assert!(result.is_err()); | ||
| AleoV0::reset(); | ||
| } | ||
| (false, true) => { | ||
| let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(AleoV0::eject_r1cs_and_reset)); | ||
| assert!(result.is_err()); | ||
| AleoV0::reset(); | ||
| } | ||
| // Ejection succeeds when every injected scalar was converted to bits. | ||
| (true, false) => { | ||
| let _assignment = AleoV0::eject_assignment_and_reset(); | ||
| } | ||
| (false, false) => { | ||
| let _r1cs = AleoV0::eject_r1cs_and_reset(); | ||
| } | ||
| } | ||
|
|
||
| AleoV0::reset(); | ||
| } |
Comment on lines
+91
to
+93
| // Convert all tracked, still-unconverted values to bits. | ||
| A::convert_unconverted_values(); | ||
|
|
Comment on lines
1289
to
+1293
| or pipeline.git.branch == "canary" | ||
| or pipeline.git.branch == "testnet" | ||
| or pipeline.git.branch == "mainnet" | ||
| or pipeline.git.branch == "ensure_finalize_scopes_match" | ||
| or pipeline.git.branch == "scalar_conversion" |
| } | ||
|
|
||
| // Convert all tracked, still-unconverted values to bits. | ||
| A::convert_unconverted_values(); |
Collaborator
There was a problem hiding this comment.
This runs after the is_satisfied() check above, so any constraint added by the conversion here would not be covered by that check and would only fail at prove time. Should the conversion happen before is_satisfied() so a newly added range check is still gated by it?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
(Edit: Converted to draft pending investigation on the possibility of bad-circuit construction)
A
Scalarcircuit value is stored as an underlyingField(i.e. base-field) element. No range checks (i.e. checks that the bit-decomposition of theFieldcorresponds to the canonical representation of aScalarand not, say, to a larger value) occur upon injection. These checks do happen wheneverScalar::to_bitsis called in-circuit (which is also triggered by many other circuit operations)This is not an issue today because the Aleo-instructions language (used to construct transition circuits), record translation and record inclusion all result in circuits satisfying the following: every
Scalarinjected into the circuit is convertedto_bits(and therefore range-checked) at some later point during synthesis. As an example, private and public transition inputs are wrapped in aPlaintextthat gets convertedto_bitswhen the circuit processes the input, i.e. hashes it (public) or encrypts it (private).This PR future-proofs synthesis against failure to convert to bits (i.e. to range-check) all
Scalars. See also the note at the end of the next section for potential independent uses this PR could have in the future.Solution
Scalaris injected into a circuit, it is added to a tracking set.Scalaris converted to bits (which might in turn be caused by many higher-level operations), it is removed from the tracking set.eject_r1cs_and_reset/eject_assignment_and_reset), allScalars not yet converted to bits are so (and i.p. are range-checked).The reason for this flow as opposed to simply range-checking upon injection is that the latter would not be backwards-compatible (right now, many deployed circuits perform some operations between
Scalarinjection and whatever operation it is which triggersto_bits), but the implemented flow is (cf. next section).Going into some more detail, it was not possible to have the tracking set simply contain the variable identifier of still-unconverted
Scalars: because tracking occurs at a lower level than most of our Aleo-type-specific circuit machinery, it is not aware of the existence of ato_bitsfunction it can call directly. For that reason, when tracking a newScalar, an abstract function is stores alongside it, which is alwaysto_bitsin the case of interest. This abstract function which the lower-level knows nothing about is what is called inconvert_unconverted_valuesbefore ejection.Note: The
*_unconverted_valuesmachinery implemented can also be used in the future whenever we need to be able to a) track circuit values, b) untrack circuit values, and c) guarantee that a certain closure is called before the end of synthesis for all still-untracked values.Backwards-compatibility
It has been checked that all
mainnet, test andcanarycircuits in the regressions repository already convert all of theirScalars to bits. In particular, their synthesis remains unaffected after the implemented change, the original certificates also validate and no redeployments are needed.This means the change does not need to be version guarded.
Tests
The main checks were carried out in a separate repo and consisted of the aforementioned regression checks that the updated synthesis doesn’t affect existing transition/translation circuits (or the inclusion one).
A new small test has been added:
test_unconverted_scalar_rejection, which checkseject_r1cs_and_resetandeject_assignment_and_resetindeed reject circuits with still-unconvertedScalars. This fact was also temporarily tested while running the regression tests.