Skip to content

Commit 5573b37

Browse files
Gustavo2622Gustavo2622
committed
Added documentation and tests for circuit tactics
1 parent 2260a26 commit 5573b37

File tree

4 files changed

+221
-0
lines changed

4 files changed

+221
-0
lines changed

‎doc/tactics/bindings.rst‎

Lines changed: 216 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,216 @@
1+
========================================================================
2+
Command: `bind`
3+
========================================================================
4+
5+
The ``bind`` family of commands is used to allow translation of EasyCrypt
6+
objects into boolean circuits for use in the `circuit` family of tactics.
7+
8+
We have the following possibilities for these commands:
9+
10+
- `bind bitstring`, which establishes a bijection between the given type
11+
and a type of fixed size bitstrings through given isomorphisms with lists
12+
of booleans (plus necessary side conditions)
13+
14+
- `bind array`, which establishes the bijection between the given type constructor
15+
(which must be polymorphic over a given type which must be bound to a
16+
bitstring type in instantiations) and the type of arrays of a given fixed size.
17+
18+
- `bind op`, which establishes the semantic equivalence of the given operator to
19+
a specified operator from a fixed list (detailed below), which roughly corresponds
20+
to the operators supported by the QFABV theory of SMTLib.
21+
22+
- `bind circuit`, which asserts the semantic equivalence of the given operator to
23+
the one given by a definition in the low level specification (spec) language.
24+
All equivalences establishes through this particular mean are trusted (rather than
25+
verified) and so become part of the TCB for the given proof.
26+
27+
.. contents::
28+
:local:
29+
30+
------------------------------------------------------------------------
31+
Variant: ``bind bitstring``
32+
------------------------------------------------------------------------
33+
34+
.. ecproof::
35+
:title: Bitstring Binding Example
36+
37+
require import AllCore List QFABV.
38+
39+
type W8.
40+
41+
op to_bits : W8 -> bool list.
42+
op from_bits : bool list -> W8.
43+
op of_int : int -> W8.
44+
op to_uint : W8 -> int.
45+
op to_sint : W8 -> int.
46+
47+
(*$*) bind bitstring
48+
to_bits
49+
from_bits
50+
to_uint
51+
to_sint
52+
of_int
53+
W8
54+
8.
55+
56+
realize gt0_size by admit.
57+
realize tolistP by admit.
58+
realize oflistP by admit.
59+
realize touintP by admit.
60+
realize tosintP by admit.
61+
realize ofintP by admit.
62+
realize size_tolist by admit.
63+
64+
65+
Here we have an example of defining a type and establishing
66+
its equivalence with the type of bitstring of size 8, along
67+
with the side conditions needed to verify that equivalence.
68+
Since we only give an abstract type, these side conditions
69+
are admitted, but in a real example they would need to be
70+
proven using the semantics of whatever type we were using.
71+
72+
------------------------------------------------------------------------
73+
Variant: ``bind array``
74+
------------------------------------------------------------------------
75+
76+
.. ecproof::
77+
:title: Array Binding Example
78+
79+
require import AllCore List QFABV.
80+
81+
theory Array8.
82+
type 'a t.
83+
84+
op tolist : 'a t -> 'a list.
85+
op oflist : 'a list -> 'a t.
86+
op "_.[_]" : 'a t -> int -> 'a.
87+
op "_.[_<-_]" : 'a t -> int -> 'a -> 'a t.
88+
89+
end Array8.
90+
91+
(*$*) bind array Array8."_.[_]" Array8."_.[_<-_]" Array8.tolist Array8.oflist Array8.t 8.
92+
realize gt0_size by auto.
93+
realize tolistP by admit.
94+
realize eqP by admit.
95+
realize get_setP by admit.
96+
realize get_out by admit.
97+
98+
99+
In this example, we can see how the correspondence is established
100+
for a given polymorphic array type. As in the example above, we
101+
use an abstract type and admit the side conditions for simplicity
102+
of presentation, but in a real case we would have to use the
103+
semantics of our array type in order to discharge these conditions.
104+
105+
106+
------------------------------------------------------------------------
107+
Variant: ``bind op``
108+
------------------------------------------------------------------------
109+
110+
.. ecproof::
111+
:title: Operator Binding Example
112+
113+
require import AllCore List QFABV.
114+
115+
type W8.
116+
117+
op to_bits : W8 -> bool list.
118+
op from_bits : bool list -> W8.
119+
op of_int : int -> W8.
120+
op to_uint : W8 -> int.
121+
op to_sint : W8 -> int.
122+
123+
bind bitstring
124+
to_bits
125+
from_bits
126+
to_uint
127+
to_sint
128+
of_int
129+
W8
130+
8.
131+
132+
realize gt0_size by admit.
133+
realize tolistP by admit.
134+
realize oflistP by admit.
135+
realize touintP by admit.
136+
realize tosintP by admit.
137+
realize ofintP by admit.
138+
realize size_tolist by admit.
139+
140+
op (+^) : W8 -> W8 -> W8.
141+
142+
(*$*) bind op W8 (+^) "xor".
143+
realize bvxorP by admit.
144+
145+
146+
Here we give an example of giving the semantic equivalence for
147+
an operator. We again instantiate this abstractly and admit the
148+
side conditions for ease of exposition, assuming that in a real
149+
case the semantics of the operator itself would be used in order
150+
to show that the conditions hold.
151+
152+
Of note that these bindings are only necessary for a base subset
153+
of operators, and further operators defined in terms of these basic
154+
ones are translated through recursive descent through their definition,
155+
usage of these base cases and a notion of composition for boolean circuits.
156+
157+
158+
------------------------------------------------------------------------
159+
Variant: ``bind circuit``
160+
------------------------------------------------------------------------
161+
.. ecproof::
162+
:title: Spec Binding Example
163+
164+
require import AllCore List QFABV.
165+
166+
type W8.
167+
168+
op to_bits : W8 -> bool list.
169+
op from_bits : bool list -> W8.
170+
op of_int : int -> W8.
171+
op to_uint : W8 -> int.
172+
op to_sint : W8 -> int.
173+
174+
bind bitstring
175+
to_bits
176+
from_bits
177+
to_uint
178+
to_sint
179+
of_int
180+
W8
181+
8.
182+
183+
realize gt0_size by admit.
184+
realize tolistP by admit.
185+
realize oflistP by admit.
186+
realize touintP by admit.
187+
realize tosintP by admit.
188+
realize ofintP by admit.
189+
realize size_tolist by admit.
190+
191+
op (+^) : W8 -> W8 -> W8.
192+
193+
(*$*) bind circuit
194+
(+^) <- "BVXOR_8".
195+
196+
Here we have an example of attributing semantics coming from a
197+
low level specification language (spec) file to an operator.
198+
We remark again that these equivalences are trusted and so a
199+
potential source of error and unsoundness. This will be subject
200+
to change in the future, but until then the recommended way
201+
to use them is to be very careful or otherwise just bind
202+
operators which are abstract and use these bindings as an
203+
axiomatization (proving lemmas about these through the use
204+
of the circuit family of tactics which is able to make use
205+
of these semantics).
206+
207+
The definition of the ``BVXOR_8`` operator in the spec language
208+
is as follows::
209+
210+
BVXOR_8(w1@8, w2@8) -> @8 =
211+
xor<8>(w1, w2)
212+
213+
214+
..
215+
This is similar to what is done to establish a correspondence
216+
between the basic types and their counterparts in the SMTs.

‎easycrypt.project‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
[general]
22
provers = CVC5@1.0
33
provers = Z3@4.12
4+
spec = examples/example_specs.spec

‎examples/example_specs.spec‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
BVXOR_8(w1@8, w2@8) -> @8 =
2+
xor<8>(w1, w2)

‎tests/circuit_test.ec‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -174,3 +174,5 @@ proof.
174174
circuit.
175175
qed.
176176

177+
bind circuit
178+
(+^) <- "BVXOR_8".

0 commit comments

Comments
 (0)