1  
 2  module Circuit.BinaryLTE where
 3  
 4  --------------------------------------------------------------------------------
 5  
 6  import CircuitCommon
 7  
 8  --------------------------------------------------------------------------------
 9  -- global parameters
10  
11  circomFile :: FilePath
12  circomFile = circuitLibSourceDir </> "binary_compare.circom"
13  
14  -- | comparing @n@-bit integers
15  type GP = Int
16  
17  mainComponent :: GP -> MainComponent
18  mainComponent n = MainComponent 
19    { _templateName   = "BinaryLessOrEqual"
20    , _templateParams = [n]
21    , _publicInputs   = ["A","B"]
22    }
23  
24  --------------------------------------------------------------------------------
25  -- test cases and expected semantics
26  
27  type TestCase = (Integer,Integer)
28  type Output   = Bool
29  
30  cmp :: Integer -> Integer -> Bool
31  cmp a b = (a <= b)
32  
33  semantics :: GP -> TestCase -> Expected Output
34  semantics n (a,b) = Expecting $ cmp a b
35  
36  testCases :: GP -> [TestCase]
37  testCases n = [ (a,b) | a<-[0..2^n-1] , b<-[0..2^n-1] ]
38  
39  --------------------------------------------------------------------------------
40  -- inputs and outputs
41  
42  inputs :: GP -> TestCase -> Inputs Name Integer
43  inputs n (a,b) = Inputs $  toMapping "A" (toBitsLE' n a)
44                          <> toMapping "B" (toBitsLE' n b)
45  
46  outputs :: Output -> Outputs Name Integer
47  outputs y = Outputs $ toMapping "out" y
48  
49  --------------------------------------------------------------------------------
50  
51  spec :: GP -> TestSpec TestCase Output
52  spec n = TestSpec circomFile (mainComponent n) (inputs n) outputs (semantics n) (testCases n)
53  
54  specs :: [ ( GP, TestSpec TestCase Output) ]
55  specs = [ (n, spec n) | n <- [3,5,6] ]
56  
57  --------------------------------------------------------------------------------
58