Skip to content

Commit

Permalink
Adjust sha256 example (argumentcomputer#490)
Browse files Browse the repository at this point in the history 
* change sha256 benchmark

* constraint second limb

* add `as_lurk_boolean` and use it in coprocessor and circuit

* move as_lurk_boolean to the right place

* fix preimage hack

* delete extraneous `get_constants()`

* change boolean name

* remove extra parens from evaluated expression

* fix rebase conflicts

* constrain preimage?

* use `alloc_conditionally`

* attempt to return terminal cont ptr

* add logging

* constrain preimage and revert cont ptr "fix"

* more descriptive allocatedptr name

* delete extraneous let binding
  • Loading branch information
@mpenciak
mpenciak authored Jul 20, 2023
1 parent 4a92ae0 commit adb7290
Show file tree
Hide file tree
Showing 7 changed files with 81 additions and 47 deletions.
99 changes: 60 additions & 39 deletions examples/sha256.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ use std::marker::PhantomData;
use std::sync::Arc;
use std::time::Instant;

use lurk::circuit::gadgets::data::GlobalAllocations;
use lurk::circuit::gadgets::constraints::alloc_equal;
use lurk::circuit::gadgets::data::{allocate_constant, GlobalAllocations};
use lurk::circuit::gadgets::pointer::{AllocatedContPtr, AllocatedPtr};
use lurk::coprocessor::{CoCircuit, Coprocessor};
use lurk::eval::{empty_sym_env, lang::Lang};
Expand All @@ -12,8 +13,7 @@ use lurk::proof::{nova::NovaProver, Prover};
use lurk::ptr::Ptr;
use lurk::public_parameters::public_params;
use lurk::store::Store;
use lurk::tag::{ExprTag, Tag};
use lurk::{sym, Num};
use lurk::sym;
use lurk_macros::Coproc;

use bellperson::gadgets::boolean::{AllocatedBit, Boolean};
Expand All @@ -22,7 +22,6 @@ use bellperson::gadgets::num::AllocatedNum;
use bellperson::gadgets::sha256::sha256;
use bellperson::{ConstraintSystem, SynthesisError};

use itertools::enumerate;
use pasta_curves::pallas::Scalar as Fr;
use serde::{Deserialize, Serialize};
use sha2::{Digest, Sha256};
Expand All @@ -32,6 +31,7 @@ const REDUCTION_COUNT: usize = 10;
#[derive(Clone, Debug, Serialize, Deserialize)]
pub(crate) struct Sha256Coprocessor<F: LurkField> {
n: usize,
expected: [u128; 2],
pub(crate) _p: PhantomData<F>,
}

Expand All @@ -43,14 +43,23 @@ impl<F: LurkField> CoCircuit<F> for Sha256Coprocessor<F> {
fn synthesize<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
g: &GlobalAllocations<F>,
_g: &GlobalAllocations<F>,
store: &Store<F>,
_input_exprs: &[AllocatedPtr<F>],
input_env: &AllocatedPtr<F>,
input_cont: &AllocatedContPtr<F>,
) -> Result<(AllocatedPtr<F>, AllocatedPtr<F>, AllocatedContPtr<F>), SynthesisError> {
// // TODO: Maybe fix this
let false_bool = Boolean::from(AllocatedBit::alloc(cs.namespace(|| "false"), Some(false))?);
let false_bool = Boolean::from(AllocatedBit::alloc(
cs.namespace(|| "false bit"),
Some(false),
)?);

cs.enforce(
|| "enforce zero preimage",
|lc| lc,
|lc| lc,
|_| false_bool.lc(CS::one(), F::ONE),
);

let preimage = vec![false_bool; self.n * 8];

Expand All @@ -68,14 +77,29 @@ impl<F: LurkField> CoCircuit<F> for Sha256Coprocessor<F> {
})
.collect();

let result_ptr = enumerate(nums).try_fold(g.nil_ptr.clone(), |acc, (i, num)| {
let ptr = AllocatedPtr::alloc_tag(
&mut cs.namespace(|| format!("limb_value_{i}")),
ExprTag::Num.to_field(),
num,
)?;
AllocatedPtr::construct_cons(cs.namespace(|| format!("limb_{i}")), g, store, &ptr, &acc)
})?;
let eqs: Vec<Boolean> = (0..2)
.map(|i| {
let num = allocate_constant(
&mut cs.namespace(|| format!("allocate result {i}")),
F::from_u128(self.expected[i]),
)
.unwrap();

let eq = alloc_equal(
cs.namespace(|| format!("equate numbers {i}")),
&num,
&nums[i],
)
.unwrap();

eq
})
.collect();

let both_eq = Boolean::and(cs.namespace(|| "both equal"), &eqs[0], &eqs[1])?;

let result_ptr =
AllocatedPtr::as_lurk_boolean(cs.namespace(|| "result ptr"), store, &both_eq)?;

Ok((result_ptr, input_env.clone(), input_cont.clone()))
}
Expand All @@ -94,33 +118,28 @@ impl<F: LurkField> Coprocessor<F> for Sha256Coprocessor<F> {
hasher.update(input);
let result = hasher.finalize();

let u: Vec<u128> = (0..2)
let mut u: Vec<u128> = (0..2)
.map(|i| {
let a: [u8; 16] = result[(16 * i)..(16 * (i + 1))].try_into().unwrap();
u128::from_be_bytes(a)
})
.collect();

let blah = &[u[0], u[1]].map(|x| s.intern_num(u128_into_scalar::<F>(x)));
s.list(blah)
u.reverse();

s.as_lurk_boolean(u == self.expected)
}

