Tactical: extens

extens is a tactical that performs an extensionality-style case-split: it enumerates the concrete values of a finite quantity, generates one subgoal per case, and runs a user-supplied tactic on each generated subgoal. The original goal closes only when every subgoal closes.

Two goal shapes are recognised, distinguished by the presence or absence of the bracketed binder:

• A first-order proposition of the form all P (iota_ start len) (over int) — no binder. The split produces one subgoal P i per integer i in the range [start, start+len).

• A Hoare triple hoare[M.f : pre ==> post] together with a binder [v] naming a program variable. The variable’s type must be bind bitstring-bound (see Command: bind). The split produces 2^n Hoare triples (with n the bound bitstring size), in each of which the program variable v has been substituted by the corresponding of_int i everywhere — in the program, in the precondition, and in the postcondition.

In both cases the inner tactic is then run on each generated subgoal. If a subgoal fails to close, the residual goal is reported as an error.

Syntax

extens [v]? : tactic

The bracketed binder [v] is required for the Hoare-triple variant (it picks the program variable to enumerate) and forbidden for the iota_ variant.

The most common use is extens [v] : circuit (or, with simplification first, extens [v] : (circuit simplify; ...)). The benefit over a bare circuit is that the per-case translation sees a program in which one input has been replaced by a concrete constant, which lets circuit translation succeed on programs whose whole-input translation would fail or blow up.

Variant: List enumeration over iota_

The goal all (fun i => a.[i] = a.[i]) (iota_ 0 8) is split into eight independent subgoals (one per i in [0, 8)), each of which is then discharged by circuit.

Both the start and len arguments of iota_ must be ground integer literals; extens rejects a non-constant range with Iota start should be constant or Iota length should be constant.

Variant: Hoare-triple enumeration over a bitstring variable

The binder [a] picks the program variable to enumerate. Since a : W8 is bound to an eight-bit bitstring, the tactic produces 2^8 = 256 Hoare triples in which a has been replaced by each concrete value of_int i; the supplied tactic wp; skip; smt() then closes each.

This pattern is most useful when the inner tactic is circuit itself: replacing one program input by a concrete constant often lets the per-case circuit translation succeed even when the whole-program circuit translation would not. The same example with circuit as the inner tactic:

The 2^n blow-up makes this variant practical only for small bit widths: n = 8 already produces 256 subgoals, and the cost grows exponentially.

Failure modes

Wrong goal shape

The goal is neither all _ (iota_ _ _) nor a Hoare triple, or the binder presence does not match the goal shape (binder given on an iota_ goal, or omitted on a Hoare triple).

Failed to find var <name> in memory <m>

The bracketed binder names a variable that does not exist in the Hoare triple’s memory.

Failed to get size for type <τ>

The bracketed binder names a variable whose type is not bind bitstring-bound (or is bound only abstractly, without a concrete size). Arrays are not currently supported for the binder.

Iota start should be constant / Iota length should be constant

The iota_ arguments are not ground integer literals.

Unsupported List pattern

The list inside all is not of the form iota_ start len.

Failed to close goal: <residual>

The inner tactic ran on every subgoal but left at least one unclosed. The residual goal is reported as part of the error.