diff --git a/examples/sha256.rs b/examples/sha256.rs
index 41eff2fd91..849082eced 100644
--- a/examples/sha256.rs
+++ b/examples/sha256.rs
@@ -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};
@@ -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};
@@ -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};
@@ -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>,
 }
 
@@ -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];
 
@@ -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()))
     }
@@ -94,15 +118,16 @@ 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 {
@@ -110,17 +135,11 @@ impl<F: LurkField> Coprocessor<F> for Sha256Coprocessor<F> {
     }
 }
 
-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(),
         }
     }
@@ -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();
@@ -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);
diff --git a/src/circuit/circuit_frame.rs b/src/circuit/circuit_frame.rs
index 33837a224b..bee0985e9e 100644
--- a/src/circuit/circuit_frame.rs
+++ b/src/circuit/circuit_frame.rs
@@ -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();
 
@@ -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(
diff --git a/src/circuit/gadgets/constraints.rs b/src/circuit/gadgets/constraints.rs
index 0da5460ff8..d2f13774ac 100644
--- a/src/circuit/gadgets/constraints.rs
+++ b/src/circuit/gadgets/constraints.rs
@@ -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>,
diff --git a/src/circuit/gadgets/data.rs b/src/circuit/gadgets/data.rs
index 8fc9202f4e..d487f21580 100644
--- a/src/circuit/gadgets/data.rs
+++ b/src/circuit/gadgets/data.rs
@@ -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> {
diff --git a/src/circuit/gadgets/mod.rs b/src/circuit/gadgets/mod.rs
index 2a601a777e..3a547dace6 100644
--- a/src/circuit/gadgets/mod.rs
+++ b/src/circuit/gadgets/mod.rs
@@ -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;
diff --git a/src/circuit/gadgets/pointer.rs b/src/circuit/gadgets/pointer.rs
index 7beda33c8e..8b2db60e3b 100644
--- a/src/circuit/gadgets/pointer.rs
+++ b/src/circuit/gadgets/pointer.rs
@@ -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(),
diff --git a/src/eval/reduction.rs b/src/eval/reduction.rs
index 5a921806ef..03b102d465 100644
--- a/src/eval/reduction.rs
+++ b/src/eval/reduction.rs
@@ -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 {