Skip to content

Commit

Permalink
optimize step function and add synthesis tests for LEM coprocessors
Browse files Browse the repository at this point in the history
  • Loading branch information
arthurpaulino committed Sep 20, 2023
1 parent c0a1790 commit f3246db
Show file tree
Hide file tree
Showing 8 changed files with 37 additions and 28 deletions.
5 changes: 4 additions & 1 deletion src/coprocessor/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,10 @@ pub(crate) mod test {
let a = &args[0];
let b = &args[1];

// FIXME: Check tags.
// We don't need to enforce variants on the input because they're
// already constrained from outside. In fact, we're not allowed to
// do so because we might be on a virtual path, with dummy values at
// hand. Thus we don't check/enforce the tags for the input.

// a^2 + b = c
let a2 = mul(&mut cs.namespace(|| "square"), a.hash(), a.hash())?;
Expand Down
2 changes: 0 additions & 2 deletions src/eval/reduction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,6 @@ fn reduce_with_witness_inner<F: LurkField, C: Coprocessor<F>>(
Control::ApplyContinuation(expr, env, cont)
}

ExprTag::Cproc => unreachable!(),

ExprTag::Thunk => match store
.fetch(&expr)
.ok_or_else(|| store::Error("Fetch failed".into()))?
Expand Down
4 changes: 2 additions & 2 deletions src/lem/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,14 +77,14 @@ impl<F: LurkField> GlobalAllocator<F> {
}

#[inline]
fn get_allocated_const(&self, f: F) -> Result<&AllocatedNum<F>> {
pub fn get_allocated_const(&self, f: F) -> Result<&AllocatedNum<F>> {
self.0
.get(&FWrap(f))
.ok_or_else(|| anyhow!("Global allocation not found for {}", f.hex_digits()))
}

#[inline]
fn get_allocated_const_cloned(&self, f: F) -> Result<AllocatedNum<F>> {
pub fn get_allocated_const_cloned(&self, f: F) -> Result<AllocatedNum<F>> {
self.get_allocated_const(f).cloned()
}
}
Expand Down
47 changes: 30 additions & 17 deletions src/lem/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ pub fn eval_step() -> &'static Func {

pub fn make_eval_step(cprocs: &[(&Symbol, usize)]) -> Func {
let reduce = reduce(cprocs);
let apply_cont = apply_cont();
let apply_cont = apply_cont(cprocs);
let make_thunk = make_thunk();

func!(step(expr, env, cont): 3 => {
Expand Down Expand Up @@ -471,7 +471,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
return (nil)
});
let is_cproc = is_cproc(cprocs);
let call_cproc = call_cproc(cprocs);

func!(reduce(expr, env, cont): 4 => {
// Useful constants
Expand Down Expand Up @@ -738,16 +737,11 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
}
return (expr, env, err, errctrl)
}
Expr::Cproc => {
let (cproc_name, evaluated_args) = decons2(expr);
let (expr, env, cont) = call_cproc(cproc_name, evaluated_args, env, cont);
return (expr, env, cont, apply);
}
}
})
}

