Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add --disable-safety-check option #235

Merged
merged 4 commits into from
Dec 4, 2024
Merged
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
7 changes: 7 additions & 0 deletions examples/fixture/asm/kimchi/unused_variables.asm
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
@ noname.0.7.0
@ public inputs: 1

DoubleGeneric<1>
DoubleGeneric<1,0,-1,0,1>
DoubleGeneric<1,0,0,0,-2>
(0,0) -> (2,0)
4 changes: 4 additions & 0 deletions examples/fixture/asm/r1cs/unused_variables.asm
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
@ noname.0.7.0
@ public inputs: 1

2 == (v_1) * (1)
4 changes: 4 additions & 0 deletions examples/unused_variables.no
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
fn main(pub xx: Field, yy: Field) {
let zz = yy + 1;
assert_eq(xx, 2);
}
3 changes: 2 additions & 1 deletion src/backends/kimchi/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -335,6 +335,7 @@ impl Backend for KimchiVesta {
&mut self,
public_output: Option<Var<Self::Field, Self::Var>>,
returned_cells: Option<Vec<KimchiCellVar>>,
disable_safety_check: bool,
) -> Result<()> {
// TODO: the current tests pass even this is commented out. Add a test case for this one.
// important: there might still be a pending generic gate
Expand All @@ -357,7 +358,7 @@ impl Backend for KimchiVesta {
}

for var in 0..self.next_variable {
if !written_vars.contains(&var) {
if !written_vars.contains(&var) && !disable_safety_check {
if let Some(private_cell_var) = self
.private_input_cell_vars
.iter()
Expand Down
2 changes: 1 addition & 1 deletion src/backends/kimchi/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -269,7 +269,7 @@ mod tests {
.unwrap();

let kimchi_vesta = KimchiVesta::new(false);
let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None)?;
let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None, false)?;

let (prover_index, _) = compiled_circuit.compile_to_indexes().unwrap();

Expand Down
1 change: 1 addition & 0 deletions src/backends/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -407,6 +407,7 @@ pub trait Backend: Clone {
&mut self,
public_output: Option<Var<Self::Field, Self::Var>>,
returned_cells: Option<Vec<Self::Var>>,
disable_safety_check: bool,
) -> Result<()>;

/// Generate the witness for a backend.
Expand Down
8 changes: 5 additions & 3 deletions src/backends/r1cs/arkworks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ pub const WITH_PUBLIC_OUTPUT_ARRAY: &str =

pub fn compile_source_code<BF: BackendField>(
code: &str,
disable_safety_check: bool,
) -> Result<CompiledCircuit<R1CS<BF>>, crate::error::Error> {
let mut sources = Sources::new();

Expand All @@ -111,7 +112,7 @@ pub fn compile_source_code<BF: BackendField>(
let mast = mast::monomorphize(tast)?;
let r1cs = R1CS::<BF>::new();
// compile
CircuitWriter::generate_circuit(mast, r1cs)
CircuitWriter::generate_circuit(mast, r1cs, disable_safety_check)
}

#[cfg(test)]
Expand All @@ -124,7 +125,8 @@ mod tests {

#[test]
fn test_arkworks_cs_is_satisfied() {
let compiled_circuit = compile_source_code::<R1csBn254Field>(SIMPLE_ADDITION).unwrap();
let compiled_circuit =
compile_source_code::<R1csBn254Field>(SIMPLE_ADDITION, false).unwrap();
let inputs_public = r#"{"public_input": "2"}"#;
let inputs_private = r#"{"private_input": "2"}"#;

Expand All @@ -148,7 +150,7 @@ mod tests {
#[test]
fn test_arkworks_cs_is_satisfied_array() {
let compiled_circuit =
compile_source_code::<R1csBn254Field>(WITH_PUBLIC_OUTPUT_ARRAY).unwrap();
compile_source_code::<R1csBn254Field>(WITH_PUBLIC_OUTPUT_ARRAY, false).unwrap();
let inputs_public = r#"{"public_input": ["2", "5"]}"#;
let inputs_private = r#"{"private_input": ["8", "2"]}"#;

Expand Down
3 changes: 2 additions & 1 deletion src/backends/r1cs/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -407,6 +407,7 @@ where
&mut self,
public_output: Option<crate::var::Var<Self::Field, Self::Var>>,
returned_cells: Option<Vec<LinearCombination<F>>>,
disable_safety_check: bool,
) -> crate::error::Result<()> {
// store the return value in the public input that was created for that
if let Some(public_output) = public_output {
Expand Down Expand Up @@ -440,7 +441,7 @@ where
continue;
}

if !written_vars.contains(&index) {
if !written_vars.contains(&index) && !disable_safety_check {
if let Some(private_cell_var) = self
.private_input_cell_vars
.iter()
Expand Down
14 changes: 10 additions & 4 deletions src/circuit_writer/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,11 @@ impl<B: Backend> CircuitWriter<B> {
}
}

pub fn generate_circuit(typed: Mast<B>, backend: B) -> Result<CompiledCircuit<B>> {
pub fn generate_circuit(
typed: Mast<B>,
backend: B,
disable_safety_check: bool,
) -> Result<CompiledCircuit<B>> {
// create circuit writer
let mut circuit_writer = CircuitWriter::new(typed, backend);

Expand Down Expand Up @@ -212,9 +216,11 @@ impl<B: Backend> CircuitWriter<B> {
}
}

circuit_writer
.backend
.finalize_circuit(public_output, returned_cells)?;
circuit_writer.backend.finalize_circuit(
public_output,
returned_cells,
disable_safety_check,
)?;

//
Ok(CompiledCircuit::new(circuit_writer))
Expand Down
85 changes: 71 additions & 14 deletions src/cli/cmd_build_and_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,11 @@ pub struct CmdBuild {
/// Run in server mode to help debug and understand the compiler passes.
#[clap(long)]
server_mode: bool,

/// WARNING: This option disables safety checks that ensure each variable is properly constrained.
/// Do not check that every variable is in a constraint
#[arg(long = "disable-safety-check", global = true)]
Copy link
Collaborator

@katat katat Nov 18, 2024

Choose a reason for hiding this comment

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

Maybe adding a doc on why this is necessary in certain cases, and it should not be recommended by default.

disable_safety_check: bool,
}

pub fn cmd_build(args: CmdBuild) -> miette::Result<()> {
Expand All @@ -87,8 +92,13 @@ pub fn cmd_build(args: CmdBuild) -> miette::Result<()> {
};

// build
let (sources, prover_index, verifier_index) =
build(&curr_dir, args.asm, args.debug, &mut server_mode)?;
let (sources, prover_index, verifier_index) = build(
&curr_dir,
args.asm,
args.debug,
&mut server_mode,
args.disable_safety_check,
)?;

// create COMPILED_DIR
let compiled_path = curr_dir.join(COMPILED_DIR);
Expand Down Expand Up @@ -255,6 +265,7 @@ pub fn build(
asm: bool,
debug: bool,
server_mode: &mut Option<crate::server::ServerShim>,
disable_safety_check: bool,
) -> miette::Result<(Sources, ProverIndex, VerifierIndex)> {
// produce all TASTs
let (sources, tast) = produce_all_asts(curr_dir, server_mode)?;
Expand All @@ -263,7 +274,13 @@ pub fn build(
let double_generic_gate_optimization = false;

let kimchi_vesta = KimchiVesta::new(double_generic_gate_optimization);
let compiled_circuit = compile(&sources, tast, kimchi_vesta, server_mode)?;
let compiled_circuit = compile(
&sources,
tast,
kimchi_vesta,
server_mode,
disable_safety_check,
)?;

if asm {
println!("{}", compiled_circuit.asm(&sources, debug));
Expand Down Expand Up @@ -304,6 +321,11 @@ pub struct CmdTest {
/// enable the double generic gate optimization of kimchi (by default noname uses that optimization)
#[clap(long)]
double: bool,

/// WARNING: This option disables safety checks that ensure each variable is properly constrained.
/// Do not check that every variable is in a constraint
#[arg(long = "disable-safety-check", global = true)]
disable_safety_check: bool,
}

pub fn cmd_test(args: CmdTest) -> miette::Result<()> {
Expand All @@ -324,7 +346,13 @@ pub fn cmd_test(args: CmdTest) -> miette::Result<()> {
BackendKind::KimchiVesta(_) => {
let (tast, sources) = typecheck_file(&args.path)?;
let kimchi_vesta = KimchiVesta::new(args.double);
let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None)?;
let compiled_circuit = compile(
&sources,
tast,
kimchi_vesta,
&mut None,
args.disable_safety_check,
)?;

let (prover_index, verifier_index) = compiled_circuit.compile_to_indexes()?;
println!("successfully compiled");
Expand All @@ -343,10 +371,24 @@ pub fn cmd_test(args: CmdTest) -> miette::Result<()> {
println!("proof verified");
}
BackendKind::R1csBls12_381(r1cs) => {
test_r1cs_backend(r1cs, &args.path, public_inputs, private_inputs, args.debug)?;
test_r1cs_backend(
r1cs,
&args.path,
public_inputs,
private_inputs,
args.debug,
args.disable_safety_check,
)?;
}
BackendKind::R1csBn254(r1cs) => {
test_r1cs_backend(r1cs, &args.path, public_inputs, private_inputs, args.debug)?;
test_r1cs_backend(
r1cs,
&args.path,
public_inputs,
private_inputs,
args.debug,
args.disable_safety_check,
)?;
}
}

Expand All @@ -371,6 +413,11 @@ pub struct CmdRun {
/// JSON encoding of the private inputs. Similar to `--public-inputs` but for private inputs.
#[clap(long, value_parser, default_value = "{}")]
private_inputs: Option<String>,

/// WARNING: This option disables safety checks that ensure each variable is properly constrained.
/// Do not check that every variable is in a constraint
#[arg(long = "disable-safety-check", global = true)]
disable_safety_check: bool,
}

pub fn cmd_run(args: CmdRun) -> miette::Result<()> {
Expand All @@ -395,12 +442,20 @@ pub fn cmd_run(args: CmdRun) -> miette::Result<()> {
BackendKind::KimchiVesta(_) => {
unimplemented!("kimchi-vesta backend is not yet supported for this command")
}
BackendKind::R1csBls12_381(r1cs) => {
run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs)?
}
BackendKind::R1csBn254(r1cs) => {
run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs)?
}
BackendKind::R1csBls12_381(r1cs) => run_r1cs_backend(
r1cs,
&curr_dir,
public_inputs,
private_inputs,
args.disable_safety_check,
)?,
BackendKind::R1csBn254(r1cs) => run_r1cs_backend(
r1cs,
&curr_dir,
public_inputs,
private_inputs,
args.disable_safety_check,
)?,
}

Ok(())
Expand All @@ -411,14 +466,15 @@ fn run_r1cs_backend<F>(
curr_dir: &PathBuf,
public_inputs: JsonInputs,
private_inputs: JsonInputs,
disable_safety_check: bool,
) -> miette::Result<()>
where
F: BackendField,
{
// Assuming `curr_dir`, `public_inputs`, and `private_inputs` are available in the scope
let (sources, tast) = produce_all_asts(curr_dir, &mut None)?;

let compiled_circuit = compile(&sources, tast, r1cs, &mut None)?;
let compiled_circuit = compile(&sources, tast, r1cs, &mut None, disable_safety_check)?;

let generated_witness =
generate_witness(&compiled_circuit, &sources, public_inputs, private_inputs)?;
Expand All @@ -445,6 +501,7 @@ fn test_r1cs_backend<F: BackendField>(
public_inputs: JsonInputs,
private_inputs: JsonInputs,
debug: bool,
disable_safety_check: bool,
) -> miette::Result<()>
where
F: BackendField,
Expand All @@ -471,7 +528,7 @@ where
&mut None,
)?;

let compiled_circuit = compile(&sources, tast, r1cs, &mut None)?;
let compiled_circuit = compile(&sources, tast, r1cs, &mut None, disable_safety_check)?;

generate_witness(&compiled_circuit, &sources, public_inputs, private_inputs)?;

Expand Down
26 changes: 24 additions & 2 deletions src/cli/cmd_prove_and_verify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,25 @@ pub struct CmdProve {
/// JSON encoding of the private inputs. Similar to `--public-inputs` but for private inputs.
#[clap(long, value_parser, default_value = "{}")]
private_inputs: String,

/// WARNING: This option disables safety checks that ensure each variable is properly constrained.
/// Do not check that every variable is in a constraint
#[arg(long = "disable-safety-check", global = true)]
disable_safety_check: bool,
}

pub fn cmd_prove(args: CmdProve) -> miette::Result<()> {
let curr_dir = args
.path
.unwrap_or_else(|| std::env::current_dir().unwrap().try_into().unwrap());

let (sources, prover_index, verifier_index) = build(&curr_dir, false, args.debug, &mut None)?;
let (sources, prover_index, verifier_index) = build(
&curr_dir,
false,
args.debug,
&mut None,
args.disable_safety_check,
)?;

// parse inputs
let public_inputs = parse_inputs(&args.public_inputs).unwrap();
Expand Down Expand Up @@ -86,14 +97,25 @@ pub struct CmdVerify {
/// An optional expected public output, in JSON format.
#[clap(short, long, value_parser)]
public_output: Option<String>,

/// WARNING: This option disables safety checks that ensure each variable is properly constrained.
/// Do not check that every variable is in a constraint
#[arg(long = "disable-safety-check", global = true)]
disable_safety_check: bool,
}

pub fn cmd_verify(args: CmdVerify) -> miette::Result<()> {
let curr_dir = args
.path
.unwrap_or_else(|| std::env::current_dir().unwrap().try_into().unwrap());

let (_sources, _prover_index, verifier_index) = build(&curr_dir, false, false, &mut None)?;
let (_sources, _prover_index, verifier_index) = build(
&curr_dir,
false,
false,
&mut None,
args.disable_safety_check,
)?;

// parse inputs
let mut public_inputs = parse_inputs(&args.public_inputs).unwrap();
Expand Down
3 changes: 2 additions & 1 deletion src/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -210,6 +210,7 @@ pub fn compile<B: Backend>(
tast: TypeChecker<B>,
backend: B,
server_mode: &mut Option<crate::server::ServerShim>,
disable_safety_check: bool,
) -> miette::Result<CompiledCircuit<B>> {
// monomorphization pass
let mast = mast::monomorphize(tast)?;
Expand All @@ -228,7 +229,7 @@ pub fn compile<B: Backend>(
serde_json::to_string(&mast).unwrap();

// synthesizer pass
CircuitWriter::generate_circuit(mast, backend).into_miette(sources)
CircuitWriter::generate_circuit(mast, backend, disable_safety_check).into_miette(sources)
}

pub fn generate_witness<B: Backend>(
Expand Down
2 changes: 1 addition & 1 deletion src/negative_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ fn mast_pass(code: &str) -> Result<Mast<R1csBackend>> {

fn synthesizer_pass(code: &str) -> Result<CompiledCircuit<R1csBackend>> {
let mast = mast_pass(code);
CircuitWriter::generate_circuit(mast?, R1CS::new())
CircuitWriter::generate_circuit(mast?, R1CS::new(), false)
}

#[test]
Expand Down
Loading
Loading