Optimize oct insertion.

filecoin-project · May 28, 2020 · eab7af5 · eab7af5
1 parent a7e4c58
commit eab7af5
Show file tree

Hide file tree

Showing 8 changed files with 234 additions and 47 deletions.
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -26,7 +26,7 @@ jobs:
           no_output_timeout: 30m
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - run: rustup install $(cat rust-toolchain)
       - run: rustup default $(cat rust-toolchain)
       - run: rustup component add rustfmt-preview
@@ -40,7 +40,7 @@ jobs:
           paths:
             - Cargo.lock
       - save_cache:
-          key: cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+          key: cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
           paths:
             - /root/.cargo
             - /root/.rustup
@@ -56,7 +56,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - restore_parameter_cache
       - run:
           name: Test (stable)
@@ -85,7 +85,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - restore_parameter_cache
       - run:
           name: Test (stable) in release profile
@@ -111,7 +111,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - restore_parameter_cache
       - run:
           name: Test ignored in release profile
@@ -134,7 +134,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - restore_parameter_cache
       - run:
           name: Test (nightly)
@@ -153,7 +153,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - restore_parameter_cache
       - run:
           name: Benchmarks (nightly)
@@ -241,7 +241,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - run:
           name: Run cargo fmt
           command: cargo fmt --all -- --check
@@ -258,7 +258,7 @@ jobs:
           at: "."
       - restore_cache:
           keys:
-            - cargo-v26d-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
+            - cargo-v27b-{{ checksum "rust-toolchain" }}-{{ checksum "Cargo.toml" }}-{{ checksum "Cargo.lock" }}-{{ arch }}
       - run:
           name: Run cargo clippy
           command: cargo +$(cat rust-toolchain) clippy --all
@@ -319,7 +319,7 @@ commands:
   save_parameter_cache:
     steps:
       - save_cache:
-          key: proof-params-v26d-{{ checksum "filecoin-proofs/parameters.json" }}-{{ arch }}
+          key: proof-params-v27b-{{ checksum "filecoin-proofs/parameters.json" }}-{{ arch }}
           paths:
             - "~/paramcache.awesome"
             - "~/filecoin-proof-parameters/"
@@ -328,7 +328,7 @@ commands:
       - configure_environment_variables
       - restore_cache:
          keys:
-            - proof-params-v26d-{{ checksum "filecoin-proofs/parameters.json" }}-{{ arch }}
+            - proof-params-v27b-{{ checksum "filecoin-proofs/parameters.json" }}-{{ arch }}
   configure_environment_variables:
     steps:
       - run:

diff --git a/storage-proofs/core/src/gadgets/insertion.rs b/storage-proofs/core/src/gadgets/insertion.rs
@@ -3,7 +3,7 @@
 //! Insert an `AllocatedNum` into a sequence of `AllocatedNums` at an arbitrary position.
 //! This can be thought of as a generalization of `AllocatedNum::conditionally_reverse` and reduces to it in the binary case.
 
-use bellperson::gadgets::boolean::Boolean;
+use bellperson::gadgets::boolean::{AllocatedBit, Boolean};
 use bellperson::gadgets::num::AllocatedNum;
 use bellperson::{ConstraintSystem, SynthesisError};
 use ff::Field;
