haloumi 0.5.15

Entrypoint crate for the Haloumi framework.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47


(prime-number 21888242871839275222246405745257275088548364400416034343698204186575808495617)
(begin-module mul_many)
(input in_0)
(input in_1)
(output out_0)
(assert (= (* 1 (+ (* adv_0_4 adv_1_4) (- out_0))) 0))
(assert (= in_0 adv_0_4))
(assert (= in_1 adv_1_4))
(end-module)
(begin-module mul_many1)
(input in_0)
(input in_1)
(input in_2)
(output out_0)
(call [cout_0_0] mul_many [in_1 in_2])
(assert (= adv_2_4 cout_0_0))
(assert (= (* 1 (+ (* adv_0_5 adv_1_5) (- out_0))) 0))
(assert (= in_0 adv_0_5))
(assert (= adv_2_4 adv_1_5))
(end-module)
(begin-module mul_many2)
(input in_0)
(input in_1)
(input in_2)
(input in_3)
(output out_0)
(call [cout_0_0] mul_many1 [in_1 in_2 in_3])
(assert (= adv_2_5 cout_0_0))
(assert (= (* 1 (+ (* adv_0_6 adv_1_6) (- out_0))) 0))
(assert (= in_0 adv_0_6))
(assert (= adv_2_5 adv_1_6))
(end-module)
(begin-module Main)
(input in_0)
(input in_1)
(input in_2)
(input in_3)
(output out_0)
(call [cout_0_0] mul_many2 [adv_0_0 adv_0_1 adv_0_2 adv_0_3])
(assert (= adv_2_6 cout_0_0))
(assert (= adv_0_0 in_0))
(assert (= adv_0_1 in_1))
(assert (= adv_0_2 in_2))
(assert (= adv_0_3 in_3))
(assert (= adv_2_6 out_0))
(end-module)