feat: std::initializer_list

rocq-brick-libstdcpp/proof/dune.inc

@@ -71,6 +71,18 @@
   	 (with-stderr-to inc_cstring_cpp.v.stderr (run cpp2v -v %{input} -o inc_cstring_cpp.v --no-elaborate --templates=inc_cstring_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_cstring.cpp))
 )
+(subdir initializer_list
+ (rule
+  (targets inc_initializer_list_cpp.v.stderr inc_initializer_list_cpp.v inc_initializer_list_cpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc_initializer_list.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_initializer_list_cpp.v.stderr (run cpp2v -v %{input} -o inc_initializer_list_cpp.v --no-elaborate --templates=inc_initializer_list_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_initializer_list.cpp))
+)
 (subdir iostream
  (rule
   (targets inc_iostream_cpp.v.stderr inc_iostream_cpp.v inc_iostream_cpp_templates.v)

rocq-brick-libstdcpp/proof/initializer_list/hints.v

@@ -0,0 +1,52 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Export skylabs.brick.libstdcpp.initializer_list.spec.
+
+Import linearity.
+
+(**
+    Automation for <<std::initializer_list>> construction.
+
+    [wp_init_initlist_std] in BRiCk reduces [Einitlist_std] to a call of the
+    constructor named by [std_initlist_ctor]; this hint applies that reduction so
+    that [go] can then use the constructor's specification. It lives here rather
+    than in <<auto>> because the constructor it lands on is the one *this*
+    package specifies -- which is also what lets the availability side condition
+    discharge by reduction: libstdc++ declares that constructor.
+ *)
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Section with_resolve.
+    Variables (tu : translation_unit) (ρ : region).
+
+    #[local] Abbreviation wp_init := (wp_init tu ρ).
+
+    Lemma wp_init_initlist_std_hint ty cls aety n (base : ptr) backing Q :
+      ((decompose_type ty).2, drop_qualifiers (drop_reference (type_of backing)))
+        =[Vm]=> (Tnamed cls, Tarray aety n) ->
+      std_initlist_ctor_available tu cls aety =[Vm]=> true ->
+      wp_init ty base
+        (Econstructor (std_initlist_ctor cls aety)
+           [Ecast Carray2ptr backing; Eint (Z.of_N n) Tsize_t] ty) Q
+      |-- wp_init ty base (Einitlist_std backing ty) Q.
+    Proof.
+      rewrite !RedEq_eq_iff => Heq Havail.
+      case: Heq => Hcls Harr.
+      rewrite -(wp_init_initlist_std tu ρ cls base (decompose_type ty).1 ty backing aety n Q).
+      - (* The typing side condition holds by reduction: [decltype.of_expr]
+           takes [Econstructor _ _ ty] to [ty]. *)
+        cbv zeta. by rewrite only_provable_True// left_id.
+      - by rewrite {1}(surjective_pairing (decompose_type ty)) Hcls.
+      - exact: Harr.
+      - exact: Havail.
+    Qed.
+    Definition wp_init_initlist_std_hint_B := [BWD] wp_init_initlist_std_hint.
+  End with_resolve.
+End with_cpp.
+
+#[export] Hint Resolve wp_init_initlist_std_hint_B | 150 : db_skylabs_wp.

rocq-brick-libstdcpp/proof/initializer_list/inc_initializer_list.cpp

@@ -0,0 +1,6 @@
+/**
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+#include <initializer_list>

rocq-brick-libstdcpp/proof/initializer_list/pred.v

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Export skylabs.brick.libstdcpp.initializer_list.spec.
+(* The construction hint only fires on [Einitlist_std], so it is inert unless a
+   proof actually builds an <<std::initializer_list>>; exporting it here saves
+   every such client from importing it separately. *)
+Require Export skylabs.brick.libstdcpp.initializer_list.hints.

rocq-brick-libstdcpp/proof/initializer_list/spec.v

@@ -0,0 +1,187 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.auto.cpp.spec.
+Require Export skylabs.cpp.slice.
+
+Require Import skylabs.cpp.spec.concepts.
+
+Require Import skylabs.brick.libstdcpp.initializer_list.inc_initializer_list_cpp.
+Require Import skylabs.brick.libstdcpp.initializer_list.inc_initializer_list_cpp_templates.
+
+NES.Begin std.
+  #[local] Open Scope Z_scope.
+
+  NES.Begin initializer_list.
+    (**
+        Module [std.initializer_list] provides specifications for
+        <<std::initializer_list<ty> >>.
+
+        # The spine
+
+        A <<std::initializer_list>> refers to a backing array
+        (<https://eel.is/c++draft/dcl.init.list#5>) that the *language*, not the
+        library, creates: [Einitlist_std] in BRiCk builds one by calling the
+        constructor specified below.
+
+        [spineR] owns the object itself. Its model [M] is the pair the three
+        accessors pin down -- <<begin()>>, <<end()>> and <<size()>>, with
+        <<end() - begin() == size()>>.
+
+        # The payload
+
+        Like [std.vector], the spine owns only the shape. The elements live at
+        [arrayp] and are owned separately, via [array_sliceR]:
+        <<
+          p |-> std.initializer_list.spineR ty q (Mk arrayp (lengthN xs)) **
+          arrayp |-> array_sliceR ty 0 (lengthZ xs) Rpayload xs
+        >>
+        [R_at] and [R] below bundle the two for convenience. Keeping them
+        separable matters more here than for other containers, because a
+        <<std::initializer_list>> is a *view*: the backing array is a temporary
+        whose storage has automatic duration tied to the enclosing
+        full-expression, not to the <<initializer_list>> object. Bundling
+        unconditionally would suggest the object owns storage it does not control.
+
+        LIMITATION: these specifications are *axiomatized*, not proved against
+          libstdc++'s implementation, even though [spineR] is stated in terms of
+          its fields.
+
+        LIMITATION: BRiCk does not support the lifetime-extended form
+          <<std::initializer_list<int> il = {1,2,3};>>, which needs scope-extruded
+          temporaries. Uses where the backing array dies with the enclosing
+          full-expression -- passing a braced-init-list to a function, or to a
+          constructor taking an <<initializer_list>> -- are supported.
+     *)
+
+    (** The backing array and its length: the information content
+        <<begin()>>/<<end()>>/<<size()>> pin down.
+
+        NOTE declared before the [N] abbreviation below, which would otherwise
+        shadow the [N] of [len]. *)
+    Record M : Type := Mk { arrayp : ptr ; len : N }.
+
+    #[global] Abbreviation N ty := (Ninst "std::initializer_list" [Atype ty]) (only parsing).
+    #[global] Abbreviation T ty := (Tnamed (N ty)) (only parsing).
+
+    (** Ownership of the <<std::initializer_list>> object alone.
+
+        NOTE the field names are libstdc++'s; this package specifies that
+        implementation. Nothing outside this definition depends on them. *)
+    sl.lock
+    Definition spineR `{Σ : cpp_logic, σ : genv} (ty : type) (q : cQp.t) (m : M) : Rep :=
+      structR (N ty) q **
+      _field (N ty .:: Nid "_M_array") |-> ptrR<Tconst ty> q m.(arrayp) **
+      _field (N ty .:: Nid "_M_len") |-> primR Tsize_t q (Vn m.(len)).
+    #[only(cfracsplittable,type_ptr,lazy_unfold(global))] derive spineR.
+
+    (** Spine and payload together, for a known backing array.
+
+        NOTE the spine and the payload carry *separate* fractions. They are
+        genuinely different resources: the <<initializer_list>> object may well
+        be mutable (a freshly materialized temporary is), while the backing
+        array is an array of <<const E>>
+        (<https://eel.is/c++draft/dcl.init.list#5>) and so is owned constly. *)
+    #[global] Abbreviation R_at ty q qx p xs :=
+      ( spineR ty q (Mk p (lengthN xs)) **
+        pureR (p |-> array_sliceR ty 0 (lengthZ xs) (objR ty qx) xs) )%I
+      (q in scope cQp_scope, qx in scope cQp_scope).
+
+    (** Spine and payload together, hiding the backing array. *)
+    #[global] Abbreviation R ty q qx xs := (∃ p, R_at ty q qx p xs)%I
+      (q in scope cQp_scope, qx in scope cQp_scope).
+
+    Section with_cpp.
+      Context `{Σ : cpp_logic, σ : genv}.
+      Context (ty : type).
+
+      #[local] Abbreviation spineR := (spineR ty).
+
+      #[global] Instance: LearnEqF1 spineR := ltac:(solve_learnable).
+
+      (** <<constexpr initializer_list(const E*, size_t) noexcept;>>
+
+          The constructor the *compiler* calls for a braced-init-list; it is
+          private, and [wp_init_initlist_std] in BRiCk reduces [Einitlist_std] to
+          a call of it. See [std_initlist_ctor] there. *)
+      cpp.spec "std::initializer_list<$ty>::initializer_list(const $ty*, unsigned long)"
+        as ctor from source templates templates (
+        \\with
+        \this this
+        \arg{p} "" (Vptr p)
+        \arg{n} "" (Vn n)
+        \post this |-> spineR (cQp.m 1) (Mk p n)
+      ).
+
+      (** <<constexpr initializer_list() noexcept;>>
+
+          <https://eel.is/c++draft/support.initlist.cons> -- an empty list. The
+          backing array is empty, so there is no payload. *)
+      cpp.spec "std::initializer_list<$ty>::initializer_list()"
+        as default_ctor from source templates templates (
+        \\with
+        \this this
+        \post Exists p, this |-> spineR (cQp.m 1) (Mk p 0)
+      ).
+
+      (** The (trivial) destructor.
+
+          NOTE this is needed even though <<std::initializer_list>> owns
+          nothing: a braced-init-list passed to a function creates a temporary
+          <<initializer_list>>, and the enclosing full-expression destroys it.
+          It consumes only the spine -- the backing array is a separate
+          temporary with its own lifetime. *)
+      cpp.spec "std::initializer_list<$ty>::~initializer_list()"
+        as dtor from source templates templates (
+        \\with
+        \this this
+        \pre{m} this |-> spineR (cQp.m 1) m
+        \post emp
+      ).
+
+      (** <<constexpr size_t size() const noexcept;>>
+
+          <https://eel.is/c++draft/support.initlist.access> *)
+      cpp.spec "std::initializer_list<$ty>::size() const"
+        as size from source templates templates (
+        \\with
+        \this this
+        \prepost{q m} this |-> spineR q m
+        \post[Vn m.(len)] emp
+      ).
+
+      (** <<constexpr const E* begin() const noexcept;>>
+
+          <https://eel.is/c++draft/support.initlist.access> *)
+      cpp.spec "std::initializer_list<$ty>::begin() const"
+        as begin from source templates templates (
+        \\with
+        \this this
+        \prepost{q m} this |-> spineR q m
+        \post[Vptr m.(arrayp)] emp
+      ).
+
+      (** <<constexpr const E* end() const noexcept;>>
+
+          <https://eel.is/c++draft/support.initlist.access>: one past the last
+          element, i.e. [begin() + size()]. *)
+      cpp.spec "std::initializer_list<$ty>::end() const"
+        as end_ from source templates templates (
+        \\with
+        \this this
+        \prepost{q m} this |-> spineR q m
+        \post[Vptr (m.(arrayp) .[ ty ! Z.of_N m.(len) ])] emp
+      ).
+
+      (** NOTE templated [cpp.spec]s are indexed by the translation unit they
+          were resolved against, so this bundle is too: clients write
+          <<std.initializer_list.specs ty source>>. *)
+      Definition specs (tu : translation_unit) :=
+        ctor tu ** default_ctor tu ** dtor tu ** size tu ** begin tu ** end_ tu.
+      #[global] Hint Opaque specs : typeclass_instances sl_opacity.
+      #[only(knowledge)] derive specs.
+    End with_cpp.
+  NES.End initializer_list.
+NES.End std.

rocq-brick-libstdcpp/test/dune.inc

@@ -215,6 +215,18 @@
   	 (with-stderr-to N6_print_sizeof_cpp.v.stderr (run cpp2v -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps N6_print_sizeof.cpp))
 )
+(subdir initializer_list
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v)
+  (alias test_ast)
+  (deps
+   (:input test.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir memory
  (rule
   (targets test_cpp.v.stderr test_cpp.v)

rocq-brick-libstdcpp/test/initializer_list/test.cpp

@@ -0,0 +1,48 @@
+/**
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+#include <initializer_list>
+
+/** Reads only the spine. */
+unsigned long
+il_size(std::initializer_list<int> l) {
+    return l.size();
+}
+
+/** Reads the payload, through the templated interface. */
+int
+il_first(std::initializer_list<int> l) {
+    return *l.begin();
+}
+
+/** Constructs a <<std::initializer_list>> from a braced-init-list, i.e.
+    exercises clang's [CXXStdInitializerListExpr] and BRiCk's
+    [wp_init_initlist_std]. The backing array is a temporary that dies with the
+    enclosing full-expression, which is the form BRiCk supports. */
+unsigned long
+use_size() {
+    return il_size({1, 2, 3});
+}
+
+int
+use_first() {
+    return il_first({7, 8, 9});
+}
+
+/** A class with an <<initializer_list>> constructor. This is the other way a
+    braced-init-list reaches [Einitlist_std]: as the argument of a constructor
+    rather than of a function. The body is deliberately trivial -- what is under
+    test is that *building* such an object works. */
+struct Boxed {
+    unsigned long n;
+    Boxed(std::initializer_list<int> l) : n(l.size()) {}
+};
+
+/** Brace-initialization of a class with an <<initializer_list>> constructor. */
+unsigned long
+use_ctor() {
+    Boxed b{1, 2, 3};
+    return b.n;
+}