Tactic: circuit

The circuit tactic discharges or simplifies goals over finite types by translating them into boolean circuits and reasoning about the resulting bit-level representation. It applies to three goal shapes — first-order propositions, Hoare triples, and program equivalences — and has two modes, circuit and circuit simplify.

circuit attempts to close the current goal by translating it into a boolean circuit and checking that the circuit is identically true.

circuit simplify performs the same translation but does not close the goal: instead, it rewrites the postcondition using bit-level equalities derived from the circuit, leaving a simpler residual goal to be discharged by other tactics.

Important

The circuit family of tactics relies entirely on the bind family of commands to know how EasyCrypt types and operators correspond to their bit-level counterparts. Every type appearing in the goal must be bind bitstring- or bind array-bound; every operator must be bind op- or bind circuit-bound, or definable in terms of bound operators; and every program statement must be an assignment whose right-hand side translates to a circuit.

See Command: bind for the syntax and semantics of the bind commands and the catalog of supported operator names — the examples below all begin with bind declarations, whose side conditions (the realize lines) come from that catalog.

Variant: circuit (FOL)

When the goal is a first-order proposition (i.e., not a Hoare or equivalence judgement), circuit translates the formula directly into a boolean circuit and checks that it is a tautology.

The equality w1 +^ w2 = w2 +^ w1 is translated into a boolean circuit parameterised by the bits of w1 and w2 and equal to true exactly when the two sides agree. The tactic closes the goal by checking that this circuit is identically true — in effect, a case-analysis over all assignments of the input bits, but performed symbolically on the circuit structure.

The goal must contain no free type variables (the FOL case requires a ground context).

Variant: circuit (HL)

When the goal is a Hoare triple, circuit translates the precondition, the program, and the postcondition into circuits and checks that the postcondition circuit is implied by the precondition on every initial state.

The execution proceeds in three phases:

  1. Precondition processing. The precondition is split along its top-level conjunctions. Each equation of the form prog_var = expr (in either direction) is treated as a definition: it is added to the symbolic state and used to specialise the construction of all later circuits. Each remaining clause that translates to a boolean circuit is recorded as an antecedent; clauses that do not translate are silently dropped.

  2. Program translation. The body is processed instruction by instruction, maintaining a mapping from each program variable to the circuit that computes its current value from the program’s inputs. The inputs are the program variables (treated as universally quantified bit-vectors) together with any logical variables constrained by the precondition.

  3. Postcondition discharge. The postcondition is split along its conjuncts; each conjunct is translated into a boolean circuit using the input-to-output map computed in phase 2. The tactic then checks that, on every input satisfying the precondition antecedents, every postcondition circuit is true.

When the goal is an equality, the postcondition is decomposed bit-by-bit and the tactic looks for structurally identical sub-conditions across the bits, sharing them so that each input bit is examined only once.

Variant: circuit (rHL)

When the goal is a program equivalence (equiv[M.f1 ~ M.f2 : pre ==> post]), the tactic produces a separate input-to-output map for each program, then checks that the postcondition relating the two sides holds on every joint initial state satisfying the precondition.

Variant: circuit simplify

circuit simplify runs the same translation as circuit (HL) but does not attempt to close the goal. Instead, it rewrites the postcondition using the bit-level equalities derived from the circuit translation of the program, then normalises by callbyvalue reduction. The result is a new Hoare triple with the same precondition and program but a simplified postcondition, which can then be discharged by ordinary tactics.

Here the original postcondition res = a_ +^ b_ becomes true after the circuit-level simplification, which trivial then closes. More generally, circuit simplify is useful as a preprocessing step when the full circuit translation would succeed only on part of the postcondition and other reasoning is needed for the rest.

circuit simplify only applies to Hoare triples.

Failure modes

Both circuit and circuit simplify may fail in the following ways:

failed to verify postcondition

The translation succeeded but the resulting circuit is not a tautology — i.e., the postcondition is genuinely false on some input satisfying the precondition, or its translation was too weak to capture the property.

exception(s) not supported

The Hoare triple’s postcondition includes an exception-monad invariant component; the circuit translation handles only the pure (inv-empty) part of the goal.

circuit solve failed with error: … (or Circuit simplify failed with error: …)

A CircError was raised during translation. The most common causes are: an operator with no bind op or bind circuit binding; a type with no bind bitstring or bind array binding; a program statement that is not a translatable assignment.

Wrong goal shape

circuit simplify was invoked on a goal that is not a Hoare triple.

Limitations

  • Program statements must be assignments whose right-hand sides translate into circuits. Control flow (if, while, match) and module/procedure calls are not handled — they must be eliminated (e.g. via unrolling or inlining) before circuit is invoked.

  • Sampling statements (<$) and exception-raising statements are not supported.

  • Every type appearing in the goal must be either bind bitstring-bound to a concrete (non-abstract) size, or bind array-bound with a bound element type.

  • The FOL variant additionally requires that the goal has no free type variables.

  • The cost of the equivalence check grows with the bit-width of the variables and the depth of the resulting circuit; goals over large bitstrings or with many independent inputs may be infeasible to check directly. circuit simplify and the extens tactical (see Tactical: extens) are the usual escape hatches.

Tactic: proc change circuit

proc change circuit rewrites a contiguous run of program statements into an alternative block, using circuit equivalence as the soundness check. Unlike the regular proc change — which generates a separate proof obligation for the equivalence of the two fragments — proc change circuit discharges that obligation automatically through the same machinery as the circuit tactic.

Syntax

proc change circuit [bindings]? cpos + N { stmt } .

  • cpos is the code position at which to begin rewriting.

  • N is the number of source instructions to replace, starting at cpos.

  • stmt is the replacement block, enclosed in braces.

  • [bindings] (optional) introduces fresh local variables visible only inside the replacement block, using the standard [x : ty, …] syntax. This lets the new code use intermediate names that did not exist in the original procedure.

The equivalence check considers only those variables that are live at the end of the rewritten region — i.e., read by the rest of the procedure body or by the postcondition. Variables written by the replacement block but never read again may freely differ.

The single instruction at code position 1 is replaced by c <- b +^ a; the circuit-equivalence checker establishes that the two fragments agree on the value of c, which is the only variable read downstream.

The [d : W8] binding introduces a fresh local that exists only inside the replacement block; the original procedure body has no such variable.

Failure modes (proc change circuit)

statements are not circuit-equivalent

Both fragments translated into circuits, but the equivalence check failed. This means the rewrite is genuinely unsound on at least one live output. (Use fail proc change circuit … to assert that a rewrite is rejected — see tests/proc-change-circuit.ec for an example.)

circuit-equivalence checker error: …

Translation of one of the fragments raised an exception. The typical cause is the same as for circuit: an unbound operator, an unbound type, or a non-assignment instruction inside the region being replaced.

exceptions not supported

The postcondition’s exception-monad invariant is non-empty.