challenge operator (#145)

Cargo.lock

@@ -278,6 +278,7 @@ dependencies = [
  "quickcheck",
  "quickcheck_macros",
  "rand 0.8.5",
+ "rand_chacha 0.3.1",
  "rsmt2",
  "rug",
  "serde",

Cargo.toml

@@ -14,6 +14,7 @@ rug = { version = "1.11", features = ["serde"] }
 gmp-mpfr-sys = { version = "1.4", optional = true }
 lazy_static = { version = "1.4", optional = true }
 rand = "0.8"
+rand_chacha = "0.3"
 rsmt2 = { version = "0.14", optional = true }
 ieee754 = { version = "0.2", optional = true}
 zokrates_parser = { path = "third_party/ZoKrates/zokrates_parser", optional = true }

src/ir/term/fmt.rs

@@ -185,6 +185,7 @@ impl DisplayIr for Op {
             Op::IntNaryOp(a) => write!(f, "{a}"),
             Op::IntBinPred(a) => write!(f, "{a}"),
             Op::UbvToPf(a) => write!(f, "(bv2pf {})", a.modulus()),
+            Op::PfChallenge(n, m) => write!(f, "(challenge {} {})", n, m.modulus()),
             Op::Select => write!(f, "select"),
             Op::Store => write!(f, "store"),
             Op::Tuple => write!(f, "tuple"),

src/ir/term/mod.rs

@@ -125,6 +125,13 @@ pub enum Op {
     ///
     /// Takes the modulus.
     UbvToPf(FieldT),
+    /// A random value, sampled uniformly and independently of its arguments.
+    ///
+    /// Takes a name (if deterministically sampled, challenges of different names are sampled
+    /// differentely) and a field to sample from.
+    ///
+    /// In IR evaluation, we sample deterministically based on a hash of the name.
+    PfChallenge(String, FieldT),
 
     /// Integer n-ary operator
     IntNaryOp(IntNaryOp),
@@ -272,6 +279,7 @@ impl Op {
             Op::FpToFp(_) => Some(1),
             Op::PfUnOp(_) => Some(1),
             Op::PfNaryOp(_) => None,
+            Op::PfChallenge(_, _) => None,
             Op::IntNaryOp(_) => None,
             Op::IntBinPred(_) => Some(2),
             Op::UbvToPf(_) => Some(1),
@@ -1367,6 +1375,21 @@ pub fn eval_op(op: &Op, args: &[&Value], var_vals: &FxHashMap<String, Value>) ->
             )
         }),
         Op::UbvToPf(fty) => Value::Field(fty.new_v(args[0].as_bv().uint())),
+        Op::PfChallenge(name, field) => {
+            use rand::SeedableRng;
+            use rand_chacha::ChaChaRng;
+            use std::hash::{Hash, Hasher};
+            // hash the string
+            let mut hasher = fxhash::FxHasher::default();
+            name.hash(&mut hasher);
+            let hash: u64 = hasher.finish();
+            // seed ChaCha with the hash
+            let mut seed = [0u8; 32];
+            seed[0..8].copy_from_slice(&hash.to_le_bytes());
+            let mut rng = ChaChaRng::from_seed(seed);
+            // sample from ChaCha
+            Value::Field(field.random_v(&mut rng))
+        }
         // tuple
         Op::Tuple => Value::Tuple(args.iter().map(|a| (*a).clone()).collect()),
         Op::Field(i) => {

src/ir/term/text/mod.rs

@@ -288,6 +288,10 @@ impl<'src> IrInterp<'src> {
                 [Leaf(Ident, b"ubv2fp"), a] => Ok(Op::UbvToFp(self.usize(a))),
                 [Leaf(Ident, b"sbv2fp"), a] => Ok(Op::SbvToFp(self.usize(a))),
                 [Leaf(Ident, b"fp2fp"), a] => Ok(Op::FpToFp(self.usize(a))),
+                [Leaf(Ident, b"challenge"), name, field] => Ok(Op::PfChallenge(
+                    self.ident_string(name),
+                    FieldT::from(self.int(field)),
+                )),
                 [Leaf(Ident, b"bv2pf"), a] => Ok(Op::UbvToPf(FieldT::from(self.int(a)))),
                 [Leaf(Ident, b"field"), a] => Ok(Op::Field(self.usize(a))),
                 [Leaf(Ident, b"update"), a] => Ok(Op::Update(self.usize(a))),
@@ -958,4 +962,12 @@ mod test {
         let c2 = parse_precompute(s.as_bytes());
         assert_eq!(c, c2);
     }
+
+    #[test]
+    fn challenge_roundtrip() {
+        let t = parse_term(b"(declare ((a bool) (b bool)) ((challenge hithere 17) a b))");
+        let s = serialize_term(&t);
+        let t2 = parse_term(s.as_bytes());
+        assert_eq!(t, t2);
+    }
 }

src/ir/term/ty.rs

@@ -59,6 +59,7 @@ fn check_dependencies(t: &Term) -> Vec<Term> {
         Op::IntNaryOp(_) => Vec::new(),
         Op::IntBinPred(_) => Vec::new(),
         Op::UbvToPf(_) => Vec::new(),
+        Op::PfChallenge(_, _) => Vec::new(),
         Op::Select => vec![t.cs()[0].clone()],
         Op::Store => vec![t.cs()[0].clone()],
         Op::Tuple => t.cs().to_vec(),
@@ -128,6 +129,7 @@ fn check_raw_step(t: &Term, tys: &TypeTable) -> Result<Sort, TypeErrorReason> {
         Op::IntNaryOp(_) => Ok(Sort::Int),
         Op::IntBinPred(_) => Ok(Sort::Bool),
         Op::UbvToPf(m) => Ok(Sort::Field(m.clone())),
+        Op::PfChallenge(_, m) => Ok(Sort::Field(m.clone())),
         Op::Select => array_or(get_ty(&t.cs()[0]), "select").map(|(_, v)| v.clone()),
         Op::Store => Ok(get_ty(&t.cs()[0]).clone()),
         Op::Tuple => Ok(Sort::Tuple(t.cs().iter().map(get_ty).cloned().collect())),
@@ -332,6 +334,7 @@ pub fn rec_check_raw_helper(oper: &Op, a: &[&Sort]) -> Result<Sort, TypeErrorRea
                 .map(|a| a.clone())
         }
         (Op::UbvToPf(m), &[a]) => bv_or(a, "ubv-to-pf").map(|_| Sort::Field(m.clone())),
+        (Op::PfChallenge(_, m), _) => Ok(Sort::Field(m.clone())),
         (Op::PfUnOp(_), &[a]) => pf_or(a, "pf unary op").map(|a| a.clone()),
         (Op::IntNaryOp(_), a) => {
             let ctx = "int nary op";