Integer-indexed types

[strub]

Adds integer-indexed types to EasyCrypt: type constructors parameterised by both type variables and natural-number indices, with a small index language and decidable index equality. This lets you express size-carrying types like 'a vec<:n> and track index arithmetic through operators, lemmas, instances, SMT, and cloning.

type {n} 'a vec.

op concat {n m} ['a] (xs : 'a vec<:n>) (ys : 'a vec<:m>) : 'a vec<:n+m>.
op tail   {n}   ['a] (xs : 'a vec<:n+1>) : 'a vec<:n>.

(* index inference: n+1 = 5 solves to n = 4 *)
op behead ['a] (xs : 'a vec<:5>) : 'a vec<:4> = tail xs.

Surface language

• Binders: {n m} on types, ops, preds, lemmas, notations, abbrevs, and clone overrides -- always before the type-variable binder (type {n} 'a vec).
• Type application: t<:e> with positional (mat<:3, 5>) or named (mat<:m = 5, n = 3>, partial allowed) arguments; _ holes for inference.
• Op/lemma instantiation: f[:e], positional or named/partial (f[:n = 3]), composable with type instantiation in either order (f[:3]<:int> = f<:int>[:3]).
• Section-declared indices: declare index {n}. puts n in scope for a whole section; ops and lemmas written without binders get a {n} binder back at section close. theories/datatypes/IArray.ec and IWord.ec are written this way.
• Indexed datatypes, records, and matchfix operators are supported (non-refining: every constructor's result type is the datatype at its own binders).

Index language and inference

Indices form the polynomial fragment over the naturals: variables, literals, +, *. Equality checking is complete and decidable, by canonical polynomial form (4 + 1 = 5, n + n = 2 * n, associativity/commutativity for free); type hashconsing identifies canonically-equal spellings, so vec<:8> and vec<:3+5> are one type.

Solving (inference) is deliberately restricted to a principal fragment: naked-variable assignment plus single-variable affine equations with unit coefficient and non-negative residual (?n + 1 = 5 gives n = 4; ?n + 1 = m is refused -- nothing guarantees m >= 1), with deferral and retry for equations that become affine after other assignments. General polynomial unification over the naturals is non-principal; anything outside the fragment asks for an explicit f[:...].

Indices are naturals, enforced end to end: the grammar has no negative literals or subtraction (dedicated hints), index arithmetic is closed over the naturals, the solver refuses possibly-negative solutions, and proof-term instantiation only accepts indices built from the goal's own index variables. The single axiom Int.ge0_index {k} : 0 <= k exposes this invariant as a fact (ge0_index[:n], smt(ge0_index)); its model is the discipline itself.

Standard library

• IArray: length-indexed arrays 'a array<:n> (indexed counterpart of Array.ec) -- opaque single-head accessors, get/set laws, extensionality (arrayP), injectivity, induction (arrayW), offun, map. 3 axioms (list reflection), model named in-file.
• IWord: length-indexed bit-words word<:n> over IArray (counterpart of BitWord.eca plus a JWord slice) -- bit ops with a boolean-ring instance, bit-set layer, to_uint/of_int/to_sint numeric layer with the mod-2^n arithmetic, subtraction, unsigned/signed comparisons with an order kit, shifts/rotates with composition and normalization laws. 2 axioms; the header names what is not yet ported (DWord, division, sar laws, ...).
• IntDiv gains five generic range facts (gt0_pow2, modz_cmp, ...) that bit-level developments consume (Jasmin's JUtils exports the same statements).

Ring/field instances

Instances can be named, index-parametric, and type-polymorphic, and every instance operator records its own instantiation at the carrier:

instance ring [warith] with {wsz} word<:wsz+1>
  op rzero = zeroa    op rone = onea    op add = ( + )
  op mul   = ( * )    op opp  = oppa
  op expr  = WRingA.exp        (* predecessor-shaped: recorded at [wsz] *)
  op ofint = of_int            (* literals in the theory's vocabulary  *)
  proof ...

ring [warith] then fires at any manifestly-positive width, concrete (word<:8>) or symbolic (word<:k+1>), including exponents and integer literals -- while refusing an arbitrary word<:m> (which could be word<:0>, where the instance is unsound). Bare ring keeps selecting anonymous instances, so multiple structures can coexist on one carrier. tests/ring-poly-instance.ec registers a ring over 'a -> int.

SMT

Indexed types reach the provers by sort erasure + term-level relativization: one Why3 sort per type constructor, with the index carried as (i) leading int arguments on indexed operators, (ii) per-family width observers (size x), (iii) relativized quantifiers (forall (x : t<:i>), P becomes forall x, size x = i => P), and (iv) 0 <= n facts for lemma/goal index variables. Symbolic-width goals go through unchanged -- the index is a first-class integer for the prover. Plain-bodied indexed operators export standard definitions (conservative, unguarded); the pre-relativization erasure was demonstrably unsound and the exploits are pinned as fail smt regressions (tests/indexed-smt-guards.ec).

Tooling

• hint simplify rules accept indexed heads; index patterns are restricted to the affine single-variable fragment and matched without the unification engine (constant / k / k + b per position), so a rule stated at n+1 fires at width 8 and at j+1, and unindexed rules pay nothing.
• Diagnostics distinguish ground index mismatches (incompatible index arguments: `5' vs `3') from genuinely unsolvable unifications; unknown/duplicate names, arity errors, mixed positional/named lists, negative literals, subtraction, and the >> token all get dedicated located messages.
• Cloning supports indexed type/op/pred overrides in both modes, and instance records survive replay with their per-slot instantiations.

Known limitations (deliberate, documented in-source)

1. Index solving fragment: single-variable affine with unit coefficient and non-negative residual, as above. Outside it, instantiate explicitly (f[:...]) -- including obligations whose operators appear un-applied or whose only index link is behind a definitional equality or a premise, where no inference anchor exists in principle.
2. Indexed datatypes/records are not exported to SMT: a sound erased-constructor encoding needs a hand-axiomatized datatype theory (indices as constructor arguments, relativized exhaustiveness); until then such goals are refused (CanNotTranslate skip -- incompleteness, never unsoundness) and are proved by case/elim/rewrite. Matchfix operators over them likewise stay opaque to smt.
3. f<:int vec<:3>> needs a space (...<:3> >): >> is a single operator token and the lexer is context-free; the parse error says exactly this.
4. IWord is a first slice; its header lists the unported remainder (DWord awaits an indexed FinType/Distr story).

Tests

tests/indexed-*.ec, iword_*.ec, named-index-instantiation.ec, instance-family-shape.ec, ring-poly-instance.ec, clone-indexed-override.ec, indexed-simplify-rules.ec, indexed-smt-{guards,defs}.ec -- including regression pins for every soundness issue found while hardening the branch (naturals discipline, SMT width guards, conversion index-blindness), each written from a previously-working exploit.

[oskgo]

It seems to me like unification of indexed types with unification variables in the indices is equivalent to solving systems of polynomial equations over the positive integers. This is an intractable problem in general.

What are the limitations of the unification algorithm you implement?

[alleystoughton]

It would be good to allow

op f {n m} ['a, 'b] : 'a -> 'b -> bool.

op g = f[:n = 3, m = 4]<:'a = int, 'b = real>.

[alleystoughton]

Should the operator added messages and operator printing show indices?

op f {n m} ['a, 'b] : 'a -> 'b -> bool.

op g = f[:3, 4]<:int, real>.
(*
+ added operator g : int -> real -> bool
*)
print g.
(*
* In [operators, predicates or exceptions]:

op g : int -> real -> bool = f<:int, real>.
*)

[alleystoughton]

This error message could be more specific.

op f {n m} ['a, 'b] : 'a -> 'b -> bool.

op g = f<:int, real>.
(* this operator type contains free type variables *)

[alleystoughton]

And this is pretty confusing:

op f {n m} ['a, 'b] : 'a -> 'b -> bool.

op g = f[:3]<:int, real>.
(* unknown variable or constant: `f' *)

[alleystoughton]

At the moment, there is no way to override indexed operators in cloning. We need:

type {n} 'a vec.
op cons {n} ['a] (x : 'a) (xs : 'a vec<:n>) : 'a vec<:n+1>.

theory U.

type {n} 'a foo.

op f {n} ['a] : 'a -> 'a foo<:n> -> 'a foo<:n+1>.

end U.

clone U as U' with
  type {n} 'a foo = 'a vec<:n>,
  op f {n} ['a] (x : 'a) (xs : 'a vec<:n>) = cons[:n] x xs.

[strub]

It would be good to allow op g = f[:n = 3, m = 4]<:'a = int, 'b = real>

Done in 9460bc0: index and type instantiation can each be positional or named, in any combination. Named indices may be partial (cat[:n = 3] u v infers m), and unknown names are now rejected with a proper error.

[strub]

Should the operator added messages and operator printing show indices?

Yes — fixed in 4908019: print g now shows f[:3, 4]<:int, real> (indices follow the same display policy as type arguments: hidden when inferable from the printed arguments, shown otherwise). The added-operator message already prints index binders when the operator has them (added operator f {n m} ['a, 'b] : ...); for g there is nothing to add since it has no index parameters and added messages don't show bodies.

[strub]

This error message could be more specific. / And this is pretty confusing:

Both fixed in f2074ba. Omitted indices now report

cannot infer all index parameters of this operator; supply them explicitly (e.g. `f[:n = 3]')

and an incompatible instantiation is classified per candidate instead of degenerating to "unknown variable or constant" — f[:3]<:int, real> gives

operator `Top.f' cannot be applied:
it takes 2 index parameter(s) but is given 1

(same treatment for unknown named arguments and wrong type-argument counts). Application failures also list inferred indices alongside inferred type parameters.

[strub]

What are the limitations of the unification algorithm you implement?

Right: the general problem (univars on both sides) subsumes solving polynomial systems over ℕ, so we do not attempt it. What is implemented is a small deterministic fragment, and the split matters. Checking index equality is complete: indices are compared by canonical polynomial normal form, which is decidable. Solving is restricted to (a) naked-univar assignment with an occurs-check, and (b) single-univar affine equations with net coefficient ±1 whose solution has non-negative coefficients, e.g. ?u + 1 = n + 5 yields n + 4. Constraints that are not solvable yet are deferred and retried as other assignments land; there is no search or backtracking. Everything outside the fragment is refused: multi-univar Diophantine equations, non-unit coefficients, nonlinear occurrences, and anything whose solution would need an unproven non-negativity assumption (?u + 1 = n is refused since ?u := n - 1 requires n >= 1). Refusal is conservative. The unifier never guesses, so incompleteness shows up as a type error asking for an explicit index (f[:n = 3]), never as a wrong instantiation.