fn apply_cont() -> Func {
fn apply_cont(cprocs: &[(&Symbol, usize)]) -> Func {
let car_cdr = car_cdr();
let make_tail_continuation = func!(make_tail_continuation(env, continuation): 1 => {
let foo: Expr::Nil;
Expand Down Expand Up @@ -817,6 +811,7 @@ fn apply_cont() -> Func {
};
return (nil)
});
let call_cproc = call_cproc(cprocs);
func!(apply_cont(result, env, cont, ctrl): 4 => {
// Useful constants
let ret = Symbol("return");
Expand Down Expand Up @@ -1301,9 +1296,9 @@ fn apply_cont() -> Func {
let evaluated_args: Expr::Cons = cons2(result, evaluated_args);
match unevaled_args.tag {
Expr::Nil => {
// nothing else to evaluate. prepare the call to `Ctrl::Cproc`
let expr: Expr::Cproc = cons2(cproc_name, evaluated_args);
return (expr, env, cont, ret);
// nothing else to evaluate
let (expr, env, cont) = call_cproc(cproc_name, evaluated_args, env, cont);
return (expr, env, cont, makethunk);
}
Expr::Cons => {
// pop the next argument that needs to be evaluated
Expand Down Expand Up @@ -1363,8 +1358,8 @@ mod tests {
use blstrs::Scalar as Fr;

const NUM_INPUTS: usize = 1;
const NUM_AUX: usize = 10561;
const NUM_CONSTRAINTS: usize = 12948;
const NUM_AUX: usize = 10559;
const NUM_CONSTRAINTS: usize = 12932;
const NUM_SLOTS: SlotsCounter = SlotsCounter {
hash4: 14,
hash6: 3,
Expand Down Expand Up @@ -1550,16 +1545,34 @@ mod tests {

let state = State::init_lurk_state().rccell();

let mut all_frames = Vec::default();
for e in [expr, expr2, expr3] {
let ptr = store.read(state.clone(), e).unwrap();
let (io, ..) = evaluate_simple(Some((&func, &lang)), ptr, store, 100).unwrap();
assert_eq!(io[0], res);
let (frames, _) = evaluate(Some((&func, &lang)), ptr, store, 100).unwrap();
assert_eq!(frames.last().unwrap().output[0], res);
all_frames.extend(frames);
}

for e in [expr4, expr5] {
let ptr = store.read(state.clone(), e).unwrap();
let (io, ..) = evaluate_simple(Some((&func, &lang)), ptr, store, 100).unwrap();
assert_eq!(io[2], error);
let (frames, _) = evaluate(Some((&func, &lang)), ptr, store, 100).unwrap();
assert_eq!(frames.last().unwrap().output[2], error);
all_frames.extend(frames);
}

store.hydrate_z_cache();

let mut cs_prev = None;
for frame in all_frames.iter() {
let mut cs = TestConstraintSystem::<Fr>::new();
func.synthesize_frame_aux(&mut cs, store, frame, &lang)
.unwrap();
assert!(cs.is_satisfied());
if let Some(cs_prev) = cs_prev {
// Check for all input expresssions that all frames are uniform.
assert_eq!(cs.delta(&cs_prev, true), Delta::Equal);
}
cs_prev = Some(cs);
}
}
}
1 change: 0 additions & 1 deletion src/lem/store.rs
Original file line number Diff line number Diff line change
Expand Up @@ -763,7 +763,6 @@ impl<F: LurkField> Ptr<F> {
}
None => "<Malformed Comm>".into(),
},
Cproc => "<COPROCESSOR (TODO)>".into(),
},
Tag::Cont(_) => "<CONTINUATION (TODO)>".into(),
_ => unreachable!(),
Expand Down
1 change: 0 additions & 1 deletion src/store.rs
Original file line number Diff line number Diff line change
Expand Up @@ -773,7 +773,6 @@ impl<F: LurkField> Store<F> {
.map(|(car, cdr)| Expression::Str(car, cdr)),
ExprTag::Char => self.fetch_char(ptr).map(Expression::Char),
ExprTag::U64 => self.fetch_uint(ptr).map(Expression::UInt),
ExprTag::Cproc => unreachable!(),
}
}

Expand Down
4 changes: 1 addition & 3 deletions src/tag.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ pub enum ExprTag {
Comm,
U64,
Key,
Cproc,
}

impl From<ExprTag> for u16 {
Expand Down Expand Up @@ -66,7 +65,6 @@ impl fmt::Display for ExprTag {
ExprTag::Char => write!(f, "char#"),
ExprTag::Comm => write!(f, "comm#"),
ExprTag::U64 => write!(f, "u64#"),
ExprTag::Cproc => write!(f, "cproc#"),
}
}
}
Expand All @@ -77,7 +75,7 @@ impl TypePredicates for ExprTag {
}
fn is_self_evaluating(&self) -> bool {
match self {
Self::Cons | Self::Thunk | Self::Sym | Self::Cproc => false,
Self::Cons | Self::Thunk | Self::Sym => false,
Self::Nil
| Self::Fun
| Self::Num
Expand Down
1 change: 0 additions & 1 deletion src/z_data/z_expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,6 @@ impl<F: LurkField> ZExpr<F> {
store.hash_cont(&thunk.continuation)?,
))
}),
ExprTag::Cproc => unreachable!(),
}
}
}
Expand Down

0 comments on commit f3246db

Please sign in to comment.