Skip to content

Commit 2260a26

Browse files
Gustavo2622Gustavo2622
committed
Started documenting circuit tactic and small fix to circuit test
1 parent fc94b6c commit 2260a26

2 files changed

Lines changed: 216 additions & 6 deletions

File tree

‎doc/tactics/circuit.rst‎

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
2+
========================================================================
3+
Tactic: `circuit`
4+
========================================================================
5+
6+
The ``circuit`` tactic can be used to resolve a multitude of goals where
7+
the semantics in question are over finite types.
8+
9+
There are currently two variants of this tactic:
10+
11+
- `circuit`, which attempts to automatically solve/prove the goal
12+
13+
- `circuit simplify`, which performs a simplification over the goal structure
14+
augmented by equivalence checks whenever an equality between two finite types
15+
with bindings is encountered.
16+
17+
.. contents::
18+
:local:
19+
20+
..
21+
------------------------------------------------------------------------
22+
Variant: ``circuit`` (FOL)
23+
------------------------------------------------------------------------
24+
.. ecproof::
25+
:title: First-order logic example
26+
27+
require import AllCore List QFABV.
28+
29+
type W8.
30+
31+
op to_bits : W8 -> bool list.
32+
op from_bits : bool list -> W8.
33+
op of_int : int -> W8.
34+
op to_uint : W8 -> int.
35+
op to_sint : W8 -> int.
36+
37+
bind bitstring
38+
to_bits
39+
from_bits
40+
to_uint
41+
to_sint
42+
of_int
43+
W8
44+
8.
45+
46+
realize gt0_size by admit.
47+
realize tolistP by admit.
48+
realize oflistP by admit.
49+
realize touintP by admit.
50+
realize tosintP by admit.
51+
realize ofintP by admit.
52+
realize size_tolist by admit.
53+
54+
op (+^) : W8 -> W8 -> W8.
55+
bind op W8 (+^) "xor".
56+
realize bvxorP by admit.
57+
58+
lemma L (w1 w2 : W8) : w1 +^ w2 = w2 +^ w1.
59+
proof.
60+
proc. (*$*) circuit solve.
61+
abort.
62+
63+
As we can see, the tactic can, through the generation of the appropriate
64+
circuit representing validity of the proposition for a given value and
65+
the equation of this function with the constant function equal to true,
66+
establish the truth of the lemma.
67+
This is, in a sense, a reverse use of function extensionality, to convert
68+
statements about functions to statements about universal quantification.
69+
70+
71+
------------------------------------------------------------------------
72+
Variant: ``circuit`` (HL)
73+
------------------------------------------------------------------------
74+
75+
.. ecproof::
76+
:title: Hoare logic example
77+
78+
require import AllCore List QFABV.
79+
80+
type W8.
81+
82+
op to_bits : W8 -> bool list.
83+
op from_bits : bool list -> W8.
84+
op of_int : int -> W8.
85+
op to_uint : W8 -> int.
86+
op to_sint : W8 -> int.
87+
88+
bind bitstring
89+
to_bits
90+
from_bits
91+
to_uint
92+
to_sint
93+
of_int
94+
W8
95+
8.
96+
97+
realize gt0_size by admit.
98+
realize tolistP by admit.
99+
realize oflistP by admit.
100+
realize touintP by admit.
101+
realize tosintP by admit.
102+
realize ofintP by admit.
103+
realize size_tolist by admit.
104+
105+
op (+^) : W8 -> W8 -> W8.
106+
bind op W8 (+^) "xor".
107+
realize bvxorP by admit.
108+
109+
module M = {
110+
proc f(w : W8) = {
111+
return w +^ w;
112+
}
113+
}.
114+
115+
lemma L (w_ : W8) : hoare[M.f : w_ = w ==> res = of_int 0].
116+
proof.
117+
proc. (*$*) circuit.
118+
abort.
119+
120+
121+
As we can see from the output, the execution of the tactic has several components:
122+
123+
- The translation of the precondition to a circuit, using any explicit equations
124+
that define values of program variables at the start of execution in the further
125+
construction of circuits henceforth.
126+
127+
- The translation of the program to a (collection of) circuits. This is done instruction-wise
128+
by keeping and updating a mapping from program variables to circuits determining how their
129+
value is obtained from the value of some initial "input" variables. In the case of a program
130+
these are either logical variables constraining initial values of program variables or the
131+
program variables themselves, interpreted as symbols which are then universally quantified.
132+
133+
- The translation of the postcondition into a circuit outputting a boolean, representing whether
134+
the postcondition holds for given values of the input variables. The knowledge of how the
135+
inputs relate to the outputs through the program and the knowledge of any initial relations
136+
or known facts about these variables coming from the precondition or proof context is also
137+
incorporated into this circuit. The goal of the tactic is then to prove that this circuit
138+
is identically true for all values of the input, which is equivalent to the given hoare triple
139+
being valid/true under the current proof context.
140+
141+
In the case where the goal is an equality, some extra optimization are effected.
142+
This corresponds to a heuristic inferrence procedure which tries to find structurally identical
143+
conditions in order to avoid having to check the same condition more than once and also reduce
144+
the number of inputs which are considered for each condition check, in order to reduce checking time.
145+
146+
147+
------------------------------------------------------------------------
148+
Variant: ``circuit`` (rHL)
149+
------------------------------------------------------------------------
150+
151+
.. ecproof::
152+
:title: Program equivalence example
153+
154+
require import AllCore List QFABV.
155+
156+
type W8.
157+
158+
op to_bits : W8 -> bool list.
159+
op from_bits : bool list -> W8.
160+
op of_int : int -> W8.
161+
op to_uint : W8 -> int.
162+
op to_sint : W8 -> int.
163+
164+
bind bitstring
165+
to_bits
166+
from_bits
167+
to_uint
168+
to_sint
169+
of_int
170+
W8
171+
8.
172+
173+
realize gt0_size by admit.
174+
realize tolistP by admit.
175+
realize oflistP by admit.
176+
realize touintP by admit.
177+
realize tosintP by admit.
178+
realize ofintP by admit.
179+
realize size_tolist by admit.
180+
181+
op (+^) : W8 -> W8 -> W8.
182+
bind op W8 (+^) "xor".
183+
realize bvxorP by admit.
184+
185+
module M = {
186+
proc f1(w1 w2 : W8) = {
187+
var a : W8;
188+
a <- w1 +^ w2;
189+
return a;
190+
}
191+
192+
proc f2(w1 w2 : W8) = {
193+
var a : W8;
194+
a <- w2 +^ w1;
195+
return a;
196+
}
197+
}.
198+
199+
lemma L : equiv[M.f1 ~ M.f2 : ={arg} ==> ={res}].
200+
proof.
201+
proc. (*$*) circuit.
202+
abort.
203+
204+
205+
As we can see in this example, the tactic is also able to automatically prove
206+
equivalence of these two programs. The way this is done is similar to the way
207+
that single procedures are handled, but now we consider two sets of transformations
208+
from input to outputs variables, one for each program. We then use this knowledge
209+
to convert the postcondition into the appropriate circuit and use the same procedure
210+
to attempt to automatically discharge it.

‎tests/circuit_test.ec‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
require import AllCore List QFABV IntDiv.
22

3-
43
theory FakeWord.
54
type W.
65
op size : int.
@@ -30,6 +29,12 @@ realize size_tolist by admit.
3029

3130
op zero : W = of_int 0.
3231
op one : W = of_int 1.
32+
op (+^) : W -> W -> W.
33+
34+
bind op W (+^) "xor".
35+
realize bvxorP by admit.
36+
37+
end FakeWord.
3338

3439
op bool2bits (b : bool) : bool list = [b].
3540
op bits2bool (b: bool list) : bool = List.nth false b 0.
@@ -47,12 +52,7 @@ realize touintP by admit.
4752
realize tosintP by done.
4853
realize gt0_size by done.
4954

50-
op (+^) : W -> W -> W.
51-
52-
bind op W (+^) "xor".
53-
realize bvxorP by admit.
5455

55-
end FakeWord.
5656

5757
type W8.
5858

0 commit comments

Comments
 (0)