Command: bind

The bind family of commands declares a correspondence between EasyCrypt objects and their counterparts in the boolean-circuit world used by the circuit family of tactics.

Four variants are available:

• bind bitstring — declares that a type is a fixed-size bitstring, by giving an isomorphism with bool list together with conversions from/to (signed and unsigned) integers.

• bind array — declares that a polymorphic type constructor is a fixed-size array, by giving access/update operators plus an isomorphism with list. The element type need not be a bitstring at the time of binding, but it must become one whenever the array type is used at a circuit-translated site.

• bind op — declares that a user-defined operator implements one of a fixed catalog of bitvector/array primitives (corresponding to the operators of the QFABV theory of SMT-LIB). A monomorphic and a multi-type form are available.

• bind circuit — asserts that a user-defined operator is semantically equivalent to a circuit definition given in the low-level specification (.spec) language. These bindings are trusted and become part of the TCB (see the warning below).

Each variant may be prefixed with the locality modifier local or global, with the usual section-locality semantics. The default, inside a section, is to be exported; outside a section the modifier is ignored.

Variant: bind bitstring

Syntax

bind bitstring to_bits from_bits to_uint to_sint of_int type size .

The seven arguments are: the two halves of the type ↔ bool list isomorphism (to_bits, from_bits), the two integer projections (to_uint for the unsigned reading and to_sint for the two’s-complement signed reading), the integer injection (of_int), the type being bound, and its size in bits (an integer formula).

The command leaves seven side conditions to be discharged via realize (in this example with admit; in practice they should be proved from the type’s defining equations). The axioms are those of the abstract BV theory in theories/datatypes/QFABV.ec:

Axiom	Statement
gt0_size	0 < size
size_tolist	size (tolist bv) = size (the list image has the expected length)
tolistP	oflist (tolist bv) = bv (round-trip via the list isomorphism)
oflistP	size xs = size => tolist (oflist xs) = xs (other direction, on lists of the right length)
touintP	touint bv = bs2int (tolist bv) (unsigned reading)
tosintP	two’s-complement reading: tosint bv = touint bv when the MSB is 0, and touint bv - 2^size otherwise (with size = 1 as a degenerate case)
ofintP	ofint i = oflist (int2bs size i) (integer injection is the inverse of bs2int on size-many bits)

Variant: bind array

Syntax

bind array get set tolist oflist type size .

