Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/main' into feat/ir-enhancements
Browse files Browse the repository at this point in the history
  • Loading branch information
katat committed Jan 22, 2025
2 parents 5deab01 + a9a83b8 commit 884877e
Show file tree
Hide file tree
Showing 27 changed files with 1,633 additions and 605 deletions.
33 changes: 33 additions & 0 deletions examples/fixture/asm/kimchi/generic_assert_eq.asm
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
@ noname.0.7.0
@ public inputs: 3

DoubleGeneric<1>
DoubleGeneric<1>
DoubleGeneric<1>
DoubleGeneric<1,0,0,0,-3>
DoubleGeneric<1,0,0,0,-3>
DoubleGeneric<1,0,0,0,-1>
DoubleGeneric<1,0,0,0,-2>
DoubleGeneric<1,0,-1,0,2>
DoubleGeneric<1,0,0,0,-5>
DoubleGeneric<1,0,0,0,-1>
DoubleGeneric<1,0,0,0,-2>
DoubleGeneric<1,0,-1,0,2>
DoubleGeneric<0,0,-1,1>
DoubleGeneric<1,1,-1>
DoubleGeneric<1,1,-1>
DoubleGeneric<1,0,0,0,-5>
DoubleGeneric<1,0,0,0,-1>
DoubleGeneric<1,0,0,0,-1>
DoubleGeneric<1,0,0,0,-2>
DoubleGeneric<1,0,0,0,-3>
DoubleGeneric<1,0,0,0,-4>
DoubleGeneric<1,0,0,0,-5>
(0,0) -> (5,0) -> (9,0) -> (12,1) -> (13,0) -> (16,0) -> (17,0)
(1,0) -> (6,0) -> (10,0) -> (14,0) -> (18,0)
(2,0) -> (3,0) -> (4,0) -> (7,0) -> (11,0) -> (12,0) -> (14,1) -> (19,0)
(7,2) -> (8,0)
(11,2) -> (15,0)
(12,2) -> (13,1)
(13,2) -> (20,0)
(14,2) -> (21,0)
18 changes: 18 additions & 0 deletions examples/fixture/asm/r1cs/generic_assert_eq.asm
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
@ noname.0.7.0
@ public inputs: 3

3 == (v_3) * (1)
3 == (v_3) * (1)
1 == (v_1) * (1)
2 == (v_2) * (1)
5 == (v_3 + 2) * (1)
1 == (v_1) * (1)
2 == (v_2) * (1)
v_4 == (v_3) * (v_1)
5 == (v_3 + 2) * (1)
1 == (v_1) * (1)
1 == (v_1) * (1)
2 == (v_2) * (1)
3 == (v_3) * (1)
4 == (v_1 + v_4) * (1)
5 == (v_2 + v_3) * (1)
2 changes: 2 additions & 0 deletions examples/functions.no
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ fn main(pub one: Field) {
let four = add(one, 3);
assert_eq(four, 4);

// double() should not be folded to return 8
// the asm test will catch the missing constraint if it is folded
let eight = double(4);
assert_eq(eight, double(four));
}
64 changes: 64 additions & 0 deletions examples/generic_assert_eq.no
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
const size = 2;
struct Thing {
xx: Field,
yy: [Field; 2],
}

struct Nestedthing {
xx: Field,
another: [Another; 2],
}

struct Another {
aa: Field,
bb: [Field; 2],
}

fn init_arr(element: Field, const LEN: Field) -> [Field; LEN] {
let arr = [element; LEN];
return arr;
}

fn main(pub public_arr: [Field; 2], pub public_input: Field) {
let generic_arr = init_arr(public_input, size);
let arr = [3, 3];

assert_eq(generic_arr, arr);
let mut concrete_arr = [1, 2];

// instead of the following:
// assert_eq(public_arr[0], concrete_arr[0]);
// assert_eq(public_arr[1], concrete_arr[1]);
// we can write:
assert_eq(public_arr, concrete_arr);

let thing = Thing { xx: 5, yy: [1, 2] };
let other_thing = Thing { xx: generic_arr[0] + 2, yy: public_arr };

// instead of the following:
// assert_eq(thing.xx, other_thing.xx);
// assert_eq(thing.yy[0], other_thing.yy[0]);
// assert_eq(thing.yy[1], other_thing.yy[1]);
// we can write:
assert_eq(thing, other_thing);

let nested_thing = Nestedthing { xx: 5, another: [
Another { aa: public_arr[0], bb: [1, 2] },
Another { aa: generic_arr[1], bb: [4, 5] }
] };
let other_nested_thing = Nestedthing { xx: generic_arr[0] + 2, another: [
Another { aa: 1, bb: public_arr },
Another { aa: 3, bb: [public_arr[0] + (public_input * public_arr[0]), public_arr[1] + public_input] }
] };

// instead of the following:
// assert_eq(nested_thing.xx, other_nested_thing.xx);
// assert_eq(nested_thing.another[0].aa, other_nested_thing.another[0].aa);
// assert_eq(nested_thing.another[0].bb[0], other_nested_thing.another[0].bb[0]);
// assert_eq(nested_thing.another[0].bb[1], other_nested_thing.another[0].bb[1]);
// assert_eq(nested_thing.another[1].aa, other_nested_thing.another[1].aa);
// assert_eq(nested_thing.another[1].bb[0], other_nested_thing.another[1].bb[0]);
// assert_eq(nested_thing.another[1].bb[1], other_nested_thing.another[1].bb[1]);
// we can write:
assert_eq(nested_thing, other_nested_thing);
}
23 changes: 23 additions & 0 deletions examples/log.no
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@

