added func zkcons! to enable adding constraints instruction to the zkvm

This commit is contained in:
ada
2020-10-28 20:16:19 +01:00
parent 9a099f4e36
commit 6813ad46bc
3 changed files with 23 additions and 22 deletions

View File

@@ -252,6 +252,11 @@ fn conj(a: MalArgs) -> MalRet {
}
}
fn add(a: MalArgs) -> MalRet {
println!("{:?}", a);
Ok(Nil)
}
fn seq(a: MalArgs) -> MalRet {
match a[0] {
List(ref v, _) | Vector(ref v, _) if v.len() == 0 => Ok(Nil),
@@ -352,5 +357,6 @@ pub fn ns() -> Vec<(&'static str, MalVal)> {
("reset!", func(|a| a[0].reset_bang(&a[1]))),
("swap!", func(|a| a[0].swap_bang(&a[1..].to_vec()))),
("unpack-bits", func(unpack_bits)),
("add", func(add)),
]
}

View File

@@ -265,25 +265,21 @@ fn eval(mut ast: MalVal, mut env: Env) -> MalRet {
_ => Ok(Nil),
}
}
Sym(ref a0sym) if a0sym == "zk*" => {
Sym(ref a0sym) if a0sym == "zkcons!" => {
println!("{:?}", l);
let (a1, a2) = (l[1].clone(), l[2].clone());
let zk_circuit = ZKCircuit{
Ok(Nil)
}
Sym(ref a0sym) if a0sym == "defzk!" => {
let (a1, a2) = (l[1].clone(), l[2].clone());
let zk_circuit = MalVal::Zk(ZKCircuit{
name: a1.pr_str(true),
constraints: Vec::new(),
private: Vec::new(),
public: Vec::new()
};
env_set(&env, l[1].clone(), MalVal::Zk(zk_circuit));
// TODO add alloc name and nested eval to zkcircuit
Ok(MalFunc {
eval: eval,
ast: Rc::new(a2),
env: env,
params: Rc::new(a1),
is_macro: false,
meta: Rc::new(Nil),
})
});
env_set(&env, l[1].clone(), zk_circuit.clone());
Ok(zk_circuit)
}
Sym(ref a0sym) if a0sym == "fn*" => {
let (a1, a2) = (l[1].clone(), l[2].clone());

View File

@@ -1,18 +1,17 @@
(def! circuit (zk* [x] (
(def! bits (unpack-bits x 256))
(map (fn* [b] (println b
'(add lc0 one)
(def! x "73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000000")
(defzk! circuit ())
(def! bits (unpack-bits x 256))
;;zkcons add a constraints instruction to the circuit
(map (fn* [b] (zkcons!
(add 'lc0 'one)
'(sub b)
'(add lc1 x)
'enforce)
) bits)
(map (fn* [b] (println b '(add lc0 b)
(map (fn* [b] (quote '(add lc0 b)
'double-coeff-lc)
) bits)
(println 'reset-coeff-lc
'(sub lc0 x)
'(add lc1 one)
'enforce)
)))
(def! dec "73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000000")
(circuit dec)