add log2 circuit template

circuit/log2.circom

@@ -0,0 +1,38 @@
+pragma circom 2.0.0;
+
+// 
+// given an input `inp`, this template checks that inp == 2^out
+// with 0 < out <= n
+//
+// we also output a mask vector which is 1 for i=0..out-1, and 0 elsewhere
+//
+
+template Log2(n) {
+
+  signal input  inp;
+  signal output out;  
+  signal output mask[n+1];
+
+  // mask will be a vector [1,1,1,...1,0,...,0,0]
+  // which can change only where inp == 2^out
+
+  var log2 = -1;
+  for(var i=0; i<=n; i++) { 
+    mask[i] <-- ((2**i) < inp) ? 1 : 0;
+    if (2**i == inp) { log2 = i; }
+  }
+
+  out <-- log2;
+
+  mask[0] === 1;
+  mask[n] === 0;
+
+  var sum = 0;
+  for(var i=0; i<n; i++) { 
+    sum += (2**(i+1)) * (mask[i] - mask[i+1]);
+    0 === (mask[i] - mask[i+1]) * (i + 1 - out);
+  }
+
+  inp === sum;  
+
+}

test/.gitignore

@@ -0,0 +1 @@
+.ghc.environment*

test/Circuit/Log2.hs

@@ -0,0 +1,70 @@
+
+module Circuit.Log2 where
+
+--------------------------------------------------------------------------------
+
+import Data.Bits
+
+import CircuitCommon
+
+--------------------------------------------------------------------------------
+-- global parameters
+
+circomFile :: FilePath
+circomFile = circuitSourceDir </> "log2.circom"
+
+-- `n` = maximum number of bits
+type GP = Int
+
+mainComponent :: GP -> MainComponent
+mainComponent n = MainComponent 
+  { _templateName   = "Log2"
+  , _templateParams = [n]
+  , _publicInputs   = ["inp"]
+  }
+
+--------------------------------------------------------------------------------
+-- test cases and expected semantics
+
+type TestCase = Integer
+type Output   = (Int,[Bool])
+
+semantics :: GP -> TestCase -> Expected Output
+semantics n a 
+  | (2^k == a) && (k>0) && (k<=n)  = Expecting (k,mask) 
+  | otherwise                      = ShouldFail
+  where
+    k = ceilingLog2 a
+    mask = [ i < k | i<-[0..n] ]
+
+
+-- | Smallest integer @k@ such that @2^k@ is larger or equal to @n@
+ceilingLog2 :: Integer -> Int
+ceilingLog2 0 = 0
+ceilingLog2 n = 1 + go (n-1) where
+  go 0 = -1
+  go k = 1 + go (shiftR k 1)
+
+testCases :: GP -> [TestCase]
+testCases n = [0..2^(n+1)+3] -- [-3..2^n+3]
+
+--------------------------------------------------------------------------------
+-- inputs and outputs
+
+inputs :: GP -> TestCase -> Inputs Name Integer
+inputs n a = Inputs $ toMapping "inp" a
+
+outputs :: Output -> Outputs Name Integer
+outputs (y,mask) = Outputs $  toMapping "out"  y
+                           <> toMapping "mask" mask
+
+--------------------------------------------------------------------------------
+
+spec :: GP -> TestSpec TestCase Output
+spec n = TestSpec circomFile (mainComponent n) (inputs n) outputs (semantics n) (testCases n)
+
+specs :: [ ( GP, TestSpec TestCase Output) ]
+specs = [ (n, spec n) | n <- [1..7] ]
+
+--------------------------------------------------------------------------------
+

test/Main.hs

@@ -14,6 +14,7 @@ import qualified Circuit.BinaryLTE     as BinaryLTE
 import qualified Circuit.BinaryGTE     as BinaryGTE
 import qualified Circuit.BinaryCompare as BinaryCmp
 import qualified Circuit.ExtractBits   as ExtractBits
+import qualified Circuit.Log2          as Log2
 
 --------------------------------------------------------------------------------
 
@@ -26,6 +27,8 @@ testSimple' verbosity = do
   let runSpec     what = Spec.testSemantics     what verbosity
   let runSpecMany what = Spec.testSemanticsMany what verbosity
 
+  runSpecMany Log2.specs
+
   runSpecMany BinaryCmp.specs
   runSpecMany BinaryLTE.specs
   runSpecMany BinaryGTE.specs