struct Thing {
xx: Field,
yy: Field
}

fn main(pub public_input: Field) -> Field {

log(1234);
log(true);

let arr = [1,2,3];
log(arr);

let thing = Thing { xx : public_input , yy: public_input + 1};

log(thing);

let tup = (1 , true , thing);
log("formatted string with a number {} boolean {} arr {} tuple {} struct {}" , 1234 , true, arr, tup, thing);

return public_input + 1;
}
47 changes: 47 additions & 0 deletions examples/tuple.no
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
struct Thing {
xx: Field,
tuple_field: (Field,Bool)
}

// return tuples from functions
fn Thing.new(xx: Field , tup: (Field,Bool)) -> (Thing , (Field,Bool)) {
return (
Thing {
xx: xx,
tuple_field:tup
},
tup
);
}

fn generic_array_tuple_test(var : ([[Field;NN];LEN],Bool)) -> (Field , [Field;NN]) {
let zero = 0;
let result = if var[1] {var[0][LEN - 1][NN - 1]} else { var[0][LEN - 2][NN - 2] };
return (result , var[0][LEN - 1]);
}

// xx should be 0
fn main(pub xx: [Field; 2]) -> Field {
// creation of new tuple with different types
let tup = (1, true);

// create nested tuples
let nested_tup = ((false, [1,2,3]), 1);
log(nested_tup); // (1, (true , [1,2,3]))

let incr = nested_tup[1]; // 1

// tuples can be input to function
let mut thing = Thing.new(xx[1] , (xx[0] , xx[0] == 0));

// you can access a tuple type just like you access a array
thing[0].tuple_field[0] += incr;
log(thing[0].tuple_field[0]);
let new_allocation = [xx,xx];
let ret = generic_array_tuple_test((new_allocation, true));

assert_eq(thing[0].tuple_field[0] , 1);
log(ret[1]); // logs xx i.e [0,123]

return ret[0];
}
14 changes: 9 additions & 5 deletions src/backends/kimchi/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ use crate::{
backends::kimchi::asm::parse_coeffs,
circuit_writer::{
writer::{AnnotatedCell, Cell, PendingGate},
DebugInfo, Gate, GateKind, Wiring,
DebugInfo, Gate, GateKind, VarInfo, Wiring,
},
compiler::Sources,
constants::Span,
Expand Down Expand Up @@ -128,6 +128,9 @@ pub struct KimchiVesta {
/// Indexes used by the private inputs
/// (this is useful to check that they appear in the circuit)
pub(crate) private_input_cell_vars: Vec<KimchiCellVar>,

/// Log information
pub(crate) log_info: Vec<(Span, VarInfo<VestaField, KimchiCellVar>)>,
}

impl Witness {
Expand Down Expand Up @@ -174,6 +177,7 @@ impl KimchiVesta {
finalized: false,
public_input_size: 0,
private_input_cell_vars: vec![],
log_info: vec![],
}
}

Expand Down Expand Up @@ -428,11 +432,11 @@ impl Backend for KimchiVesta {
self.compute_val(env, &val.0, var.index)
}

fn generate_witness<B: Backend>(
fn generate_witness(
&self,
witness_env: &mut WitnessEnv<VestaField>,
sources: &Sources,
_typed: &Mast<B>,
typed: &Mast<Self>,
) -> Result<GeneratedWitness> {
if !self.finalized {
unreachable!("the circuit must be finalized before generating a witness");
Expand Down Expand Up @@ -481,6 +485,7 @@ impl Backend for KimchiVesta {
}
public_outputs.push(val);
}
self.print_log(witness_env, &self.log_info, sources, typed)?;

// sanity check the witness
for (row, (gate, witness_row, debug_info)) in
Expand Down Expand Up @@ -809,9 +814,8 @@ impl Backend for KimchiVesta {
fn log_var(
&mut self,
var: &crate::circuit_writer::VarInfo<Self::Field, Self::Var>,
msg: String,
span: Span,
) {
println!("todo: implement log_var for kimchi backend");
self.log_info.push((span, var.clone()));
}
}
Loading

0 comments on commit 884877e

Please sign in to comment.