fn has_circuit(&self) -> bool {
true
}
}

fn u128_into_scalar<F: LurkField>(u: u128) -> Num<F> {
let bytes: [u8; 16] = u.to_le_bytes();
let zeroes: [u8; 16] = [0u8; 16];
let result: [u8; 32] = [bytes, zeroes].concat().try_into().unwrap();
Num::Scalar(F::from_bytes(&result).unwrap())
}

impl<F: LurkField> Sha256Coprocessor<F> {
pub(crate) fn new(n: usize) -> Self {
pub(crate) fn new(n: usize, expected: [u128; 2]) -> Self {
Self {
n,
expected,
_p: Default::default(),
}
}
Expand All @@ -134,6 +153,7 @@ enum Sha256Coproc<F: LurkField> {
/// Run the example in this file with
/// `cargo run --release --example sha256 1 f5a5fd42d16a20302798ef6ed309979b43003d2320d9f0e8ea9831a92759fb4b false`
fn main() {
pretty_env_logger::init();
let args: Vec<String> = env::args().collect();

let num_of_64_bytes = args[1].parse::<usize>().unwrap();
Expand All @@ -142,25 +162,26 @@ fn main() {

let input_size = 64 * num_of_64_bytes;

let store = &mut Store::<Fr>::new();
let sym = sym!("sha256", format!("{}-zero-bytes", input_size));
let mut u: [u128; 2] = [0u128; 2];
for i in 0..2 {
u[i] = u128::from_be_bytes(expect[(i * 16)..(i + 1) * 16].try_into().unwrap())
}

u.reverse();

let coproc_expr = format!("({})", &sym);
let store = &mut Store::<Fr>::new();
let sym_str = sym!("sha256", format!("{}-zero-bytes", input_size));

let lang = Lang::<Fr, Sha256Coproc<Fr>>::new_with_bindings(
store,
vec![(sym, Sha256Coprocessor::new(input_size).into())],
vec![(
sym_str.clone(),
Sha256Coprocessor::new(input_size, u).into(),
)],
);

let mut u: [u128; 2] = [0u128; 2];

for i in 0..2 {
u[i] = u128::from_be_bytes(expect[(i * 16)..(i + 1) * 16].try_into().unwrap())
}
let result_expr = format!("({} {})", u[0], u[1]);

let expr = format!("(emit (eq {coproc_expr} (quote {result_expr})))");
let ptr = store.read(&expr).unwrap();
let coproc_expr = format!("({})", sym_str);
let ptr = store.read(&coproc_expr).unwrap();

let nova_prover = NovaProver::<Fr, Sha256Coproc<Fr>>::new(REDUCTION_COUNT, lang.clone());
let lang_rc = Arc::new(lang);
Expand Down
6 changes: 2 additions & 4 deletions src/circuit/circuit_frame.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2913,7 +2913,6 @@ fn apply_continuation<F: LurkField, CS: ConstraintSystem<F>>(
),
SynthesisError,
> {
let c = store.get_constants();
let mut hash_default_results = HashInputResults::default();
let mut results = Results::default();

Expand Down Expand Up @@ -3754,11 +3753,10 @@ fn apply_continuation<F: LurkField, CS: ConstraintSystem<F>>(

let args_equal = arg1_final.alloc_equal(&mut cs.namespace(|| "args_equal"), &arg2_final)?;

let args_equal_ptr = AllocatedPtr::pick_const(
let args_equal_ptr = AllocatedPtr::as_lurk_boolean(
&mut cs.namespace(|| "args_equal_ptr"),
store,
&args_equal,
&c.t.z_ptr(),
&c.nil.z_ptr(),
)?;

let not_dummy = cont.alloc_tag_equal(
Expand Down
2 changes: 1 addition & 1 deletion src/circuit/gadgets/constraints.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -433,7 +433,7 @@ where
}

// This could now use alloc_is_zero to avoid duplication.
pub(crate) fn alloc_equal<CS: ConstraintSystem<F>, F: PrimeField>(
pub fn alloc_equal<CS: ConstraintSystem<F>, F: PrimeField>(
mut cs: CS,
a: &AllocatedNum<F>,
b: &AllocatedNum<F>,
Expand Down
2 changes: 1 addition & 1 deletion src/circuit/gadgets/data.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -384,7 +384,7 @@ impl<F: LurkField> Ptr<F> {
}
}

pub(crate) fn allocate_constant<F: LurkField, CS: ConstraintSystem<F>>(
pub fn allocate_constant<F: LurkField, CS: ConstraintSystem<F>>(
cs: &mut CS,
val: F,
) -> Result<AllocatedNum<F>, SynthesisError> {
Expand Down
2 changes: 1 addition & 1 deletion src/circuit/gadgets/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
pub(crate) mod macros;

pub(crate) mod case;
pub(crate) mod constraints;
pub mod constraints;
pub mod data;
pub(crate) mod hashes;
pub mod pointer;
15 changes: 15 additions & 0 deletions src/circuit/gadgets/pointer.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -496,6 +496,21 @@ impl<F: LurkField> AllocatedPtr<F> {
Ok(AllocatedPtr { tag, hash })
}

/// Takes a boolean and returns an allocated pointer corresponding to the Boolean's value.
pub fn as_lurk_boolean<CS: ConstraintSystem<F>>(
mut cs: CS,
store: &Store<F>,
boolean: &Boolean,
) -> Result<AllocatedPtr<F>, SynthesisError> {
let c = store.get_constants();
AllocatedPtr::pick_const(
cs.namespace(|| "allocated lurk bool"),
boolean,
&c.t.z_ptr(),
&c.nil.z_ptr(),
)
}

pub fn by_index(n: usize, ptr_vec: &[AllocatedNum<F>]) -> Self {
AllocatedPtr {
tag: ptr_vec[n * 2].clone(),
Expand Down
2 changes: 1 addition & 1 deletion src/eval/reduction.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1366,7 +1366,7 @@ fn extend_closure<F: LurkField>(
}

impl<F: LurkField> Store<F> {
fn as_lurk_boolean(&mut self, x: bool) -> Ptr<F> {
pub fn as_lurk_boolean(&mut self, x: bool) -> Ptr<F> {
if x {
self.t()
} else {
Expand Down

0 comments on commit adb7290

Please sign in to comment.