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

Minor LEM changes #809

Merged
merged 1 commit into from
Oct 30, 2023
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
12 changes: 6 additions & 6 deletions src/lem/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,7 @@
) -> Result<Vec<(Vec<AllocatedNum<F>>, AllocatedVal<F>)>> {
assert!(
slots_data.len() == num_slots,
"collected preimages not equal to the number of available slots"

Check warning on line 279 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L279

Added line #L279 was not covered by tests
);

let mut preallocations = Vec::with_capacity(num_slots);
Expand Down Expand Up @@ -541,19 +541,19 @@

match op {
Op::Cproc(out, sym, inp) => {
let cproc = ctx

Check warning on line 544 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L544

Added line #L544 was not covered by tests
.lang
.lookup_by_sym(sym)
.ok_or_else(|| anyhow!("Coprocessor for {sym} not found"))?;
let not_dummy_and_not_blank = not_dummy.get_value() == Some(true) && !ctx.blank;

Check warning on line 548 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L548

Added line #L548 was not covered by tests
let collected_z_ptrs = if not_dummy_and_not_blank {
let collected_ptrs = &ctx.cproc_outputs[cproc_idx];

Check warning on line 550 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L550

Added line #L550 was not covered by tests
if out.len() != collected_ptrs.len() {
bail!("Incompatible output length for coprocessor {sym}")
}
collected_ptrs
.iter()
.map(|ptr| ctx.store.hash_ptr(ptr).expect("hash_ptr failed"))

Check warning on line 556 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L556

Added line #L556 was not covered by tests
.collect::<Vec<_>>()
} else {
vec![ZPtr::dummy(); out.len()]
Expand All @@ -564,8 +564,8 @@
let inp_ptrs = bound_allocations.get_many_ptr(inp)?;
let synthesize_output = cproc.synthesize_lem_internal(
&mut cs.namespace(|| format!("Coprocessor {sym}")),
ctx.global_allocator,
ctx.store,

Check warning on line 568 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L567-L568

Added lines #L567 - L568 were not covered by tests
not_dummy,
&inp_ptrs,
)?;
Expand Down Expand Up @@ -1333,7 +1333,7 @@
)?;
} else {
assert!(!cs.is_witness_generator());
let slots_allocations = build_slots_allocations(cs, store, frame, &self.slot)?;
let slots_allocations = build_slots_allocations(cs, store, frame, &self.slots_count)?;
let hash4_slots = &slots_allocations.hash4.iter().collect::<Vec<_>>();
let hash6_slots = &slots_allocations.hash6.iter().collect::<Vec<_>>();
let hash8_slots = &slots_allocations.hash8.iter().collect::<Vec<_>>();
Expand Down Expand Up @@ -1549,11 +1549,11 @@
};

// fixed cost for each slot
let slot_constraints = 289 * self.slot.hash4
+ 337 * self.slot.hash6
+ 388 * self.slot.hash8
+ 265 * self.slot.commitment
+ bit_decomp_cost * self.slot.bit_decomp;
let slot_constraints = 289 * self.slots_count.hash4
+ 337 * self.slots_count.hash6
+ 388 * self.slots_count.hash8
+ 265 * self.slots_count.commitment
+ bit_decomp_cost * self.slots_count.bit_decomp;

Check warning on line 1556 in src/lem/circuit.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/circuit.rs#L1552-L1556

Added lines #L1552 - L1556 were not covered by tests
let num_constraints = recurse(&self.body, globals, store, false);
slot_constraints + num_constraints + globals.len()
}
Expand Down
2 changes: 1 addition & 1 deletion src/lem/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1785,7 +1785,7 @@
let mut cs = TestConstraintSystem::<Fr>::new();
let lang: Lang<Fr, Coproc<Fr>> = Lang::new();
let _ = func.synthesize_frame_aux(&mut cs, &store, &frame, &lang);
assert_eq!(func.slot, NUM_SLOTS);
assert_eq!(func.slots_count, NUM_SLOTS);

Check warning on line 1788 in src/lem/eval.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/eval.rs#L1788

Added line #L1788 was not covered by tests
assert_eq!(cs.num_inputs(), NUM_INPUTS);
assert_eq!(
(cs.aux().len(), cs.num_constraints()),
Expand Down
14 changes: 7 additions & 7 deletions src/lem/interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ pub struct Hints<F: LurkField> {

impl<F: LurkField> Hints<F> {
pub fn new_from_func(func: &Func) -> Hints<F> {
let slot = func.slot;
let slot = func.slots_count;
let hash4 = Vec::with_capacity(slot.hash4);
let hash6 = Vec::with_capacity(slot.hash6);
let hash8 = Vec::with_capacity(slot.hash8);
Expand All @@ -86,7 +86,7 @@ impl<F: LurkField> Hints<F> {
}

pub fn blank(func: &Func) -> Hints<F> {
let slot = func.slot;
let slot = func.slots_count;
let hash4 = vec![None; slot.hash4];
let hash6 = vec![None; slot.hash6];
let hash8 = vec![None; slot.hash8];
Expand Down Expand Up @@ -530,19 +530,19 @@ impl Func {
let commitment_used = hints.commitment.len() - commitment_init;
let bit_decomp_used = hints.bit_decomp.len() - bit_decomp_init;

for _ in hash4_used..self.slot.hash4 {
for _ in hash4_used..self.slots_count.hash4 {
hints.hash4.push(None);
}
for _ in hash6_used..self.slot.hash6 {
for _ in hash6_used..self.slots_count.hash6 {
hints.hash6.push(None);
}
for _ in hash8_used..self.slot.hash8 {
for _ in hash8_used..self.slots_count.hash8 {
hints.hash8.push(None);
}
for _ in commitment_used..self.slot.commitment {
for _ in commitment_used..self.slots_count.commitment {
hints.commitment.push(None);
}
for _ in bit_decomp_used..self.slot.bit_decomp {
for _ in bit_decomp_used..self.slots_count.bit_decomp {
hints.bit_decomp.push(None);
}

Expand Down
6 changes: 3 additions & 3 deletions src/lem/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ pub struct Func {
pub input_params: Vec<Var>,
pub output_size: usize,
pub body: Block,
pub slot: SlotsCounter,
pub slots_count: SlotsCounter,
}

/// LEM variables
Expand Down Expand Up @@ -315,9 +315,9 @@ impl Func {
output_size: usize,
body: Block,
) -> Result<Func> {
let slot = body.count_slots();
let slots_count = body.count_slots();
let func = Func {
slot,
slots_count,
name,
input_params,
output_size,
Expand Down
6 changes: 3 additions & 3 deletions src/lem/multiframe.rs
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@
let (Some(alloc_ptr_tag), Some(alloc_ptr_hash)) =
(aptr.tag().get_value(), aptr.hash().get_value())
else {
return Err(SynthesisError::AssignmentMissing);

Check warning on line 134 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L134

Added line #L134 was not covered by tests
};
assert_eq!(alloc_ptr_tag, z_ptr.tag().to_field());
assert_eq!(&alloc_ptr_hash, z_ptr.value());
Expand Down Expand Up @@ -160,7 +160,7 @@
.into_iter()
.for_each(|(sd_vec, st)| sd_vec.iter().for_each(|sd| slots_data.push((sd, st))));
});
// cache the slots witnesses wit `Arc` for speedy clones
// cache dummy slots witnesses with `Arc` for speedy clones
let dummy_witnesses_cache: FrozenMap<_, Box<Arc<SlotWitness<F>>>> = FrozenMap::default();
let gen_slot_witness = |(slot_idx, (slot_data, slot_type))| {
let mk_witness = || {
Expand Down Expand Up @@ -188,11 +188,11 @@
}
};
if parallel {
slots_data
.into_par_iter()
.enumerate()
.map(gen_slot_witness)
.collect()

Check warning on line 195 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L191-L195

Added lines #L191 - L195 were not covered by tests
} else {
slots_data
.into_iter()
Expand Down Expand Up @@ -243,84 +243,84 @@
/// Synthesize each frame in parallel, ideally one in each CPU. Each
/// frame will produce its corresponding partial witness, which are then
/// used to extend the final witness.
fn synthesize_frames_parallel<F: LurkField, CS: ConstraintSystem<F>, C: Coprocessor<F>>(
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
input: Vec<AllocatedPtr<F>>,
frames: &[Frame<F>],
func: &Func,
lang: &Lang<F, C>,
slots_witnesses: &[Arc<SlotWitness<F>>],
num_slots_per_frame: usize,
) -> Vec<AllocatedPtr<F>> {
assert!(cs.is_witness_generator());
assert_eq!(frames.len() * num_slots_per_frame, slots_witnesses.len());

Check warning on line 258 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L246-L258

Added lines #L246 - L258 were not covered by tests

let mut css = frames
.par_iter()
.enumerate()
.map(|(i, frame)| {
let mut frame_cs = WitnessCS::new();

Check warning on line 264 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L260-L264

Added lines #L260 - L264 were not covered by tests
// The first frame will take as input the actual input of the circuit.
// Subsequent frames would have to take the output of the previous one as input.
// But since we know the values of each frame input and we are generating the
// witnesses separately and in parallel, we will allocate new variables for each
// frame.
let allocated_input = if i == 0 {
input.clone()

Check warning on line 271 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L270-L271

Added lines #L270 - L271 were not covered by tests
} else {
frame
.input
.iter()
.map(|input_ptr| {
let z_ptr = store.hash_ptr(input_ptr).expect("hash_ptr failed");
AllocatedPtr::alloc(&mut frame_cs, || Ok(z_ptr)).expect("allocation failed")
})
.collect::<Vec<_>>()

Check warning on line 280 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L273-L280

Added lines #L273 - L280 were not covered by tests
};
let bound_allocations = &mut BoundAllocations::new();
func.bind_input(&allocated_input, bound_allocations);
let first_sw_idx = i * num_slots_per_frame;
let last_sw_idx = first_sw_idx + num_slots_per_frame;
let frame_slots_witnesses = &slots_witnesses[first_sw_idx..last_sw_idx];

let allocated_output = func
.synthesize_frame(
&mut frame_cs,
store,
frame,
g,
bound_allocations,
lang,
Some(frame_slots_witnesses),
)
.expect("failed to synthesize frame");
assert_eq!(allocated_input.len(), allocated_output.len());
assert_eq_ptrs_aptrs(store, frame.blank, &frame.output, &allocated_output)
.expect("assertion failed");
(frame_cs, allocated_output)
})
.collect::<Vec<_>>();

Check warning on line 304 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L282-L304

Added lines #L282 - L304 were not covered by tests

// At last, we need to concatenate all the partial witnesses into a single witness.
// Since we have allocated the input for each frame (apart from the first) instead
// of using the output of the previous frame, we will have to ignore the allocated
// inputs before concatenating the witnesses
for (i, (frame_cs, _)) in css.iter().enumerate() {
let start = if i == 0 { 0 } else { input.len() * 2 };
cs.extend_aux(&frame_cs.aux_slice()[start..]);

Check warning on line 312 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L310-L312

Added lines #L310 - L312 were not covered by tests
}

if let Some((_, last_output)) = css.pop() {

Check warning on line 315 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L315

Added line #L315 was not covered by tests
// the final output is the output of the last chunk
last_output

Check warning on line 317 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L317

Added line #L317 was not covered by tests
} else {
// there were no frames so we just return the input, preserving the
// same behavior as the sequential version
input

Check warning on line 321 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L321

Added line #L321 was not covered by tests
}
}

Check warning on line 323 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L323

Added line #L323 was not covered by tests

impl<'a, F: LurkField, C: Coprocessor<F> + 'a> MultiFrameTrait<'a, F, C> for MultiFrame<'a, F, C> {
type Ptr = Ptr<F>;
Expand Down Expand Up @@ -385,7 +385,7 @@
) -> Result<Self::AllocatedIO, SynthesisError> {
let func = self.get_func();
if cs.is_witness_generator() {
let num_slots_per_frame = func.slot.total();
let num_slots_per_frame = func.slots_count.total();
let slots_witnesses = generate_slots_witnesses(
store,
frames,
Expand All @@ -402,17 +402,17 @@
.synthesis
.is_parallel()
{
Ok(synthesize_frames_parallel(
cs,
g,
store,
input,
frames,
func,
self.get_lang(),
&slots_witnesses,
num_slots_per_frame,
))

Check warning on line 415 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L405-L415

Added lines #L405 - L415 were not covered by tests
} else {
synthesize_frames_sequential(
cs,
Expand Down Expand Up @@ -905,111 +905,111 @@

use super::*;

#[test]
fn test_sequential_and_parallel_witnesses_equivalences() {
let lurk_step = eval_step();
let num_slots_per_frame = lurk_step.slot.total();
let num_slots_per_frame = lurk_step.slots_count.total();
let store = Store::<Fq>::default();
let mut cs = WitnessCS::new();

let expr = store.read_with_default_state("(if t (+ 5 5) 6)").unwrap();

let (frames, _) = evaluate::<Fq, Coproc<Fq>>(None, expr, &store, 10).unwrap();

let sequential_slots_witnesses =
generate_slots_witnesses(&store, &frames, num_slots_per_frame, false);

let parallel_slots_witnesses =
generate_slots_witnesses(&store, &frames, num_slots_per_frame, true);

// asserting equality of slots witnesses
assert_eq!(
sequential_slots_witnesses.len(),
parallel_slots_witnesses.len()
);
for (ssw, psw) in sequential_slots_witnesses
.iter()
.zip(parallel_slots_witnesses)

Check warning on line 932 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L908-L932

Added lines #L908 - L932 were not covered by tests
{
assert_eq!(ssw.witness, psw.witness);
let (ssw_alloc_preimg, ssw_alloc_img) = &ssw.allocations;
let (psw_alloc_preimg, psw_alloc_img) = &psw.allocations;
assert_eq!(ssw_alloc_preimg.len(), psw_alloc_preimg.len());
for (ssw_alloc_preimg_num, psw_alloc_preimg_num) in
ssw_alloc_preimg.iter().zip(psw_alloc_preimg)

Check warning on line 939 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L934-L939

Added lines #L934 - L939 were not covered by tests
{
assert_eq!(
ssw_alloc_preimg_num.get_value(),
psw_alloc_preimg_num.get_value()
);
match (ssw_alloc_img, psw_alloc_img) {
(AllocatedVal::Pointer(x), AllocatedVal::Pointer(y)) => {
assert_eq!(x.tag().get_value(), y.tag().get_value());
assert_eq!(x.hash().get_value(), y.hash().get_value());

Check warning on line 948 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L941-L948

Added lines #L941 - L948 were not covered by tests
}
(AllocatedVal::Number(x), AllocatedVal::Number(y)) => {
assert_eq!(x.get_value(), y.get_value())

Check warning on line 951 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L950-L951

Added lines #L950 - L951 were not covered by tests
}
(AllocatedVal::Boolean(x), AllocatedVal::Boolean(y)) => {
assert_eq!(x.get_value(), y.get_value())

Check warning on line 954 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L953-L954

Added lines #L953 - L954 were not covered by tests
}
(AllocatedVal::Bits(x), AllocatedVal::Bits(y)) => {
assert_eq!(x.len(), y.len());
for (x, y) in x.iter().zip(y) {
assert_eq!(x.get_value(), y.get_value());

Check warning on line 959 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L956-L959

Added lines #L956 - L959 were not covered by tests
}
}
_ => panic!("allocated image mismatch"),

Check warning on line 962 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L962

Added line #L962 was not covered by tests
}
}
}
let g = lurk_step.alloc_globals(&mut cs, &store).unwrap();

// asserting equality of frames witnesses
let frame = frames.first().unwrap();
let mut input = Vec::with_capacity(frame.input.len());
for ptr in &frame.input {
let z_ptr = store.hash_ptr(ptr).unwrap();
let allocated_tag = AllocatedNum::alloc_infallible(&mut cs, || z_ptr.tag_field());
allocated_tag.inputize(&mut cs).unwrap();
let allocated_hash = AllocatedNum::alloc_infallible(&mut cs, || *z_ptr.value());
allocated_hash.inputize(&mut cs).unwrap();
input.push(AllocatedPtr::from_parts(allocated_tag, allocated_hash));
}

Check warning on line 978 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L966-L978

Added lines #L966 - L978 were not covered by tests

let mut cs_clone = cs.clone();

let lang = Lang::<Fq, Coproc<Fq>>::new();

let output_sequential = synthesize_frames_sequential(
&mut cs,
&g,
&store,
&input,
&frames,
lurk_step,
&lang,
Some((&sequential_slots_witnesses, num_slots_per_frame)),
)
.unwrap();

let output_parallel = synthesize_frames_parallel(
&mut cs_clone,
&g,
&store,
input,
&frames,
lurk_step,
&lang,
&sequential_slots_witnesses,
num_slots_per_frame,
);

assert_eq!(cs, cs_clone);
assert_eq!(output_sequential.len(), output_parallel.len());
for (x, y) in output_sequential.iter().zip(output_parallel) {
assert_eq!(x.tag().get_value(), y.tag().get_value());
assert_eq!(x.hash().get_value(), y.hash().get_value());

Check warning on line 1012 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L980-L1012

Added lines #L980 - L1012 were not covered by tests
}
}

Check warning on line 1014 in src/lem/multiframe.rs

View check run for this annotation

Codecov / codecov/patch

src/lem/multiframe.rs#L1014

Added line #L1014 was not covered by tests
}
2 changes: 1 addition & 1 deletion src/lem/slot.rs
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ impl Block {
Op::Hide(..) | Op::Open(..) => SlotsCounter::new((0, 0, 0, 1, 0)),
Op::Lt(..) => SlotsCounter::new((0, 0, 0, 0, 3)),
Op::Trunc(..) => SlotsCounter::new((0, 0, 0, 0, 1)),
Op::Call(_, func, _) => func.slot,
Op::Call(_, func, _) => func.slots_count,
_ => SlotsCounter::default(),
};
acc.add(val)
Expand Down
2 changes: 1 addition & 1 deletion src/lem/tests/misc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ fn synthesize_test_helper(func: &Func, inputs: Vec<Ptr<Fr>>, expected_num_slots:
let nil = store.intern_nil();
let outermost = Ptr::null(Tag::Cont(Outermost));

assert_eq!(func.slot, expected_num_slots);
assert_eq!(func.slots_count, expected_num_slots);

let computed_num_constraints = func.num_constraints::<Fr>(store);

Expand Down
Loading