The six arguments are: read/write operators (get of type 'a t -> int -> 'a and set of type 'a t -> int -> 'a -> 'a t), the two halves of the type ↔ list isomorphism (tolist, oflist), the (polymorphic) type constructor being bound, and the array length.

The command leaves six side conditions to be discharged. The axioms are those of the abstract A theory in theories/datatypes/QFABV.ec:

Axiom	Statement
gt0_size	0 < size
tolistP	to_list a = mkseq (fun i => get a i) size (the list view is the canonical enumeration)
oflistP	for indices 0 <= i < size, nth dfl xs i = get (of_list dfl xs) i (the list-to-array constructor preserves indexing in range)
eqP	extensional equality: two arrays are equal iff they agree at every in-range index
get_setP	get (set a j v) i is v if i = j, else get a i (in-range)
get_out	out-of-range reads agree across all arrays (i.e. the value at an out-of-range index is unspecified-but-uniform)

Variant: bind op

Syntax

bind op type operator " name " .

bind op [ type₁ & type₂ & … ] operator " name " .

The first (monomorphic) form is for operators whose signature mentions a single bound type. The second (multi-type) form takes a &-separated list of types inside brackets and is needed for operators whose signature mixes types — for instance get (a bitstring and a single-bit bitstring) or ainit (a bitstring index type and an array element type).

The name string must be one of the operator catalog below.

The [W8 & bool] syntax names the two bitstring types involved in get’s signature: the bitvector being indexed, and the single-bit bitvector holding the extracted bit. Since bool is a primitive type, it must itself be bind bitstring-bound (to size 1) before it can appear in a multi-type bind op.

Each bind op leaves a single side condition of the form bv<name>P, stating the semantics of the operator (e.g. bvxorP for xor, bvgetP for get). Multi-type bindings may also leave size-relation side conditions, e.g. le_size (one bitstring size bounds another), eq1_size (a bitstring has size one). These all come from the corresponding sub-theories of BVOperators in theories/datatypes/QFABV.ec.

Only this base catalog of operators needs an explicit binding. Operators built on top of them are translated into circuits by recursive descent through their definitions, applying the bindings at the leaves and composing the resulting sub-circuits.

Operator catalog

The name argument to bind op must be one of the following. The “Types” column shows the shape of the bracketed type list expected by the multi-type form (BV = a bitstring type, BV[1] = a bitstring type of size 1, A = an array type); single-BV operators may also be given to the monomorphic form.

Arithmetic (one BV argument):

add, sub, mul, opp

signed-wrap arithmetic on bitvectors of size n.

udiv, urem, sdiv, srem

unsigned and signed division and remainder.

Bitwise (one BV argument):

and, or, xor, not

pointwise boolean operations.

Constant shifts (one BV argument):

shl, shr, ashr

shift left, logical shift right, arithmetic (sign-extending) shift right.

rol, ror

rotate left, rotate right.

Variable shifts (BV & BV — value, amount):

shls, shrs, ashrs

shift left / logical shift right / arithmetic shift right where the shift amount is itself a bitvector.

Comparisons (BV[1] & BV — result and operand):

ult, ule, slt, sle

unsigned and signed strict and non-strict ordering, returning a one-bit bitvector.

Size manipulation (BV & BV — source and target sizes):

zextend, sextend

zero- and sign-extension to a wider bitvector.

truncate

truncation to a narrower bitvector.

insert, extract, aextract

insert/extract a sub-bitvector; aextract is the arithmetic-extracting variant.

concat (BV & BV & BV)

concatenation of two bitvectors.

Bit-level indexing:

init (BV[1] & BV)

build a bitvector from a function int -> bit.

get (BV & BV[1])

extract a single bit at a given index.

Array primitives:

ainit (BV & A)

build an array of bitvectors from a function int -> BV.

asliceget (BV & BV & A), asliceset (BV & BV & A)

read/write a sub-bitvector slice spanning array cells.

a2b (BV & BV & A), b2a (BV & BV & A)

reshape between a single wide bitvector and an array of bitvectors whose concatenation has the same width.

map (BV & BV & A)

pointwise map of a bitvector function over an array of bitvectors.

Variant: bind circuit

Syntax

bind circuit op₁ <- " name₁ " , … , opₖ <- " nameₖ " from " file " .

A non-empty comma-separated list of op <- "name" associations is followed by a mandatory from "<file>" clause naming the .spec file from which the named circuit definitions are loaded.

Warning

The equivalences declared by bind circuit are trusted: no proof obligation is generated, and so an incorrect binding silently becomes part of the trusted computing base of every proof that uses it. Use bind op whenever possible. The recommended use of bind circuit is to attach circuit semantics to operators that are otherwise abstract, treating the binding as an axiomatisation rather than as a definition — proofs about the operator are then discharged via the circuit tactic, which makes use of these semantics.

A typical use looks like the following (this example is shown as plain text rather than as a checked proof because it depends on a spec file outside the example’s working directory):

require import AllCore List QFABV.

type W8.

op to_bits : W8 -> bool list.
op from_bits : bool list -> W8.
op of_int : int -> W8.
op to_uint : W8 -> int.
op to_sint : W8 -> int.

bind bitstring
  to_bits from_bits to_uint to_sint of_int W8 8.
(* ... realize side conditions ... *)

op (+^) : W8 -> W8 -> W8.

bind circuit
  (+^) <- "BVXOR_8" from "specs.spec".

The definition of the BVXOR_8 circuit, in the companion specs.spec file, is:

BVXOR_8(w1@8, w2@8) -> @8 =
  xor<8>(w1, w2)

Each op named in the binding list must already be declared, its arity must match the corresponding spec definition, and every argument and the return type must be bind bitstring-bound to a bitstring of the size declared in the spec.