add CeilingLog2 template

circuit/log2.circom

@@ -1,5 +1,8 @@
 pragma circom 2.0.0;
 
+include "misc.circom";
+
+//------------------------------------------------------------------------------
 // 
 // given an input `inp`, this template checks that inp == 2^out
 // with 0 < out <= n
@@ -36,3 +39,37 @@ template Log2(n) {
   inp === sum;  
 
 }
+
+//------------------------------------------------------------------------------
+// 
+// given an input `inp`, this template computes `k` such that 2^k <= inp < 2^{k+1}
+// it also returns the binary decomposition of `inp-1`, and the binary deocmpositiom
+// of the mask `(2^k-1)`
+//
+// we also output a mask vector which is 1 for i=0..out-1, and 0 elsewhere
+//
+
+template CeilingLog2(n) {
+
+  signal input  inp;
+  signal output out;  
+  signal output bits[n];
+  signal output mask[n];
+
+  component tb = ToBits(n);
+  tb.inp <== inp - 1; 
+  tb.out ==> bits;
+
+  signal aux[n+1];
+  aux[n] <== 1;
+  var sum = 0;
+  for(var i=n-1; i>=0; i--) {
+    aux[i]  <== aux[i+1] * (1 - bits[i]);
+    mask[i] <== 1 - aux[i];
+    sum = sum + (aux[i+1] - aux[i]) * (i+1);
+  }
+
+  out <== sum;
+}
+
+//------------------------------------------------------------------------------

test/Circuit/CeilingLog2.hs

@@ -0,0 +1,71 @@
+
+module Circuit.CeilingLog2 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   = "CeilingLog2"
+  , _templateParams = [n]
+  , _publicInputs   = ["inp"]
+  }
+
+--------------------------------------------------------------------------------
+-- test cases and expected semantics
+
+type TestCase = Integer
+type Output   = (Int,[Bool],[Bool])
+
+semantics :: GP -> TestCase -> Expected Output
+semantics n a 
+  | a >0 && k >= 0 && k < n  = Expecting (k,bits,mask) 
+  | otherwise                = ShouldFail
+  where
+    k = ceilingLog2 a
+    mask = [ i < k | i<-[0..n-1] ]
+    bits = [ testBit (a-1) i | i<-[0..n-1] ]
+
+-- | 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,bits,mask) = Outputs $  toMapping "out"  y
+                                <> toMapping "bits" bits
+                                <> 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

@@ -15,6 +15,7 @@ import qualified Circuit.BinaryGTE     as BinaryGTE
 import qualified Circuit.BinaryCompare as BinaryCmp
 import qualified Circuit.ExtractBits   as ExtractBits
 import qualified Circuit.Log2          as Log2
+import qualified Circuit.CeilingLog2   as CeilingLog2
 
 --------------------------------------------------------------------------------
 
@@ -27,6 +28,7 @@ testSimple' verbosity = do
   let runSpec     what = Spec.testSemantics     what verbosity
   let runSpecMany what = Spec.testSemanticsMany what verbosity
 
+  runSpecMany CeilingLog2.specs
   runSpecMany Log2.specs
 
   runSpecMany BinaryCmp.specs
@@ -38,5 +40,5 @@ testSimple' verbosity = do
 --------------------------------------------------------------------------------
 
 main = do
-  testSimple' Silent
+  testSimple' Silent -- Verbose  -- Silent