From cf0047197c39feaebe279ac644c44070f822d34b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 10 Jul 2026 13:22:10 +0200 Subject: [PATCH] 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. --- src/ecCircuits.ml | 2 +- src/ecDecl.ml | 1 + src/ecDecl.mli | 1 + src/ecLowCircuits.ml | 36 ++++++++++++++++++++++++++++++++++- src/ecPrinting.ml | 1 + src/ecScope.ml | 5 +++++ src/ecSubst.ml | 3 ++- tests/circuits/bind_painit.ec | 25 ++++++++++++++++++++++++ theories/datatypes/QFABV.ec | 12 +++++++++++- 9 files changed, 82 insertions(+), 4 deletions(-) create mode 100644 tests/circuits/bind_painit.ec diff --git a/src/ecCircuits.ml b/src/ecCircuits.ml index 3f9dae3d1..d28eb1df4 100644 --- a/src/ecCircuits.ml +++ b/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 diff --git a/src/ecDecl.ml b/src/ecDecl.ml index c2d52cdff..29449d29a 100644 --- a/src/ecDecl.ml +++ b/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) *) diff --git a/src/ecDecl.mli b/src/ecDecl.mli index e1253bfb2..d555d8b9f 100644 --- a/src/ecDecl.mli +++ b/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) *) diff --git a/src/ecLowCircuits.ml b/src/ecLowCircuits.ml index 878b44a5b..429496f8c 100644 --- a/src/ecLowCircuits.ml +++ b/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 *) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index b423e7d24..16c7334fc 100644 --- a/src/ecPrinting.ml +++ b/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" diff --git a/src/ecScope.ml b/src/ecScope.ml index 67fd16c24..65a3fc1b2 100644 --- a/src/ecScope.ml +++ b/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" diff --git a/src/ecSubst.ml b/src/ecSubst.ml index b2fa2836c..4f925709d 100644 --- a/src/ecSubst.ml +++ b/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) diff --git a/tests/circuits/bind_painit.ec b/tests/circuits/bind_painit.ec new file mode 100644 index 000000000..d18d7a28a --- /dev/null +++ b/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. diff --git a/theories/datatypes/QFABV.ec b/theories/datatypes/QFABV.ec index 10cf02a47..943a16e90 100644 --- a/theories/datatypes/QFABV.ec +++ b/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.