Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .circleci/config.yml
Original file line number Diff line number Diff line change
Expand Up @@ -1290,6 +1290,7 @@ workflows:
or pipeline.git.branch == "testnet"
or pipeline.git.branch == "mainnet"
or pipeline.git.branch == "ensure_finalize_scopes_match"
or pipeline.git.branch == "scalar_conversion"
jobs:
- check-unused-dependencies # This can be cleaned up before releases
- check-cargo-semver-checks # This can be cleaned up before releases
Expand Down
11 changes: 11 additions & 0 deletions circuit/environment/src/canary_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -286,6 +286,9 @@ impl Environment for CanaryCircuit {

/// Returns the R1CS circuit, resetting the circuit.
fn eject_r1cs_and_reset() -> R1CS<Self::BaseField> {
// Ensure all Scalars have been converted to bits.
Self::check_unconverted_values().unwrap();

CANARY_CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -308,6 +311,9 @@ impl Environment for CanaryCircuit {

/// Returns the R1CS assignment of the circuit, resetting the circuit.
fn eject_assignment_and_reset() -> Assignment<<Self::Network as console::Environment>::Field> {
// Ensure all Scalars have been converted to bits.
Self::check_unconverted_values().unwrap();

CANARY_CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -329,6 +335,9 @@ impl Environment for CanaryCircuit {

/// Clears the circuit and initializes an empty environment.
fn reset() {
// Clear the unconverted-values tracking set.
Self::clear_unconverted_values();

CANARY_CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -343,6 +352,8 @@ impl Environment for CanaryCircuit {
assert_eq!(0, circuit.borrow().num_private());
assert_eq!(1, circuit.borrow().num_variables());
assert_eq!(0, circuit.borrow().num_constraints());
// Ensure the unconverted-value tracking set is empty.
assert!(Self::check_unconverted_values().is_ok());
});
}
}
Expand Down
11 changes: 11 additions & 0 deletions circuit/environment/src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -310,6 +310,9 @@ impl Environment for Circuit {

/// Returns the R1CS circuit, resetting the circuit.
fn eject_r1cs_and_reset() -> R1CS<Self::BaseField> {
// Ensure all Scalars have been converted to bits.
Self::check_unconverted_values().unwrap();

CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -332,6 +335,9 @@ impl Environment for Circuit {

/// Returns the R1CS assignment of the circuit, resetting the circuit.
fn eject_assignment_and_reset() -> Assignment<<Self::Network as console::Environment>::Field> {
// Ensure all Scalars have been converted to bits.
Self::check_unconverted_values().unwrap();

CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -353,6 +359,9 @@ impl Environment for Circuit {

/// Clears the circuit and initializes an empty environment.
fn reset() {
// Clear the unconverted-values tracking set.
Self::clear_unconverted_values();

CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -367,6 +376,8 @@ impl Environment for Circuit {
assert_eq!(0, circuit.borrow().num_private());
assert_eq!(1, circuit.borrow().num_variables());
assert_eq!(0, circuit.borrow().num_constraints());
// Ensure the unconverted-value tracking set is empty.
assert!(Self::check_unconverted_values().is_ok());
});
}
}
Expand Down
79 changes: 79 additions & 0 deletions circuit/environment/src/environment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,29 @@ use snarkvm_curves::AffineCurve;
use snarkvm_fields::traits::*;

use core::{fmt, hash};
use std::{cell::RefCell, collections::BTreeMap};

use anyhow::Result;

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 +25 to +32

/// Returns a tracking key for a non-constant variable, or `None` for constants. An index shift of
/// 2^63 is used to distinguish private variables from public ones, as they share the same index space.
fn value_tracking_key<F: PrimeField>(variable: &Variable<F>) -> Option<u64> {
const PRIVATE_FLAG: u64 = 1 << 63;
match variable.mode() {
Mode::Constant => None,
Mode::Public => Some(variable.index()),
Mode::Private => Some(variable.index() | PRIVATE_FLAG),
}
}

/// Attention: Do not use `Send + Sync` on this trait, as it is not thread-safe.
pub trait Environment: 'static + Copy + Clone + fmt::Debug + fmt::Display + Eq + PartialEq + hash::Hash {
Expand Down Expand Up @@ -174,6 +197,62 @@ pub trait Environment: 'static + Copy + Clone + fmt::Debug + fmt::Display + Eq +
/// Sets the constraint limit for the circuit.
fn set_constraint_limit(limit: Option<u64>);

/// Records an injected value which has not been converted to bits yet, alongside a closure
/// that converts it to bits.
// The main purpose of this function is to track (non-constant) Aleo Scalars in higher-level
// crates, whose underlying base-field element is not checked to be in the canonical scalar range
// until to_bits is called.
fn track_unconverted_value(value: &LinearCombination<Self::BaseField>, convert: Box<dyn FnOnce()>) {
if let Some(key) = value.to_terms().iter().find_map(|(variable, _)| value_tracking_key(variable)) {
UNCONVERTED_VALUES.with(|set| {
set.borrow_mut().insert(key, convert);
});
}
}

/// Removes a value from the set of unconverted values.
fn untrack_unconverted_value(value: &LinearCombination<Self::BaseField>) {
UNCONVERTED_VALUES.with(|set| {
let mut set = set.borrow_mut();
for (variable, _) in value.to_terms() {
if let Some(key) = value_tracking_key(variable) {
set.remove(&key);
}
}
});
}

/// Returns `Ok` if no unconverted values remain in the tracking set and `Err` otherwise.
fn check_unconverted_values() -> Result<(), String> {
UNCONVERTED_VALUES.with(|set| {
let set = set.borrow();
if set.is_empty() {
Ok(())
} else {
Err(format!("{} unconverted value(s) remain(s) in the tracking set: {:#?}", set.len(), set.keys()))
}
})
}

/// Converts every unconverted value to bits by calling the stored closure, adding the
/// relevant constraints to the current circuit.
fn convert_unconverted_values() {
// Take ownership of the closures, releasing the borrow before invoking them: each closure is
// a `FnOnce` (so must be consumed by value) and converts a value to bits, which re-enters
// `untrack_unconverted_value` and would otherwise conflict with the outstanding borrow.
let pending: Vec<Box<dyn FnOnce()>> =
UNCONVERTED_VALUES.with(|set| core::mem::take(&mut *set.borrow_mut()).into_values().collect());
for convert in pending {
convert();
}
}

/// Clears the set of unconverted values, dropping the stored conversion closures without
/// invoking them. Used when resetting the circuit between syntheses.
fn clear_unconverted_values() {
UNCONVERTED_VALUES.with(|set| set.borrow_mut().clear());
}

/// Halts the program from further synthesis, evaluation, and execution in the current environment.
fn halt<S: Into<String>, T>(message: S) -> T {
<Self::Network as console::Environment>::halt(message)
Expand Down
65 changes: 65 additions & 0 deletions circuit/environment/src/helpers/assignment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -303,9 +303,11 @@ pub fn compare_constraints<F: PrimeField>(assignment_1: &Assignment<F>, assignme

#[cfg(test)]
mod tests {
use console::TestRng;
use snarkvm_algorithms::{AlgebraicSponge, SNARK, r1cs::ConstraintSynthesizer, snark::varuna::VarunaVersion};
use snarkvm_circuit::prelude::*;
use snarkvm_curves::bls12_377::Fr;
use snarkvm_utilities::Uniform;

/// Compute 2^EXPONENT - 1, in a purposefully constraint-inefficient manner for testing.
fn create_example_circuit<E: Environment>() -> Field<E> {
Expand Down Expand Up @@ -396,4 +398,67 @@ mod tests {
.unwrap()
);
}

fn sample_circuit_for_scalars(
// Whether to inject a scalar which is never converted or not
inject_unconverted_scalar: bool,
// True if the assignment should be ejected, false if the R1CS should be ejected
eject_assignment: bool,
rng: &mut TestRng,
) {
// Inject a few innocuous values and add a constraint.
let field_1 = Field::<AleoV0>::new(Mode::Private, Uniform::rand(rng));
let field_2 = Field::<AleoV0>::new(Mode::Public, Uniform::rand(rng));
let _product = &field_1 * &field_2;

// Inject a Scalar and convert it to bits: this is not problematic.
let scalar = Scalar::<AleoV0>::new(Mode::Private, Uniform::rand(rng));
let _scalar_bits = scalar.to_bits_le();

if inject_unconverted_scalar {
// Inject a private scalar which is never converted to bits: ejection should fail
let _unconverted_scalar = Scalar::<AleoV0>::new(Mode::Private, Uniform::rand(rng));
}

// Hash the injected fields to add a few more constraints.
let _fields_hash = AleoV0::hash_psd8(&[field_1, field_2]);

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 +426 to +448

#[test]
// Checks that a (sample) circuit fails to eject the assignment and the R1CS if a Scalar is
// injected and never converted to bits.
fn test_unconverted_scalar_rejection() {
let rng = &mut TestRng::default();

// Cases with unconverted scalars at the end: panic expected (caught by assert_panics)
sample_circuit_for_scalars(true, true, rng);
sample_circuit_for_scalars(true, false, rng);

// Sanity check: when the (unconverted) scalar is not injected, ejection works
sample_circuit_for_scalars(false, true, rng);
sample_circuit_for_scalars(false, false, rng);
}
}
2 changes: 1 addition & 1 deletion circuit/environment/src/helpers/linear_combination.rs
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ impl<F: PrimeField> LinearCombination<F> {
}

/// Returns the terms (excluding the constant value) in the linear combination.
pub(super) fn to_terms(&self) -> &[(Variable<F>, F)] {
pub(crate) fn to_terms(&self) -> &[(Variable<F>, F)] {
&self.terms
}

Expand Down
11 changes: 11 additions & 0 deletions circuit/environment/src/testnet_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -286,6 +286,9 @@ impl Environment for TestnetCircuit {

/// Returns the R1CS circuit, resetting the circuit.
fn eject_r1cs_and_reset() -> R1CS<Self::BaseField> {
// Ensure all Scalars have been converted to bits.
Self::check_unconverted_values().unwrap();

TESTNET_CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -308,6 +311,9 @@ impl Environment for TestnetCircuit {

/// Returns the R1CS assignment of the circuit, resetting the circuit.
fn eject_assignment_and_reset() -> Assignment<<Self::Network as console::Environment>::Field> {
// Ensure all Scalars have been converted to bits.
Self::check_unconverted_values().unwrap();

TESTNET_CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -329,6 +335,9 @@ impl Environment for TestnetCircuit {

/// Clears the circuit and initializes an empty environment.
fn reset() {
// Clear the unconverted-values tracking set.
Self::clear_unconverted_values();

TESTNET_CIRCUIT.with(|circuit| {
// Reset the witness mode.
IN_WITNESS.with(|in_witness| in_witness.replace(false));
Expand All @@ -343,6 +352,8 @@ impl Environment for TestnetCircuit {
assert_eq!(0, circuit.borrow().num_private());
assert_eq!(1, circuit.borrow().num_variables());
assert_eq!(0, circuit.borrow().num_constraints());
// Ensure the unconverted-value tracking set is empty.
assert!(Self::check_unconverted_values().is_ok());
});
}
}
Expand Down
4 changes: 4 additions & 0 deletions circuit/types/scalar/src/helpers/to_bits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,10 @@ impl<E: Environment> ToBits for &Scalar<E> {
Boolean::assert_less_than_or_equal_constant(&bits_le, &modulus_minus_one.to_bits_le());
}

// Now that underlying Field has been checked to represent a correct Scalar, we remove
// it from the unconverted-value tracking set.
E::untrack_unconverted_value(&LinearCombination::from(&self.field));

bits_le
});
// Extend the vector with the bits of the scalar.
Expand Down
16 changes: 15 additions & 1 deletion circuit/types/scalar/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,21 @@ impl<E: Environment> Inject for Scalar<E> {

// Initialize the scalar as a field element.
match console::ToField::to_field(&scalar) {
Ok(field) => Self { field: Field::new(mode, field), bits_le: OnceCell::new() },
Ok(field) => {
let scalar = Self { field: Field::new(mode, field), bits_le: OnceCell::new() };
// Track the underlying variable so we can detect, at the end of synthesis, any
// scalar that is never range-checked. The closure converts this scalar to bits
// (range-checking it) if it is never otherwise converted during synthesis.
let lc = LinearCombination::from(&scalar.field);
let pending = scalar.clone();
E::track_unconverted_value(
&lc,
Box::new(move || {
let _ = pending.to_bits_le();
}),
);
scalar
}
Err(error) => E::halt(format!("Unable to initialize a scalar circuit as a field element: {error}")),
}
}
Expand Down
3 changes: 3 additions & 0 deletions ledger/puzzle/epoch/src/synthesis/program/to_r1cs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,9 @@ impl<N: Network> EpochProgram<N> {
);
lap!(timer, "Ensure the circuit is satisfied");

// Convert all tracked, still-unconverted values to bits.
A::convert_unconverted_values();

// Eject the R1CS and reset the circuit.
let r1cs = A::eject_r1cs_and_reset();
finish!(timer, "Eject the circuit assignment and reset the circuit");
Expand Down
3 changes: 3 additions & 0 deletions synthesizer/benches/kary_merkle_tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,9 @@ fn batch_prove(c: &mut Criterion) {
let candidate = path.verify(&circuit_leaf_hasher, &circuit_path_hasher, &root, &leaf);
assert!(candidate.eject_value());

// Convert all tracked, still-unconverted values to bits.
CurrentAleo::convert_unconverted_values();

// Eject the assignment.
CurrentAleo::eject_assignment_and_reset()
};
Expand Down
3 changes: 3 additions & 0 deletions synthesizer/process/src/stack/call/dynamic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,9 @@ impl<N: Network> CallTrait<N> for CallDynamic<N> {
// Indicate that external calls are never a root request.
let is_root = false;

// Convert all tracked, still-unconverted values to bits.
A::convert_unconverted_values();

// Eject the existing circuit.
let r1cs = A::eject_r1cs_and_reset();
let (request, caller_response_outputs) = {
Expand Down
3 changes: 3 additions & 0 deletions synthesizer/process/src/stack/call/standard.rs
Original file line number Diff line number Diff line change
Expand Up @@ -255,6 +255,9 @@ impl<N: Network> CallTrait<N> for Call<N> {
// Indicate that external calls are never a root request.
let is_root = false;

// Convert all tracked, still-unconverted values to bits.
A::convert_unconverted_values();

use circuit::Eject;
// Eject the existing circuit.
let r1cs = A::eject_r1cs_and_reset();
Expand Down
3 changes: 3 additions & 0 deletions synthesizer/process/src/stack/execute.rs
Original file line number Diff line number Diff line change
Expand Up @@ -567,6 +567,9 @@ impl<N: Network> Stack<N> {
}
}

// Convert all tracked, still-unconverted values to bits.
A::convert_unconverted_values();

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?


// Eject the circuit assignment and reset the circuit.
let assignment = A::eject_assignment_and_reset();

Expand Down
Loading