@@ -21,6 +21,22 @@ pub fn insert<E: Engine, CS: ConstraintSystem<E>>(
     let size = elements.len() + 1;
     assert_eq!(1 << bits.len(), size);
 
+    // For the sizes we know we need, we can take advantage of redundancy in the candidate selection at each position.
+    // This allows us to accomplish insertion with fewer constraints, if we hand-optimize.
+    // We don't need a special case for size 2 because the general algorithm
+    // collapses to `conditionally_reverse` when size = 2.
+    //
+    // If no special cases have been hand-coded, use the general algorithm.
+    // This costs size * (size - 1) constraints.
+    //
+    // Future work: In theory, we could compile arbitrary lookup tables to minimize constraints and avoid
+    // the most general case except when actually required — which it never is for simple insertion.
+    if size == 4 {
+        return insert_4(cs, element, bits, elements);
+    } else if size == 8 {
+        return insert_8(cs, element, bits, elements);
+    };
+
     // Running example choices, represent inserting x into [1, 2, 3].
 
     // An indexed sequence of correct results, one of which (the indexed one) will be selected.
@@ -69,6 +85,170 @@ pub fn insert<E: Engine, CS: ConstraintSystem<E>>(
     Ok(result)
 }
 
+pub fn insert_4<E: Engine, CS: ConstraintSystem<E>>(
+    cs: &mut CS,
+    element: &AllocatedNum<E>,
+    bits: &[Boolean],
+    elements: &[AllocatedNum<E>],
+) -> Result<Vec<AllocatedNum<E>>, SynthesisError> {
+    assert_eq!(elements.len() + 1, 4);
+    assert_eq!(bits.len(), 2);
+
+    /*
+    To insert A into [b, c, d] at position n of bits, represented by booleans [b0, b1, b2].
+    n [b0, b1] pos 0 1 2 3
+    0 [0, 0]       A b c d
+    1 [1, 0]       b A c d
+    2 [0, 1]       b c A d
+    3 [1, 1]       b c d A
+
+    A = element
+    b = elements[0]
+    c = elements[1]
+    d = elements[2]
+     */
+    let (b0, b1) = (&bits[0], &bits[1]);
+    let (a, b, c, d) = (&element, &elements[0], &elements[1], &elements[2]);
+
+    /// Define witness macro to allow legible definition of positional constraints.
+    /// See example expansions in comment to first usages below.
+    macro_rules! witness {
+        ( $var:ident <== if $cond:ident { $a:expr } else { $b:expr }) => {
+            let $var = pick(cs.namespace(|| stringify!($var)), $cond, $a, $b)?;
+        };
+    }
+
+    // Witness naming convention:
+    // `p0_x0` means "Output position 0 when b0 is unknown (x) and b1 is 0."
+
+    // Declaration:
+    witness!(p0_x0 <== if b0 { b } else { a });
+    witness!(p0 <== if b1 { b } else { &p0_x0 });
+    // Expansion:
+    // let p0_x0 = pick(cs.namespace(|| "p0_x0"), b0, b, a)?;
+    // let p0 = pick(cs.namespace(|| "p0"), b1, b, &p0_x0)?;
+
+    witness!(p1_x0 <== if b0 { a } else { b });
+    witness!(p1 <== if b1 { c } else { &p1_x0 });
+
+    witness!(p2_x1 <== if b0 { d } else { a });
+    witness!(p2 <== if b1 { &p2_x1 } else {c });
+
+    witness!(p3_x1 <== if b0 { a } else { d });
+    witness!(p3 <== if b1 { &p3_x1 } else { d });
+
+    Ok(vec![p0, p1, p2, p3])
+}
+
+pub fn insert_8<E: Engine, CS: ConstraintSystem<E>>(
+    cs: &mut CS,
+    element: &AllocatedNum<E>,
+    bits: &[Boolean],
+    elements: &[AllocatedNum<E>],
+) -> Result<Vec<AllocatedNum<E>>, SynthesisError> {
+    assert_eq!(elements.len() + 1, 8);
+    assert_eq!(bits.len(), 3);
+    /*
+    To insert A into [b, c, d, e, f, g, h] at position n of bits, represented by booleans [b0, b1, b2].
+    n [b0, b1, b2] pos 0 1 2 3 4 5 6 7
+    0 [0, 0, 0]        A b c d e f g h
+    1 [1, 0, 0]        b A c d e f g h
+    2 [0, 1, 0]        b c A d e f g h
+    3 [1, 1, 0]        b c d A e f g h
+    4 [0, 0, 1]        b c d e A f g h
+    5 [1, 0, 1]        b c d e f A g h
+    6 [0, 1, 1]        b c d e f g A h
+    7 [1, 1, 1]        b c d e f g h A
+
+
+    A = element
+    b = elements[0]
+    c = elements[1]
+    d = elements[2]
+    e = elements[3]
+    f = elements[4]
+    g = elements[5]
+    h = elements[6]
+     */
+
+    let (b0, b1, b2) = (&bits[0], &bits[1], &bits[2]);
+    let (a, b, c, d, e, f, g, h) = (
+        &element,
+        &elements[0],
+        &elements[1],
+        &elements[2],
+        &elements[3],
+        &elements[4],
+        &elements[5],
+        &elements[6],
+    );
+
+    // true if booleans b0 and b1 are both false: `(not b0) and (not b1)`
+    // (1 - b0) * (1 - b1) = 1
+    let b0_nor_b1 = match (b0, b1) {
+        (Boolean::Is(ref b0), Boolean::Is(ref b1)) => {
+            Boolean::Is(AllocatedBit::nor(cs.namespace(|| "b0 nor b1"), b0, b1)?)
+        }
+        _ => panic!("bits must be allocated and unnegated"),
+    };
+
+    // true if booleans b0 and b1 are both true: `b0 and b1`
+    // b0 * b1 = 1
+    let b0_and_b1 = match (&bits[0], &bits[1]) {
+        (Boolean::Is(ref b0), Boolean::Is(ref b1)) => {
+            Boolean::Is(AllocatedBit::and(cs.namespace(|| "b0 and b1"), b0, b1)?)
+        }
+        _ => panic!("bits must be allocated and unnegated"),
+    };
+
+    /// Define witness macro to allow legible definition of positional constraints.
+    /// See example expansions in comment to first usages below.
+    macro_rules! witness {
+        ( $var:ident <== if $cond:ident { $a:expr } else { $b:expr }) => {
+            let $var = pick(cs.namespace(|| stringify!($var)), $cond, $a, $b)?;
+        };
+
+        // Match condition terms which are explict syntactic references.
+        ( $var:ident <== if &$cond:ident { $a:expr } else { $b:expr }) => {
+            let $var = pick(cs.namespace(|| stringify!($var)), &$cond, $a, $b)?;
+        };
+    }
+
+    // Declaration:
+    witness!(p0_xx0 <== if &b0_nor_b1 { a } else { b });
+    witness!(p0 <== if b2 { b } else { &p0_xx0 });
+    // Expansion:
+    // let p0_xx0 = pick(cs.namespace(|| "p0_xx0"), &b0_nor_b1, a, b)?;
+    // let p0 = pick(cs.namespace(|| "p0"), b2, b, &p0_xx0)?;
+
+    witness!(p1_x00 <== if b0 { a } else { b });
+    witness!(p1_xx0 <== if b1 { c } else { &p1_x00 });
+    witness!(p1 <== if b2 { c } else { &p1_xx0 });
+
+    witness!(p2_x10 <== if b0 { d } else { a });
+    witness!(p2_xx0 <== if b1 { &p2_x10 } else { c });
+    witness!(p2 <== if b2 { d } else { &p2_xx0 });
+
+    witness!(p3_xx0 <== if &b0_and_b1 { a } else { d });
+    witness!(p3 <== if b2 { e } else { &p3_xx0 });
+
+    witness!(p4_xx1 <== if &b0_nor_b1 { a } else { f });
+    witness!(p4 <== if b2 { &p4_xx1 } else { e });
+
+    witness!(p5_x01 <== if b0 { a } else { f });
+    witness!(p5_xx1 <== if b1 { g } else { &p5_x01 });
+    witness!(p5 <== if b2 { &p5_xx1 } else { f });
+
+    witness!(p6_x11 <== if b0 { h } else { a });
+    witness!(p6_xx1 <== if b1 { &p6_x11 } else { g });
+    witness!(p6 <== if b2 { &p6_xx1 } else { g });
+
+    witness!(p7_xx1 <== if &b0_and_b1 { a } else { h });
+    witness!(p7 <== if b2 { &p7_xx1 } else { h });
+
+    Ok(vec![p0, p1, p2, p3, p4, p5, p6, p7])
+}
+
 /// Select the nth element of `from`, where `path_bits` represents n, least-significant bit first.
 /// The returned result contains the selected element, and constraints are enforced.
 /// `from.len()` must be a power of two.
@@ -125,6 +305,8 @@ where
         }
     })?;
 
+    // Constrain (b - a) * condition = (b - c), ensuring c = a iff
+    // condition is true, otherwise c = b.
     cs.enforce(
         || "pick",
         |lc| lc + b.get_variable() - a.get_variable(),
@@ -221,7 +403,8 @@ mod tests {
 
                 let to_insert =
                     AllocatedNum::<Bls12>::alloc(&mut cs.namespace(|| "insert"), || {
-                        Ok(<Fr as Field>::random(rng))
+                        let elt_to_insert = <Fr as Field>::random(rng);
+                        Ok(elt_to_insert)
                     })
                     .unwrap();
 
@@ -256,12 +439,15 @@ mod tests {
                 for i in 0..size - 1 {
                     let a = elements[i].get_value();
                     let b = inserted[i].get_value();
-
                     assert_eq!(a, b)
                 }
 
                 // One selection for each element of the result.
-                let expected_constraints = size * (size - 1);
+                let expected_constraints = match size {
+                    8 => 22, // unoptimized, would be 56
+                    4 => 8,  // unoptimized, would be 12
+                    _ => size * (size - 1),
+                };
 
                 let actual_constraints = cs.num_constraints() - test_constraints;
                 assert_eq!(expected_constraints, actual_constraints);