diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index 14a82e4b..636d04f6 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/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) diff --git a/rocq-brick-libstdcpp/proof/initializer_list/hints.v b/rocq-brick-libstdcpp/proof/initializer_list/hints.v new file mode 100644 index 00000000..3912c9be --- /dev/null +++ b/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 <> 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 <> 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. diff --git a/rocq-brick-libstdcpp/proof/initializer_list/inc_initializer_list.cpp b/rocq-brick-libstdcpp/proof/initializer_list/inc_initializer_list.cpp new file mode 100644 index 00000000..aa942bc3 --- /dev/null +++ b/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 diff --git a/rocq-brick-libstdcpp/proof/initializer_list/pred.v b/rocq-brick-libstdcpp/proof/initializer_list/pred.v new file mode 100644 index 00000000..4e843e00 --- /dev/null +++ b/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 <>; exporting it here saves + every such client from importing it separately. *) +Require Export skylabs.brick.libstdcpp.initializer_list.hints. diff --git a/rocq-brick-libstdcpp/proof/initializer_list/spec.v b/rocq-brick-libstdcpp/proof/initializer_list/spec.v new file mode 100644 index 00000000..23708749 --- /dev/null +++ b/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 + < >>. + + # The spine + + A <> refers to a backing array + () 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 -- <>, <> and <>, with + <>. + + # 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 + <> is a *view*: the backing array is a temporary + whose storage has automatic duration tied to the enclosing + full-expression, not to the <> 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 + < 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 <> -- are supported. + *) + + (** The backing array and its length: the information content + <>/<>/<> 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 <> 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 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 <> object may well + be mutable (a freshly materialized temporary is), while the backing + array is an array of <> + () 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). + + (** <> + + 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) + ). + + (** <> + + -- 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 <> owns + nothing: a braced-init-list passed to a function creates a temporary + <>, 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 + ). + + (** <> + + *) + 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 + ). + + (** <> + + *) + 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 + ). + + (** <> + + : 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 + <>. *) + 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. diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 57dae3f1..6b620881 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/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) diff --git a/rocq-brick-libstdcpp/test/initializer_list/test.cpp b/rocq-brick-libstdcpp/test/initializer_list/test.cpp new file mode 100644 index 00000000..37c5781d --- /dev/null +++ b/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 + +/** Reads only the spine. */ +unsigned long +il_size(std::initializer_list l) { + return l.size(); +} + +/** Reads the payload, through the templated interface. */ +int +il_first(std::initializer_list l) { + return *l.begin(); +} + +/** Constructs a <> 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 <> 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 l) : n(l.size()) {} +}; + +/** Brace-initialization of a class with an <> constructor. */ +unsigned long +use_ctor() { + Boxed b{1, 2, 3}; + return b.n; +} diff --git a/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v b/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v new file mode 100644 index 00000000..9800ebc1 --- /dev/null +++ b/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v @@ -0,0 +1,171 @@ +(* + * 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.brick.libstdcpp.initializer_list.spec. +Require Import skylabs.brick.libstdcpp.initializer_list.hints. +Require Import skylabs.brick.libstdcpp.test.initializer_list.test_cpp. + +Require Import skylabs.auto.cpp.prelude.test. + +Import linearity. + +(** + A client of the <> specifications in + ../../proof/initializer_list/spec.v. + + [il_size] and [il_first] consume an <> and are + verified against those (axiomatized) specifications -- [il_size] against the + spine alone, [il_first] against the bundled [R_at]. + + [use_size] and [use_first] *construct* one from a braced-init-list, so + verifying them additionally exercises clang's [CXXStdInitializerListExpr] + and BRiCk's [wp_init_initlist_std]. + + [use_ctor] constructs one in the other position a braced-init-list can occupy + -- the argument of a *constructor* taking an <>, i.e. + <> -- so that building such an object is covered too. + *) + +(** <> has a single field and no user-declared destructor, so its + representation is just that field. *) +sl.lock +Definition BoxedR `{Σ : cpp_logic, σ : genv} (q : cQp.t) (n : N) : Rep := + structR "Boxed" q ** + _field "Boxed::n" |-> primR Tsize_t q (Vn n). +#[only(cfracsplittable,type_ptr,lazy_unfold(global))] derive BoxedR. + +Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + #[local] Abbreviation spineR q m := + (std.initializer_list.spineR Tint q m) (only parsing). + #[local] Abbreviation R_at q qx p xs := + (std.initializer_list.R_at Tint q qx p xs) (only parsing). + #[local] Abbreviation Mk := std.initializer_list.Mk (only parsing). + + Section specs. + Context `{MOD : test_cpp.source ⊧ σ}. + + (** Only the spine is needed to read the size. *) + cpp.spec "il_size(std::initializer_list)" as il_size_spec with + (\arg{lp} "l" (Vptr lp) + \prepost{q p n} lp |-> spineR q (Mk p n) + \post[Vn n] emp). + + (** Reading an element needs the payload as well, so this is stated against + the bundled form [std.initializer_list.R_at]. *) + cpp.spec "il_first(std::initializer_list)" as il_first_spec with + (\arg{lp} "l" (Vptr lp) + \prepost{q qx p x xs} lp |-> R_at q qx p (x :: xs) + \post[Vint x] emp). + + cpp.spec "use_size()" as use_size_spec with + (\post[Vn 3] emp). + + cpp.spec "use_first()" as use_first_spec with + (\post[Vint 7] emp). + + (** The constructor consumes the spine of its argument and records the + length. It needs only the spine, like [il_size]. *) + cpp.spec "Boxed::Boxed(std::initializer_list)" as boxed_ctor_spec with + (\this this + \arg{lp} "l" (Vptr lp) + \prepost{q p n} lp |-> spineR q (Mk p n) + \post this |-> BoxedR 1$m n). + + (** <> is trivially destructible, but <> still goes out of scope in + [use_ctor], so the implicit destructor needs a specification. *) + cpp.spec "Boxed::~Boxed()" as boxed_dtor_spec with + (\this this + \pre{n} this |-> BoxedR 1$m n + \post emp). + + cpp.spec "use_ctor()" as use_ctor_spec with + (\post[Vn 3] emp). + End specs. + + Section proofs. + Context `{MOD : test_cpp.source ⊧ σ}. + + (** [normalize_ptr] reduces <

