From 4a4fb6970dae9d52b97d9252abea1b28ea178362 Mon Sep 17 00:00:00 2001 From: erhant Date: Wed, 19 Jun 2024 21:11:54 +0300 Subject: [PATCH 1/6] allow array of fields on public output --- .../asm/kimchi/public_output_array.asm | 17 +++++++++++ .../fixture/asm/r1cs/public_output_array.asm | 6 ++++ examples/public_output_array.no | 6 ++++ src/circuit_writer/mod.rs | 13 ++++---- src/tests/examples.rs | 18 +++++++++++ src/type_checker/mod.rs | 30 ++++++++++++++----- 6 files changed, 78 insertions(+), 12 deletions(-) create mode 100644 examples/fixture/asm/kimchi/public_output_array.asm create mode 100644 examples/fixture/asm/r1cs/public_output_array.asm create mode 100644 examples/public_output_array.no diff --git a/examples/fixture/asm/kimchi/public_output_array.asm b/examples/fixture/asm/kimchi/public_output_array.asm new file mode 100644 index 000000000..bc6986b34 --- /dev/null +++ b/examples/fixture/asm/kimchi/public_output_array.asm @@ -0,0 +1,17 @@ +@ noname.0.7.0 + +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,0,0,0,-2> +DoubleGeneric<1,0,-1,0,6> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,-1> +DoubleGeneric<1,-1> +(0,0) -> (7,0) +(1,0) -> (8,0) +(2,0) -> (3,1) -> (6,1) +(3,2) -> (4,0) -> (5,0) -> (6,0) +(5,2) -> (7,1) +(6,2) -> (8,1) diff --git a/examples/fixture/asm/r1cs/public_output_array.asm b/examples/fixture/asm/r1cs/public_output_array.asm new file mode 100644 index 000000000..caee1b5af --- /dev/null +++ b/examples/fixture/asm/r1cs/public_output_array.asm @@ -0,0 +1,6 @@ +@ noname.0.7.0 + +2 == (v_3 + v_4) * (1) +v_5 == (v_3 + v_4) * (v_3) +v_3 + v_4 + 6 == (v_1) * (1) +v_5 == (v_2) * (1) diff --git a/examples/public_output_array.no b/examples/public_output_array.no new file mode 100644 index 000000000..60cd2f870 --- /dev/null +++ b/examples/public_output_array.no @@ -0,0 +1,6 @@ +fn main(pub public_input: Field, private_input: Field) -> [Field; 2] { + let xx = private_input + public_input; + assert_eq(xx, 2); + let yy = xx + 6; + return [yy, xx * public_input]; +} diff --git a/src/circuit_writer/mod.rs b/src/circuit_writer/mod.rs index ec935ae9b..64a7d227e 100644 --- a/src/circuit_writer/mod.rs +++ b/src/circuit_writer/mod.rs @@ -163,12 +163,15 @@ impl CircuitWriter { // create public output if let Some(typ) = &function.sig.return_type { - if typ.kind != TyKind::Field { - unimplemented!(); + match typ.kind.clone() { + TyKind::Field => { + circuit_writer.add_public_outputs(1, typ.span); + } + TyKind::Array(_, len) => { + circuit_writer.add_public_outputs(len as usize, typ.span); + } + _ => unimplemented!(), } - - // create it - circuit_writer.add_public_outputs(1, typ.span); } // public inputs should be handled first diff --git a/src/tests/examples.rs b/src/tests/examples.rs index e13947a8c..b1d86b14e 100644 --- a/src/tests/examples.rs +++ b/src/tests/examples.rs @@ -424,3 +424,21 @@ fn test_literals(#[case] backend: BackendKind) -> miette::Result<()> { Ok(()) } + +#[rstest] +#[case::kimchi_vesta(BackendKind::KimchiVesta(KimchiVesta::new(false)))] +#[case::r1cs(BackendKind::R1csBls12_381(R1CS::new()))] +fn test_public_output_array(#[case] backend: BackendKind) -> miette::Result<()> { + let public_inputs = r#"{"public_input": "1"}"#; + let private_inputs = r#"{"private_input": "1"}"#; + + test_file( + "public_output_array", + public_inputs, + private_inputs, + vec!["8", "2"], + backend, + )?; + + Ok(()) +} diff --git a/src/type_checker/mod.rs b/src/type_checker/mod.rs index ff0cb9d95..3509edc43 100644 --- a/src/type_checker/mod.rs +++ b/src/type_checker/mod.rs @@ -379,14 +379,30 @@ impl TypeChecker { // the output value returned by the main function is also a main_args with a special name (public_output) if let Some(typ) = &function.sig.return_type { if is_main { - if !matches!(typ.kind, TyKind::Field) { - unimplemented!(); + match typ.kind.clone() { + TyKind::Field => { + typed_fn_env.store_type( + "public_output".to_string(), + TypeInfo::new_mut(typ.kind.clone(), typ.span), + )?; + } + TyKind::Array(_, len) => { + println!("ARRAY TYPE OF LENGTH: {}", len); + typed_fn_env.store_type( + "public_output".to_string(), + TypeInfo::new_mut(typ.kind.clone(), typ.span), + )?; + } + _ => unimplemented!(), } - - typed_fn_env.store_type( - "public_output".to_string(), - TypeInfo::new_mut(typ.kind.clone(), typ.span), - )?; + // if typ.kind == TyKind::Field { + // typed_fn_env.store_type( + // "public_output".to_string(), + // TypeInfo::new_mut(typ.kind.clone(), typ.span), + // )?; + // } else if typ.kind == TyKind::Array(items, len) { + // unimplemented!(); + // } } } From c8794187cca7b87017e30b989f864e0100f6f925 Mon Sep 17 00:00:00 2001 From: erhant Date: Wed, 19 Jun 2024 21:16:01 +0300 Subject: [PATCH 2/6] remove comment / log and redundant clones --- src/circuit_writer/mod.rs | 2 +- src/type_checker/mod.rs | 13 ++----------- 2 files changed, 3 insertions(+), 12 deletions(-) diff --git a/src/circuit_writer/mod.rs b/src/circuit_writer/mod.rs index 64a7d227e..916a920ae 100644 --- a/src/circuit_writer/mod.rs +++ b/src/circuit_writer/mod.rs @@ -163,7 +163,7 @@ impl CircuitWriter { // create public output if let Some(typ) = &function.sig.return_type { - match typ.kind.clone() { + match typ.kind { TyKind::Field => { circuit_writer.add_public_outputs(1, typ.span); } diff --git a/src/type_checker/mod.rs b/src/type_checker/mod.rs index 3509edc43..2cf07783f 100644 --- a/src/type_checker/mod.rs +++ b/src/type_checker/mod.rs @@ -379,15 +379,14 @@ impl TypeChecker { // the output value returned by the main function is also a main_args with a special name (public_output) if let Some(typ) = &function.sig.return_type { if is_main { - match typ.kind.clone() { + match typ.kind { TyKind::Field => { typed_fn_env.store_type( "public_output".to_string(), TypeInfo::new_mut(typ.kind.clone(), typ.span), )?; } - TyKind::Array(_, len) => { - println!("ARRAY TYPE OF LENGTH: {}", len); + TyKind::Array(_, _) => { typed_fn_env.store_type( "public_output".to_string(), TypeInfo::new_mut(typ.kind.clone(), typ.span), @@ -395,14 +394,6 @@ impl TypeChecker { } _ => unimplemented!(), } - // if typ.kind == TyKind::Field { - // typed_fn_env.store_type( - // "public_output".to_string(), - // TypeInfo::new_mut(typ.kind.clone(), typ.span), - // )?; - // } else if typ.kind == TyKind::Array(items, len) { - // unimplemented!(); - // } } } From 3aa65fb5b1e9ea097b054f65e96ae8768c061673 Mon Sep 17 00:00:00 2001 From: erhant Date: Thu, 20 Jun 2024 11:58:32 +0300 Subject: [PATCH 3/6] allow only fields and bools for the array output --- src/circuit_writer/mod.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/circuit_writer/mod.rs b/src/circuit_writer/mod.rs index 916a920ae..cbaed3f15 100644 --- a/src/circuit_writer/mod.rs +++ b/src/circuit_writer/mod.rs @@ -163,12 +163,16 @@ impl CircuitWriter { // create public output if let Some(typ) = &function.sig.return_type { - match typ.kind { + match typ.kind.clone() { TyKind::Field => { circuit_writer.add_public_outputs(1, typ.span); } - TyKind::Array(_, len) => { - circuit_writer.add_public_outputs(len as usize, typ.span); + TyKind::Array(item_ty, len) => { + if item_ty.same_as(&TyKind::Field) || item_ty.same_as(&TyKind::Bool) { + circuit_writer.add_public_outputs(len as usize, typ.span); + } else { + unimplemented!("only array of fields are allowed for now"); + } } _ => unimplemented!(), } From 6d7f6898e5265ccf3cac309c52912c4e38b93bc9 Mon Sep 17 00:00:00 2001 From: erhant Date: Thu, 20 Jun 2024 19:44:00 +0300 Subject: [PATCH 4/6] public output respects the size of returned type --- .../fixture/asm/kimchi/types_array_output.asm | 28 +++++++++++++++++++ .../fixture/asm/r1cs/types_array_output.asm | 8 ++++++ examples/types_array_output.no | 21 ++++++++++++++ src/circuit_writer/mod.rs | 16 ++--------- src/tests/examples.rs | 18 ++++++++++++ 5 files changed, 78 insertions(+), 13 deletions(-) create mode 100644 examples/fixture/asm/kimchi/types_array_output.asm create mode 100644 examples/fixture/asm/r1cs/types_array_output.asm create mode 100644 examples/types_array_output.no diff --git a/examples/fixture/asm/kimchi/types_array_output.asm b/examples/fixture/asm/kimchi/types_array_output.asm new file mode 100644 index 000000000..71c87d11e --- /dev/null +++ b/examples/fixture/asm/kimchi/types_array_output.asm @@ -0,0 +1,28 @@ +@ noname.0.7.0 + +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<1> +DoubleGeneric<2,0,-1> +DoubleGeneric<2,0,-1> +DoubleGeneric<2,0,-1> +DoubleGeneric<1,-1> +DoubleGeneric<2,0,-1> +DoubleGeneric<1,-1> +DoubleGeneric<1,-1> +DoubleGeneric<1,-1> +DoubleGeneric<1,-1> +DoubleGeneric<1,-1> +(0,0) -> (12,0) +(1,0) -> (13,0) +(2,0) -> (14,0) +(3,0) -> (15,0) +(4,0) -> (6,0) -> (8,0) -> (14,1) +(5,0) -> (7,0) -> (10,0) -> (13,1) +(6,2) -> (9,1) -> (12,1) +(7,2) -> (11,1) -> (15,1) +(8,2) -> (9,0) +(10,2) -> (11,0) diff --git a/examples/fixture/asm/r1cs/types_array_output.asm b/examples/fixture/asm/r1cs/types_array_output.asm new file mode 100644 index 000000000..ad73bd17d --- /dev/null +++ b/examples/fixture/asm/r1cs/types_array_output.asm @@ -0,0 +1,8 @@ +@ noname.0.7.0 + +2 * v_5 == (2 * v_5) * (1) +2 * v_6 == (2 * v_6) * (1) +2 * v_5 == (v_1) * (1) +v_6 == (v_2) * (1) +v_5 == (v_3) * (1) +2 * v_6 == (v_4) * (1) diff --git a/examples/types_array_output.no b/examples/types_array_output.no new file mode 100644 index 000000000..43c75493e --- /dev/null +++ b/examples/types_array_output.no @@ -0,0 +1,21 @@ +struct Thing { + xx: Field, + yy: Field, +} + +fn main(pub xx: Field, pub yy: Field) -> [Thing; 2] { + let thing1 = Thing { + xx: xx * 2, + yy: yy, + }; + let thing2 = Thing { + xx: xx, + yy: yy * 2, + }; + let things = [thing1, thing2]; + + assert_eq(things[1].xx * 2, things[0].xx); + assert_eq(things[0].yy * 2, things[1].yy); + + return things; +} diff --git a/src/circuit_writer/mod.rs b/src/circuit_writer/mod.rs index cbaed3f15..7ab529941 100644 --- a/src/circuit_writer/mod.rs +++ b/src/circuit_writer/mod.rs @@ -163,19 +163,9 @@ impl CircuitWriter { // create public output if let Some(typ) = &function.sig.return_type { - match typ.kind.clone() { - TyKind::Field => { - circuit_writer.add_public_outputs(1, typ.span); - } - TyKind::Array(item_ty, len) => { - if item_ty.same_as(&TyKind::Field) || item_ty.same_as(&TyKind::Bool) { - circuit_writer.add_public_outputs(len as usize, typ.span); - } else { - unimplemented!("only array of fields are allowed for now"); - } - } - _ => unimplemented!(), - } + // whatever is the size of return type, we need to add that many public outputs + let size_of = circuit_writer.size_of(&typ.kind); + circuit_writer.add_public_outputs(size_of, typ.span); } // public inputs should be handled first diff --git a/src/tests/examples.rs b/src/tests/examples.rs index b1d86b14e..399857278 100644 --- a/src/tests/examples.rs +++ b/src/tests/examples.rs @@ -442,3 +442,21 @@ fn test_public_output_array(#[case] backend: BackendKind) -> miette::Result<()> Ok(()) } + +#[rstest] +#[case::kimchi_vesta(BackendKind::KimchiVesta(KimchiVesta::new(false)))] +#[case::r1cs(BackendKind::R1csBls12_381(R1CS::new()))] +fn test_types_array_output(#[case] backend: BackendKind) -> miette::Result<()> { + let public_inputs = r#"{"xx": "1", "yy": "4"}"#; + let private_inputs = r#"{}"#; + + test_file( + "types_array_output", + public_inputs, + private_inputs, + vec!["2", "4", "1", "8"], // 2x, y, x, 2y + backend, + )?; + + Ok(()) +} From 30f31ab61904e09dc2391c1f8f1e302eb67835a9 Mon Sep 17 00:00:00 2001 From: erhant Date: Thu, 20 Jun 2024 20:05:30 +0300 Subject: [PATCH 5/6] use `BTreeMap` instead of `HashMap` for Kimchi public outputs --- src/backends/kimchi/mod.rs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index fb77f5633..fb34c7c73 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -3,7 +3,7 @@ pub mod builtin; pub mod prover; use std::{ - collections::{HashMap, HashSet}, + collections::{BTreeMap, HashMap, HashSet}, fmt::Write, ops::Neg as _, }; @@ -243,12 +243,18 @@ impl KimchiVesta { } } -#[derive(Default, Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[derive(Default, Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Ord)] pub struct KimchiCellVar { index: usize, pub span: Span, } +impl PartialOrd for KimchiCellVar { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.index.cmp(&other.index)) + } +} + impl BackendVar for KimchiCellVar {} impl KimchiCellVar { @@ -391,7 +397,7 @@ impl Backend for KimchiVesta { let mut witness = vec![]; // compute each rows' vars, except for the deferred ones (public output) - let mut public_outputs_vars: HashMap> = HashMap::new(); + let mut public_outputs_vars: BTreeMap> = BTreeMap::new(); // calculate witness except for public outputs for (row, row_of_vars) in self.witness_table.iter().enumerate() { From f6a563de66332912b8e3f48eec9b6ab0382894c4 Mon Sep 17 00:00:00 2001 From: erhant Date: Fri, 21 Jun 2024 01:29:23 +0300 Subject: [PATCH 6/6] use `educe(PartialOrd)` instead of impl --- Cargo.toml | 2 +- src/backends/kimchi/mod.rs | 11 ++++------- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index e0807f744..1d736a14d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,7 +12,7 @@ ark-ff = "0.3.0" ark-bls12-381 = "0.3.0" # bls12-381 curve for r1cs backend ark-bn254 = "0.3.0" # bn128 curve for r1cs backend ark-serialize = "0.3.0" # serialization of arkworks types -educe = { version = "0.6", default-features = false, features = ["Hash", "PartialEq"] } +educe = { version = "0.6", default-features = false, features = ["Hash", "PartialEq", "PartialOrd"] } ena = "0.14.0" # union-find implementation for the wiring num-bigint = "0.4.3" # big int library camino = "1.1.1" # to replace Path and PathBuf diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index fb34c7c73..095ddd30b 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -2,6 +2,7 @@ pub mod asm; pub mod builtin; pub mod prover; +use educe::Educe; use std::{ collections::{BTreeMap, HashMap, HashSet}, fmt::Write, @@ -243,18 +244,14 @@ impl KimchiVesta { } } -#[derive(Default, Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Ord)] +#[derive(Default, Clone, Copy, Debug, Eq, Hash, Serialize, Deserialize, PartialEq, Ord, Educe)] +#[educe(PartialOrd)] pub struct KimchiCellVar { index: usize, + #[educe(PartialOrd(ignore))] pub span: Span, } -impl PartialOrd for KimchiCellVar { - fn partial_cmp(&self, other: &Self) -> Option { - Some(self.index.cmp(&other.index)) - } -} - impl BackendVar for KimchiCellVar {} impl KimchiCellVar {