diff --git a/circuit/log2.circom b/circuit/log2.circom index 54e26ac..78b3f74 100644 --- a/circuit/log2.circom +++ b/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; +} + +//------------------------------------------------------------------------------ diff --git a/test/Circuit/CeilingLog2.hs b/test/Circuit/CeilingLog2.hs new file mode 100644 index 0000000..f2b6041 --- /dev/null +++ b/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] ] + +-------------------------------------------------------------------------------- + diff --git a/test/Main.hs b/test/Main.hs index 033afbd..8804e01 100644 --- a/test/Main.hs +++ b/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