pf2bv

src/ir/term/mod.rs

@@ -32,6 +32,8 @@ pub enum Op {
     // number of extra bits
     BvUext(usize),
     BvSext(usize),
+    // number of bits the element should fit in.
+    PfToBv(usize),
 
     Implies,
     BoolNaryOp(BoolNaryOp),
@@ -76,6 +78,7 @@ impl Op {
             Op::BvConcat => None,
             Op::BvUext(_) => Some(1),
             Op::BvSext(_) => Some(1),
+            Op::PfToBv(_) => Some(1),
             Op::Implies => Some(2),
             Op::BoolNaryOp(_) => None,
             Op::Not => Some(1),
@@ -114,6 +117,7 @@ impl Display for Op {
             Op::BvConcat => write!(f, "concat"),
             Op::BvUext(a) => write!(f, "uext {}", a),
             Op::BvSext(a) => write!(f, "sext {}", a),
+            Op::PfToBv(a) => write!(f, "pf2bv {}", a),
             Op::Implies => write!(f, "=>"),
             Op::BoolNaryOp(a) => write!(f, "{}", a),
             Op::Not => write!(f, "not"),
@@ -695,6 +699,7 @@ pub fn check_raw(t: &Term) -> Result<Sort, TypeError> {
                         })
                         .map(Sort::BitVector),
                     (Op::BvSext(a), &[Sort::BitVector(b)]) => Ok(Sort::BitVector(a + b)),
+                    (Op::PfToBv(a), &[Sort::Field(_)]) => Ok(Sort::BitVector(*a)),
                     (Op::BvUext(a), &[Sort::BitVector(b)]) => Ok(Sort::BitVector(a + b)),
                     (Op::Implies, &[a, b]) => {
                         let ctx = "bool binary op";
@@ -853,6 +858,11 @@ pub fn eval(t: &Term, h: &HashMap<String, Value>) -> Value {
                     * Integer::from(a.uint().get_bit(a.width() as u32 - 1));
                 BitVector::new(a.uint() | (mask << a.width() as u32), a.width() + w)
             }),
+            Op::PfToBv(w) => Value::BitVector({
+                let a = vs.get(&c.cs[0]).unwrap().as_pf().clone();
+                assert!(a.i() < &(Integer::from(1) << 1));
+                BitVector::new(a.i().clone(), *w)
+            }),
             Op::BvUext(w) => Value::BitVector({
                 let a = vs.get(&c.cs[0]).unwrap().as_bv().clone();
                 BitVector::new(a.uint().clone(), a.width() + w)

src/ir/to_r1cs.rs

@@ -459,6 +459,11 @@ impl ToR1cs {
 
                         self.set_bv_bits(bv, bits.rev().chain(ext_bits).collect());
                     }
+                    Op::PfToBv(nbits) => {
+                        let lc = self.get_pf(&bv.cs[0]).clone();
+                        let bits = self.bitify("pf2bv", &lc, *nbits, false);
+                        self.set_bv_bits(bv.clone(), bits);
+                    }
                     Op::BoolToBv => {
                         let b = self.get_bool(&bv.cs[0]).clone();
                         self.set_bv_bits(bv, vec![b]);
@@ -746,6 +751,7 @@ mod test {
     use rand::distributions::Distribution;
     use rand::SeedableRng;
     use crate::target::r1cs::opt::reduce_linearities;
+    use std::sync::Arc;
 
     #[test]
     fn bool() {
@@ -908,6 +914,13 @@ mod test {
         ))))
     }
 
+    fn pf(i: isize) -> Term {
+        leaf_term(Op::Const(Value::Field(FieldElem::new(
+            Integer::from(i),
+            Arc::new(Integer::from(crate::ir::term::field::TEST_FIELD)),
+        ))))
+    }
+
     fn const_test(term: Term) {
         let cs = Constraints {
             public_inputs: HashSet::new(),
@@ -995,4 +1008,23 @@ mod test {
             bv(0b0001, 4)
         ]);
     }
+
+    #[test]
+    fn pf2bv() {
+        const_test(term![
+            Op::Eq;
+            term![Op::PfToBv(4); pf(8)],
+            bv(0b1000, 4)
+        ]);
+        const_test(term![
+            Op::Eq;
+            term![Op::PfToBv(4); pf(15)],
+            bv(0b1111, 4)
+        ]);
+        const_test(term![
+            Op::Eq;
+            term![Op::PfToBv(8); pf(15)],
+            bv(0b1111, 8)
+        ]);
+    }
 }