feat(circuit): polymorphic array init binding kind (painit)

A raw polymorphic `Array.init` (e.g. from `subarray256 x i =
Array256.init (fun k => x.[256*i+k])`) had no circuit binding: only the
monomorphic `ainit` wrapper is bindable, since `bind op`/`ainit` fixes the
element width at bind time. So a spec built on `Array.init` fell into the
reduce-on-demand fallback -- full reduction per element access -- which
could take minutes to translate a single postcondition.

Add a `painit` bv-operator kind that binds an array `init` BY PATH while
leaving the element lane-width polymorphic; the width is resolved from the
concrete components when the operator is translated at a concrete element
type.

Author: strub

src/ecCircuits.ml

@@ -383,7 +383,7 @@ open CircuitSpec
 let bvop_is_parametric (op : EcDecl.crb_bvoperator) : bool =
   match op.kind with
   | `ASliceGet _ | `ASliceSet _ | `Extract _ | `Insert _ | `Map _ | `Get _
-  | `AInit _ | `Init _ ->
+  | `AInit _ | `PAInit _ | `Init _ ->
     true
   | _ -> false
 

src/ecDecl.ml

@@ -450,6 +450,7 @@ type bv_opkind = [
   | `Init     of binding_size (* size_out *)
   | `Get      of binding_size (* size_in *)
   | `AInit    of binding_size * binding_size (* arr_len + size_out *)
+  | `PAInit   of binding_size (* arr_len; element size resolved at use (polymorphic) *)
   | `Map      of binding_size * binding_size * binding_size (* size_in + size_out + arr_size *)
   | `A2B      of (binding_size * binding_size) * binding_size (* (arr_len, elem_sz), out_size *)
   | `B2A      of binding_size * (binding_size * binding_size) (* size in, (arr_len, elem_sz)  *)

src/ecDecl.mli

