Integer-indexed types

Type constructors parameterised by both type variables and
natural-number indices, with a small index language and decidable
index equality: size-carrying types like 'a vec<:n>, with index
arithmetic tracked through operators, lemmas, instances, SMT, and
cloning.

- surface: {n} binders on types/ops/preds/lemmas/notations/abbrevs
  and clone overrides; type application t<:e> and op/lemma
  instantiation f[:e], positional or named (partial), composable in
  either order; `declare index {n}' sections; `_' inference holes;
  indexed (non-refining) datatypes, records, matchfix operators
- indices are polynomials over the naturals with canonical-form
  equality (hashconsing identifies vec<:8> and vec<:3+5>); solving is
  restricted to a principal fragment (naked assignment + unit-
  coefficient single-variable affine with non-negative residual,
  with deferral); the naturals discipline is enforced at every entry
  point and exposed as the single axiom Int.ge0_index
- stdlib: IArray (length-indexed arrays) and IWord (length-indexed
  bit-words: bit/bit-set layers, boolean ring, Z/2^n arithmetic with
  to_uint/of_int, comparisons, shifts/rotates); five generic range
  facts promoted to IntDiv
- ring/field instances are named, index-parametric, and
  type-polymorphic; each instance records ONE shared instantiation
  (index expressions and type arguments over its binders), with a
  uniformity check at declaration; oner_neq0 is no longer a ring-
  instance obligation (the tactic's certificates are purely
  equational, so the trivial ring is a sound carrier; fields keep
  it), making the word arithmetic instance family-wide:
  `instance ring [warith] with {n} word<:n>' fires at concrete
  widths, word<:k+1>, bare symbolic word<:m>, and word<:0>
- SMT: sort erasure + term-level relativization (leading int
  arguments on indexed ops, width observers, relativized
  quantifiers, 0 <= n facts); plain-bodied indexed ops export
  standard definitions; indexed datatypes are refused (sound
  incompleteness), with the encoding design documented as follow-up
- hint simplify rules over indexed heads (affine index patterns,
  matched without the unification engine)
- dedicated diagnostics: ground index mismatches vs unsolvable
  unifications, naturals hints (negative literals, subtraction),
  `>>' token, mixed positional/named argument lists

Author: strub

examples/MEE-CBC/FunctionalSpec.ec

@@ -109,7 +109,6 @@ instance bring with block
   op mul   = Self.andb
   op opp   = Self.oppb
 
-  proof oner_neq0 by apply/oneb_neq0
   proof addr0     by apply/xorb0
   proof addrA     by apply/xorbA
   proof addrC     by apply/xorbC

src/ecAlgTactic.ml

@@ -30,7 +30,12 @@ module Axioms = struct
   let cN    = "Cn"
   let cP    = "Cp"
 
-  let core_add  = ["oner_neq0"; "addr0"; "addrA"; "addrC";]
+  (* [oner_neq0] is NOT part of the ring obligations: the tactic's
+     certificates are purely equational (a disequality cannot occur in
+     a normalization proof), so the trivial ring is a sound carrier --
+     e.g. an instance over the whole family [word<:n>], including
+     width 0. Fields keep requiring it (division). *)
+  let core_add  = ["addr0"; "addrA"; "addrC";]
   let core_mul  = [ "mulr1"; "mulrA"; "mulrC"; "mulrDl"]
   let core      = core_add @ "addrN" :: core_mul
   let core_bool = core_add @ "addrK" :: "mulrK" :: core_mul
@@ -39,7 +44,7 @@ module Axioms = struct
   let intpow    = ["expr0"; "exprS"]
   let ofint     = ["ofint0"; "ofint1"; "ofintS"; "ofintN"]
   let ofsub     = ["subrE"]
-  let field     = ["mulrV"; "exprN"]
+  let field     = ["oner_neq0"; "mulrV"; "exprN"]
   let ofdiv     = ["divrE"]
   let cNax      = ["Cn_eq0"]
   let cPax      = ["Cp_idp"]
@@ -80,7 +85,7 @@ module Axioms = struct
     let addctt = fun subst x f -> EcSubst.add_opdef subst (xpath x) ([], f) in
 
     let subst  =
-      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], cr.r_type) in
+      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], [], cr.r_type) in
     let subst  =
       List.fold_left (fun subst (x, p) -> add subst x p) subst crcore in
     let subst  = odfl subst (cr.r_opp |> omap (fun p -> add subst opp p)) in
@@ -113,6 +118,33 @@ module Axioms = struct
     let subst = odfl subst (cr.f_div |> omap (fun p -> add subst div p)) in
       subst
 
