diff --git a/circuit/log2.circom b/circuit/log2.circom new file mode 100644 index 0000000..54e26ac --- /dev/null +++ b/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 "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] ] + +-------------------------------------------------------------------------------- + diff --git a/test/Main.hs b/test/Main.hs index d408ca6..033afbd 100644 --- a/test/Main.hs +++ b/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