> to [p], which is needed after + splitting element 0 off an [array_sliceR]; [only_provable_norm] tidies + the arithmetic side conditions the split leaves behind. *) + Import normalize.normalize_ptr normalize.only_provable_norm. + + (** [spineR]'s model is recovered by the [LearnEqF1] instance registered + alongside it, so the proofs below do not have to instantiate the backing + array or its length by hand. *) + + Lemma il_size_ok : verify[ source ] il_size_spec. + Proof using MOD. verify_spec. go. Qed. + Definition il_size_B := [LINK] il_size_ok. + #[local] Hint Resolve il_size_B : sl_opacity. + + (** [array_sliceR_cons] is deliberately not a registered hint -- automation + cannot guess where to split a slice -- so element 0 is split off by + hand. [array_sliceR_singleton] *is* registered, so [go] finishes. *) + Lemma il_first_ok : verify[ source ] il_first_spec. + Proof using MOD. + verify_spec. go. rewrite array_sliceR_cons offset_ptr_sub_0 //. go. + (* give the payload back: the same split, run backwards *) + rewrite array_sliceR_cons offset_ptr_sub_0 //. go. + Qed. + Definition il_first_B := [LINK] il_first_ok. + #[local] Hint Resolve il_first_B : sl_opacity. + + Lemma use_size_ok : verify[ source ] use_size_spec. + Proof using MOD. + verify_spec. go. + Qed. + Definition use_size_B := [LINK] use_size_ok. + #[local] Hint Resolve use_size_B : sl_opacity. + + (** Construct a list *and* read an element of it: the spine is a freshly + materialized (mutable) temporary while the backing array is <>, + which is why [R_at] carries the two fractions separately. *) + Lemma use_first_ok : verify[ source ] use_first_spec. + Proof using MOD. + verify_spec. go. + (* What is left belongs to [array_sliceR], not [spineR]: the payload's + fraction and the element split. [pick_frac] does not discharge it (the + bound [lengthZ xs + 1] needs [xs] first), and no cons-splitting hint is + registered, so these are supplied by hand. *) + iExists (cQp.m 1), (cQp.c 1), 7, [8; 9]. go. + Qed. + Definition use_first_B := [LINK] use_first_ok. + #[local] Hint Resolve use_first_B : sl_opacity. + + (** The constructor body is just <>, so this is [il_size_ok] + with the result stored into a field. *) + Lemma boxed_ctor_ok : verify[ source ] boxed_ctor_spec. + Proof using MOD. verify_spec. go. Qed. + Definition boxed_ctor_B := [LINK] boxed_ctor_ok. + #[local] Hint Resolve boxed_ctor_B : sl_opacity. + + Lemma boxed_dtor_ok : verify[ source ] boxed_dtor_spec. + Proof using MOD. verify_spec. go. Qed. + Definition boxed_dtor_B := [LINK] boxed_dtor_ok. + #[local] Hint Resolve boxed_dtor_B : sl_opacity. + + (** <>: the braced-init-list becomes the backing array of + an <> temporary, which is then the constructor's + argument. *) + Lemma use_ctor_ok : verify[ source ] use_ctor_spec. + Proof using MOD. + verify_spec. go. + Qed. + Definition use_ctor_B := [LINK] use_ctor_ok. + #[local] Hint Resolve use_ctor_B : sl_opacity. + + (** The client specifications, discharged from the <> + specifications they depend on. *) + Lemma specs_ok : + denoteModule source ** + ▷ std.initializer_list.specs Tint source + |-- il_size_spec ** il_first_spec ** use_size_spec ** use_first_spec ** + boxed_ctor_spec ** boxed_dtor_spec ** use_ctor_spec. + Proof using MOD. rewrite /std.initializer_list.specs. work. Qed. + End proofs. +End with_cpp.