Integer-indexed types

src/ecAlgTactic.ml

@@ -30,7 +30,15 @@ module Axioms = struct
   let cN    = "Cn"
   let cP    = "Cp"
 
-  let core_add  = ["oner_neq0"; "addr0"; "addrA"; "addrC";]
+  (* [oner_neq0] is not a REQUIRED ring obligation: 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. It stays OPTIONAL for backward compatibility: a
+     [proof oner_neq0 by ...] clause is accepted and checked
+     (downstream instances, e.g. Jasmin's JWord, discharge it).
+     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 +47,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 +88,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 +121,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,16 +156,24 @@ 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
 
   let getr env cr axs = get (`Ring  cr) env axs
   let getf env cr axs = get (`Field cr) env axs
 
+  let ring_axioms_1neq0 env (cr : ring) = getr env cr ["oner_neq0"]
+
   let ring_axioms env (cr : ring) =
     let axcore =
       match cr.r_kind with
@@ -171,6 +214,7 @@ let ring_symbols  = Axioms.ring_symbols
 let field_symbols = Axioms.field_symbols
 
 let ring_axioms  = Axioms.ring_axioms
+let ring_axioms_1neq0 = Axioms.ring_axioms_1neq0
 let field_axioms = Axioms.field_axioms
 
 (* -------------------------------------------------------------------- *)

src/ecAlgTactic.mli

@@ -14,6 +14,9 @@ val ring_symbols  : EcEnv.env -> EcDecl.rkind -> ty -> (symbol * (bool * ty)) li
 val field_symbols : EcEnv.env -> ty -> (symbol * (bool * ty)) list
 
 val ring_axioms  : EcEnv.env -> ring  -> (symbol * form) list
+(* the optional non-triviality obligation, emitted only when the
+   instance supplies a proof for it (backward compatibility) *)
+val ring_axioms_1neq0 : EcEnv.env -> ring -> (symbol * form) list
 val field_axioms : EcEnv.env -> field -> (symbol * form) list
 
 (* -------------------------------------------------------------------- *)

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))