@@ -284,6 +284,7 @@ type bv_opkind = [
   | `Init     of binding_size (* size_out *)
   | `Get      of binding_size (* size_in *)
   | `AInit    of binding_size * binding_size (* arr_len + size_out *)
+  | `PAInit   of binding_size (* arr_len; element size resolved at use (polymorphic) *)
   | `Map      of binding_size * binding_size * binding_size (* size_in + size_out + arr_size *)
   | `A2B      of (binding_size * binding_size) * binding_size (* (arr_len, elem_sz), out_size *)
   | `B2A      of binding_size * (binding_size * binding_size) (* size in, (arr_len, elem_sz)  *)

src/ecLowCircuits.ml

@@ -1224,6 +1224,40 @@ module BVOps = struct
       (* Should be caught by EC typechecking + binding correctness *)
       | _ -> assert false
     end
+    | `PAInit (_, Some n) -> begin
+      match args with
+      | [`Init init_f] ->
+        let cs = List.init n init_f in
+        let cinputs = List.map (fun (c : circuit) -> c.inputs) cs in
+        let regs =
+          List.map
+            (fun (c : circuit) ->
+              match c.cval with
+              | {type_ = CBitstring _; reg = r} -> r
+              (* Should be caught by EC typechecking + binding correctness *)
+              | _ -> assert false)
+            cs
+        in
+        (* The element width is not fixed by the binding (this init is
+           polymorphic in the element type): read it off the components,
+           which are concrete at the use site. *)
+        let w_o =
+          match regs with r :: _ -> C.Reg.length r | [] -> assert false
+        in
+        if not (List.for_all (fun r -> C.Reg.length r = w_o) regs) then
+          assert false;
+        (* Inputs should be uniform across components after mapping *)
+        if not (List.for_all (( = ) (List.hd cinputs)) cinputs) then
+          assert false;
+        let inputs = List.hd cinputs in
+        {
+          cval =
+            {type_ = CArray {width = w_o; count = n}; reg = C.Reg.concat regs};
+          inputs;
+        }
+      (* Should be caught by EC typechecking + binding correctness *)
+      | _ -> assert false
+    end
     | `Init (_, Some w) -> begin
       match args with
       | [`Init init_f] ->
@@ -1323,7 +1357,7 @@ module BVOps = struct
     | {
         kind =
           ( `ASliceGet _ | `ASliceSet _ | `Extract _ | `Insert _ | `Map _
-          | `AInit _ | `Get _ | `Init _ );
+          | `AInit _ | `PAInit _ | `Get _ | `Init _ );
       }
     | _ ->
       assert false (* Should be guarded by call to op_is_bvop *)

src/ecPrinting.ml

@@ -3923,6 +3923,7 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
         | `Init     _            -> "init"
         | `Get      _            -> "get"
         | `AInit    _            -> "ainit"
+        | `PAInit   _            -> "painit"
         | `Extend  (_, _, false) -> "zextend"
         | `Extend  (_, _, true ) -> "sextend"
         | `Extract  _            -> "extract"

src/ecScope.ml

@@ -2961,6 +2961,11 @@ module Circuit = struct
 
       | "ainit" -> (fun sz -> `AInit (as_seq2 (sz |> List.rev))), [`BV None; `A], "AInit"
 
+      (* Polymorphic array [init]: only the array is bound; the element
+         width is left free and resolved when translated at a concrete
+         element type. *)
+      | "painit" -> (fun sz -> `PAInit (as_seq1 sz)), [`A], "PAInit"
+
       | "shls"  -> 
           let mk sz = let sz1, sz2 = as_seq2 sz in `Shls (sz1, sz2) in
           mk, [`BV None; `BV None], "SHLS"

src/ecSubst.ml

@@ -1054,7 +1054,8 @@ let subst_bv_opkind ?(red: (form -> int option) option) (s: subst) (opk: bv_opki
   | `And s -> `And (ssize s) 
   | `Extract (s1, s2, aligned) -> `Extract (ssize s1, ssize s2, aligned) 
   | `Map (s1, s2, s3) -> `Map (ssize s1, ssize s2, ssize s3) 
-  | `AInit (s1, s2) -> `AInit (ssize s1, ssize s2) 
+  | `AInit (s1, s2) -> `AInit (ssize s1, ssize s2)
+  | `PAInit s -> `PAInit (ssize s)
   | `Sub s -> `Sub (ssize s) 
   | `Get s -> `Get (ssize s) 
   | `Ror s -> `Ror (ssize s) 

tests/circuits/bind_painit.ec

@@ -0,0 +1,25 @@
+(* Polymorphic array [init] binding ("painit"). *)
+
+require import AllCore List QFABV.
+
+theory Array8.
+type 'a t.
+
+op tolist : 'a t -> 'a list.
+op oflist : 'a -> 'a list -> 'a t.
+op "_.[_]" : 'a t -> int -> 'a.
+op "_.[_<-_]" : 'a t -> int -> 'a -> 'a t.
+op init : (int -> 'a) -> 'a t.
+
+end Array8.
+
+bind array Array8."_.[_]" Array8."_.[_<-_]" Array8.tolist Array8.oflist Array8.t 8.
+realize gt0_size by auto.
+realize tolistP by admit.
+realize oflistP by admit.
+realize eqP by admit.
+realize get_setP by admit.
+realize get_out by admit.
+
+bind op [Array8.t] Array8.init "painit".
+realize bvpainitP by admit.

theories/datatypes/QFABV.ec

@@ -516,10 +516,20 @@ theory BVOperators.
 
     op bvainit : (int -> BV.bv) -> BV.bv A.t.
 
-    axiom bvainitP (f : int -> BV.bv) : 
+    axiom bvainitP (f : int -> BV.bv) :
       A.to_list (bvainit f) = List.mkseq (fun i => (f i)) A.size.
   end BVAInit.
 
+  (* ------------------------------------------------------------------ *)
+  abstract theory BVPAInit.
+    clone A.
+
+    op bvpainit ['a] : (int -> 'a) -> 'a A.t.
+
+    axiom bvpainitP ['a] (f : int -> 'a) :
+      A.to_list (bvpainit f) = List.mkseq (fun i => (f i)) A.size.
+  end BVPAInit.
+
   (* ------------------------------------------------------------------ *)
   abstract theory BVMap.
     clone BV as BV1.