+  (* The op paths of an instance carry their instantiation implicitly
+     (every op shares the instance's [r_insts]). The template axioms
+     reference the ops without instantiation, and [subst_of_ring]
+     swaps paths but cannot re-introduce it; so we patch the
+     substituted axiom, tagging every instance-op occurrence with the
+     shared targs. A no-op for uninstantiated instances. *)
+  let ring_op_paths (cr : ring) : EcPath.Sp.t =
+    let ps = [cr.r_zero; cr.r_one; cr.r_add; cr.r_mul] in
+    let ps = ps @ List.filter_map (fun x -> x) [cr.r_opp; cr.r_sub; cr.r_exp] in
+    let ps = match cr.r_embed with `Embed p -> p :: ps | _ -> ps in
+    EcPath.Sp.of_list ps
+
+  let field_op_paths (cr : field) : EcPath.Sp.t =
+    let ps = cr.f_inv :: List.filter_map (fun x -> x) [cr.f_div] in
+    List.fold_left (fun s p -> EcPath.Sp.add p s) (ring_op_paths cr.f_ring) ps
+
+  let inject_targs (opset : EcPath.Sp.t) (insts : EcAst.targs) (f : form) =
+    let open EcAst in
+    if insts.indices = [] && insts.types = [] then f else
+    let rec doit f =
+      match f.f_node with
+      | Fop (p, ta)
+          when EcPath.Sp.mem p opset && ta.indices = [] && ta.types = [] ->
+          f_op_r p insts (f_ty f)
+      | _ -> f_map (fun ty -> ty) doit f
+    in doit f
+
   (* FIXME: should use operators inlining when available *)
   let get cr env axs =
     let subst  =
@@ -121,10 +153,16 @@ module Axioms = struct
       | `Field cr -> subst_of_field cr
     in
 
+    let (opset, insts) =
+      match cr with
+      | `Ring  cr -> ring_op_paths  cr, cr.r_insts
+      | `Field cr -> field_op_paths cr, cr.f_ring.r_insts
+    in
+
     let for1 axname =
       let ax = EcEnv.Ax.by_path (EcPath.pqname tmod axname) env in
-        assert (ax.ax_tparams = [] && is_axiom ax.ax_kind);
-        (axname, EcSubst.subst_form subst ax.ax_spec)
+        assert (ax.ax_tparams.tyvars = [] && ax.ax_tparams.idxvars = [] && is_axiom ax.ax_kind);
+        (axname, inject_targs opset insts (EcSubst.subst_form subst ax.ax_spec))
     in
       List.map for1 axs
 

src/ecAlgebra.ml

@@ -73,9 +73,12 @@ end
 type eq = form * form
 
 (* -------------------------------------------------------------------- *)
-let rapp r op args =
+let rapp r (op : EcPath.path) args =
   let opty = toarrow (List.map f_ty args) r.r_type in
-    f_app (f_op op [] opty) args r.r_type
+  let ta = r.r_insts in
+  let indices = if ta.EcAst.indices = [] then None else Some ta.EcAst.indices in
+  let tyargs  = if ta.EcAst.types   = [] then None else Some ta.EcAst.types   in
+    f_app (f_op op ?indices ?tyargs opty) args r.r_type
 
 let rzero r = rapp r r.r_zero []
 let rone  r = rapp r r.r_one  []
@@ -157,6 +160,9 @@ type cfieldop = [cringop | `Inv | `Div]
 type cfield   = field * (cfieldop Mp.t)
 
 (* -------------------------------------------------------------------- *)
+(* Recognition is keyed by op path, then checked against the ring's
+   shared instantiation: an occurrence of the same path at OTHER
+   indices/types is not this ring's operator. *)
 let cring_of_ring (r : ring) : cring =
   let cr = [(r.r_zero, `Zero);
             (r.r_one , `One );
@@ -192,9 +198,11 @@ let toring hyps ((r, cr) : cring) (rmap : RState.rstate) (form : form) =
   let rec doit form =
     let o, args = destr_app form in
     match o.f_node with
-    | Fop (op, _) -> begin
+    | Fop (op, ta) -> begin
         match Mp.find_opt op cr with
         | None -> abstract form
+        | Some _ when not (EcDecl.targs_equal ta r.r_insts) ->
+          abstract form
         | Some op -> begin
           match op,args with
           | `Zero, []           -> PEc c0
@@ -255,9 +263,11 @@ let tofield hyps ((r, cr) : cfield) (rmap : RState.rstate) (form : form) =
   let rec doit form =
     let o, args = destr_app form in
     match o.f_node with
-    | Fop(op, _) -> begin
+    | Fop(op, ta) -> begin
         match Mp.find_opt op cr with
         | None -> abstract form
+        | Some _ when not (EcDecl.targs_equal ta r.EcDecl.f_ring.EcDecl.r_insts) ->
+          abstract form
         | Some op -> begin
           match op,args with
           | `Zero, []           -> FEc c0

src/ecAlphaInvHashtbl.ml

@@ -5,8 +5,9 @@
    The hash is invariant under the renaming of bound variables: a bound
    occurrence is hashed by the de-Bruijn *level* of its binder (an
    integer, intrinsically stable) rather than by its name, so
-   alpha-equivalent formulas hash equal. Free variables, operators and
-   types are stable under alpha-renaming and are hashed as-is.
+   alpha-equivalent formulas hash equal. Free variables, operators
+   (with their type and index instantiations) and types are stable
+   under alpha-renaming and are hashed as-is.
 
    The hash traverses the whole formula, but is memoized on the hash-cons
    tag ([f_tag]) of every subformula reached with no binder in scope: each
@@ -78,7 +79,7 @@ let hash_memo (memo : (int, int) Hashtbl.t) (f0 : form) : int =
       combine 3 (pv_hash pv)
     | Fglob (mp, _m) -> combine 4 (id_hash mp)
     | Fop (p, tys) ->
-      combine 5 (combine_list (EcPath.p_hash p) (List.map ty_hash tys))
+      combine 5 (targ_hash (EcPath.p_hash p) tys)
     | Fif (c, t, f) -> combine 6 (combine_list 0 [hash e c; hash e t; hash e f])
     | Fmatch (c, bs, ty) ->
       combine 7 (combine_list (ty_hash ty) (hash e c :: List.map (hash e) bs))