From e3fee052a564dbd0aba649553ca59883cd2fd1be Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Mon, 10 Aug 2026 13:59:11 -0400 Subject: [PATCH 1/3] feat: std::initializer_list specifications + test --- rocq-brick-libstdcpp/proof/dune.inc | 12 ++ .../initializer_list/inc_initializer_list.cpp | 6 + .../proof/initializer_list/pred.v | 6 + .../proof/initializer_list/spec.v | 176 +++++++++++++++++ rocq-brick-libstdcpp/test/dune.inc | 12 ++ .../test/initializer_list/test.cpp | 48 +++++ .../test/initializer_list/test_cpp_proof.v | 181 ++++++++++++++++++ 7 files changed, 441 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/initializer_list/inc_initializer_list.cpp create mode 100644 rocq-brick-libstdcpp/proof/initializer_list/pred.v create mode 100644 rocq-brick-libstdcpp/proof/initializer_list/spec.v create mode 100644 rocq-brick-libstdcpp/test/initializer_list/test.cpp create mode 100644 rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v 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/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..a1f9c6c9 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/initializer_list/pred.v @@ -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. + *) +Require Export skylabs.brick.libstdcpp.initializer_list.spec. 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..ef7842dd --- /dev/null +++ b/rocq-brick-libstdcpp/proof/initializer_list/spec.v @@ -0,0 +1,176 @@ +(* + * 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. + +NES.Begin std. + #[local] Open Scope Z_scope. + + NES.Begin initializer_list. + #[global] Abbreviation N ty := (Ninst "std::initializer_list" [Atype ty]) (only parsing). + #[global] Abbreviation T ty := (Tnamed (N ty)) (only parsing). + + (** + Module [std.initializer_list] provides specifications for + < >>. + + # The spine + + Unlike the other containers here, the "spine" predicate is *not* defined + in this file: it is [initializer_listR], provided by BRiCk itself (see + <>). That is because the *language*, not the + library, creates these objects -- + -- so the rule that builds one ([wp_init_initlist_std]) has to be able to + talk about the result. + + [initializer_listR ty q arrayp n] owns a < >> + referring to a backing array of [n] elements at [arrayp]. It is abstract: + specifies only <>, + <> and <> and declares no data members, and since + <>, every conforming representation is + isomorphic to the pair ([arrayp], [n]). So nothing is lost by declining to + name fields, and neither BRiCk nor these specifications commit to a + particular standard library. + + # 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 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. + + 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. + *) + + (** Ownership of the <> object alone. + + NOTE this is [initializer_listR] from BRiCk; the alias exists so that + client code reads uniformly with [std.vector.spineR] and friends. *) + #[global] Abbreviation spineR ty q arrayp n := (initializer_listR ty q arrayp n) + (only parsing). + + (** 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. A + single fraction, as [std.vector.R_alloc_cap] uses, cannot describe that. *) + #[global] Abbreviation R_at ty q qx arrayp xs := + ( spineR ty q arrayp (lengthN xs) ** + pureR (arrayp |-> 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 := (∃ arrayp, R_at ty q qx arrayp xs)%I + (q in scope cQp_scope, qx in scope cQp_scope). + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + Context (ty : type). + + #[local] Abbreviation initializer_list := (N ty) (only parsing). + #[local] Abbreviation spineR q arrayp n := (initializer_listR ty q arrayp n). + + (** <> + + -- an empty list. The + backing array is empty, so there is no payload. *) + Definition default_ctor := + specify.template.ctor initializer_list [] $ + \this this + \post Exists arrayp, this |-> spineR (cQp.m 1) arrayp 0. + #[global] Hint Opaque default_ctor : sl_opacity. + #[global] Arguments default_ctor : simpl never. + Definition SpecFor_default_ctor := RegisterSpec default_ctor. + #[global] Existing Instance SpecFor_default_ctor. + + (** 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. *) + Definition dtor := + specify.template.dtor initializer_list $ + \this this + \pre{arrayp n} this |-> spineR (cQp.m 1) arrayp n + \post emp. + #[global] Hint Opaque dtor : sl_opacity. + #[global] Arguments dtor : simpl never. + Definition SpecFor_dtor := RegisterSpec dtor. + #[global] Existing Instance SpecFor_dtor. + + (** <> + + *) + Definition size := + let qf := function_qualifiers.Nc in + specify.template.method initializer_list "size" qf Tsize_t [] $ + \this this + \prepost{q arrayp n} this |-> spineR q arrayp n + \post[Vn n] emp. + #[global] Hint Opaque size : sl_opacity. + #[global] Arguments size : simpl never. + Definition SpecFor_size := RegisterSpec size. + #[global] Existing Instance SpecFor_size. + + (** <> + + *) + Definition begin := + let qf := function_qualifiers.Nc in + specify.template.method initializer_list "begin" qf (Tptr (Tconst ty)) [] $ + \this this + \prepost{q arrayp n} this |-> spineR q arrayp n + \post[Vptr arrayp] emp. + #[global] Hint Opaque begin : sl_opacity. + #[global] Arguments begin : simpl never. + Definition SpecFor_begin := RegisterSpec begin. + #[global] Existing Instance SpecFor_begin. + + (** <> + + : one past the last + element, i.e. [begin() + size()]. *) + Definition end_ := + let qf := function_qualifiers.Nc in + specify.template.method initializer_list "end" qf (Tptr (Tconst ty)) [] $ + \this this + \prepost{q arrayp n} this |-> spineR q arrayp n + \post[Vptr (arrayp .[ ty ! Z.of_N n ])] emp. + #[global] Hint Opaque end_ : sl_opacity. + #[global] Arguments end_ : simpl never. + Definition SpecFor_end_ := RegisterSpec end_. + #[global] Existing Instance SpecFor_end_. + + Definition specs := default_ctor ** dtor ** size ** begin ** end_. + #[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..7f63ca3b --- /dev/null +++ b/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v @@ -0,0 +1,181 @@ +(* + * 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.test.initializer_list.test_cpp. + +Require Import skylabs.auto.cpp.prelude.test. + +(** + 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 (templated) [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 arrayp n := + (std.initializer_list.spineR Tint q arrayp n) (only parsing). + #[local] Abbreviation R_at q qx arrayp xs := + (std.initializer_list.R_at Tint q qx arrayp xs) (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 arrayp n} lp |-> spineR q arrayp n + \post[Vn n] emp). + + (** Reading an element needs the payload as well, so this is stated against + the bundled (templated) 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 arrayp x xs} lp |-> R_at q qx arrayp (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 arrayp n} lp |-> spineR q arrayp 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. + + (** [initializer_listR] is abstract, so nothing in a goal determines the + backing array or its length syntactically. [initializer_listR_learn], + registered in auto, recovers both; without it every proof below would + have to instantiate them by hand. + + Only [use_first_ok] below also needs the *fraction* picked for it; it + opts into [UNSAFE_initializer_listR_learn_q] per invocation with + <> rather than registering it for the whole section. The two + compose: the unsafe hint supplies the fraction while the safe one still + supplies the backing array and length. *) + + 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. + (* the qualified name is deliberate: the hint lives in auto's [hints.wp] + alongside the rest of the <> automation, and is + not [Import]ed here. *) + verify_spec. + go using skylabs.auto.cpp.hints.wp.UNSAFE_initializer_listR_learn_q. + (* What is left belongs to [array_sliceR], not [initializer_listR]: 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.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. rewrite /BoxedR; 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. rewrite /BoxedR; 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. + + (** TODO a [specs_ok] gluing lemma, of the form + << + denoteModule source ** |> std.initializer_list.specs Tint + |-- il_size_spec ** il_first_spec ** use_size_spec ** use_first_spec + >> + in the style of [std.vector]'s. [work] does not discharge it as written: + it consumes [std.initializer_list.dtor] once, but all four client + functions need it, and neither destructing the bundle nor boxing it with + [|_|] made it reusable. Each client function above *is* separately + verified against the registered specifications, so this is a packaging + convenience rather than missing coverage. *) + End proofs. +End with_cpp. From 708c6ce5f4ce0ff75360a2fe286f2ef40e19decf Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Mon, 31 Aug 2026 14:47:52 -0400 Subject: [PATCH 2/3] fix: concrete std::initializer_list rep --- .../proof/initializer_list/hints.v | 50 +++++ .../proof/initializer_list/pred.v | 4 + .../proof/initializer_list/spec.v | 173 ++++++++++-------- .../test/initializer_list/test_cpp_proof.v | 74 ++++---- 4 files changed, 178 insertions(+), 123 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/initializer_list/hints.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..9e14e512 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/initializer_list/hints.v @@ -0,0 +1,50 @@ +(* + * 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). + - done. + - 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/pred.v b/rocq-brick-libstdcpp/proof/initializer_list/pred.v index a1f9c6c9..4e843e00 100644 --- a/rocq-brick-libstdcpp/proof/initializer_list/pred.v +++ b/rocq-brick-libstdcpp/proof/initializer_list/pred.v @@ -4,3 +4,7 @@ * 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 index ef7842dd..23708749 100644 --- a/rocq-brick-libstdcpp/proof/initializer_list/spec.v +++ b/rocq-brick-libstdcpp/proof/initializer_list/spec.v @@ -9,42 +9,33 @@ 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. - #[global] Abbreviation N ty := (Ninst "std::initializer_list" [Atype ty]) (only parsing). - #[global] Abbreviation T ty := (Tnamed (N ty)) (only parsing). - (** Module [std.initializer_list] provides specifications for < >>. # The spine - Unlike the other containers here, the "spine" predicate is *not* defined - in this file: it is [initializer_listR], provided by BRiCk itself (see - <>). That is because the *language*, not the - library, creates these objects -- - -- so the rule that builds one ([wp_init_initlist_std]) has to be able to - talk about the result. - - [initializer_listR ty q arrayp n] owns a < >> - referring to a backing array of [n] elements at [arrayp]. It is abstract: - specifies only <>, - <> and <> and declares no data members, and since - <>, every conforming representation is - isomorphic to the pair ([arrayp], [n]). So nothing is lost by declining to - name fields, and neither BRiCk nor these specifications commit to a - particular standard library. + 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 arrayp (lengthN xs) ** + 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 @@ -55,7 +46,8 @@ NES.Begin std. unconditionally would suggest the object owns storage it does not control. LIMITATION: these specifications are *axiomatized*, not proved against - libstdc++'s implementation. + 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 @@ -64,12 +56,26 @@ NES.Begin std. 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 this is [initializer_listR] from BRiCk; the alias exists so that - client code reads uniformly with [std.vector.spineR] and friends. *) - #[global] Abbreviation spineR ty q arrayp n := (initializer_listR ty q arrayp n) - (only parsing). + 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. @@ -77,36 +83,48 @@ NES.Begin std. 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. A - single fraction, as [std.vector.R_alloc_cap] uses, cannot describe that. *) - #[global] Abbreviation R_at ty q qx arrayp xs := - ( spineR ty q arrayp (lengthN xs) ** - pureR (arrayp |-> array_sliceR ty 0 (lengthZ xs) (objR ty qx) xs) )%I + () 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 := (∃ arrayp, R_at ty q qx arrayp xs)%I + #[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 initializer_list := (N ty) (only parsing). - #[local] Abbreviation spineR q arrayp n := (initializer_listR ty q arrayp n). + #[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. *) - Definition default_ctor := - specify.template.ctor initializer_list [] $ - \this this - \post Exists arrayp, this |-> spineR (cQp.m 1) arrayp 0. - #[global] Hint Opaque default_ctor : sl_opacity. - #[global] Arguments default_ctor : simpl never. - Definition SpecFor_default_ctor := RegisterSpec default_ctor. - #[global] Existing Instance SpecFor_default_ctor. + 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. @@ -115,60 +133,53 @@ NES.Begin std. <>, and the enclosing full-expression destroys it. It consumes only the spine -- the backing array is a separate temporary with its own lifetime. *) - Definition dtor := - specify.template.dtor initializer_list $ - \this this - \pre{arrayp n} this |-> spineR (cQp.m 1) arrayp n - \post emp. - #[global] Hint Opaque dtor : sl_opacity. - #[global] Arguments dtor : simpl never. - Definition SpecFor_dtor := RegisterSpec dtor. - #[global] Existing Instance SpecFor_dtor. + 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 + ). (** <> *) - Definition size := - let qf := function_qualifiers.Nc in - specify.template.method initializer_list "size" qf Tsize_t [] $ - \this this - \prepost{q arrayp n} this |-> spineR q arrayp n - \post[Vn n] emp. - #[global] Hint Opaque size : sl_opacity. - #[global] Arguments size : simpl never. - Definition SpecFor_size := RegisterSpec size. - #[global] Existing Instance SpecFor_size. + 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 + ). (** <> *) - Definition begin := - let qf := function_qualifiers.Nc in - specify.template.method initializer_list "begin" qf (Tptr (Tconst ty)) [] $ - \this this - \prepost{q arrayp n} this |-> spineR q arrayp n - \post[Vptr arrayp] emp. - #[global] Hint Opaque begin : sl_opacity. - #[global] Arguments begin : simpl never. - Definition SpecFor_begin := RegisterSpec begin. - #[global] Existing Instance SpecFor_begin. + 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()]. *) - Definition end_ := - let qf := function_qualifiers.Nc in - specify.template.method initializer_list "end" qf (Tptr (Tconst ty)) [] $ - \this this - \prepost{q arrayp n} this |-> spineR q arrayp n - \post[Vptr (arrayp .[ ty ! Z.of_N n ])] emp. - #[global] Hint Opaque end_ : sl_opacity. - #[global] Arguments end_ : simpl never. - Definition SpecFor_end_ := RegisterSpec end_. - #[global] Existing Instance SpecFor_end_. - - Definition specs := default_ctor ** dtor ** size ** begin ** end_. + 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. diff --git a/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v b/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v index 7f63ca3b..9800ebc1 100644 --- a/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v @@ -4,17 +4,20 @@ * 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 (templated) [R_at]. + 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] @@ -36,10 +39,11 @@ Definition BoxedR `{Σ : cpp_logic, σ : genv} (q : cQp.t) (n : N) : Rep := Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - #[local] Abbreviation spineR q arrayp n := - (std.initializer_list.spineR Tint q arrayp n) (only parsing). - #[local] Abbreviation R_at q qx arrayp xs := - (std.initializer_list.R_at Tint q qx arrayp xs) (only parsing). + #[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 ⊧ σ}. @@ -47,14 +51,14 @@ Section with_cpp. (** 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 arrayp n} lp |-> spineR q arrayp n + \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 (templated) form [std.initializer_list.R_at]. *) + 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 arrayp x xs} lp |-> R_at q qx arrayp (x :: xs) + \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 @@ -68,7 +72,7 @@ Section with_cpp. cpp.spec "Boxed::Boxed(std::initializer_list)" as boxed_ctor_spec with (\this this \arg{lp} "l" (Vptr lp) - \prepost{q arrayp n} lp |-> spineR q arrayp n + \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 @@ -90,16 +94,9 @@ Section with_cpp. the arithmetic side conditions the split leaves behind. *) Import normalize.normalize_ptr normalize.only_provable_norm. - (** [initializer_listR] is abstract, so nothing in a goal determines the - backing array or its length syntactically. [initializer_listR_learn], - registered in auto, recovers both; without it every proof below would - have to instantiate them by hand. - - Only [use_first_ok] below also needs the *fraction* picked for it; it - opts into [UNSAFE_initializer_listR_learn_q] per invocation with - <> rather than registering it for the whole section. The two - compose: the unsafe hint supplies the fraction while the safe one still - supplies the backing array and length. *) + (** [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. @@ -130,16 +127,12 @@ Section with_cpp. which is why [R_at] carries the two fractions separately. *) Lemma use_first_ok : verify[ source ] use_first_spec. Proof using MOD. - (* the qualified name is deliberate: the hint lives in auto's [hints.wp] - alongside the rest of the <> automation, and is - not [Import]ed here. *) - verify_spec. - go using skylabs.auto.cpp.hints.wp.UNSAFE_initializer_listR_learn_q. - (* What is left belongs to [array_sliceR], not [initializer_listR]: 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.c 1), 7, [8; 9]. go. + 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. @@ -147,12 +140,12 @@ Section with_cpp. (** 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. rewrite /BoxedR; go. Qed. + 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. rewrite /BoxedR; go. Qed. + Proof using MOD. verify_spec. go. Qed. Definition boxed_dtor_B := [LINK] boxed_dtor_ok. #[local] Hint Resolve boxed_dtor_B : sl_opacity. @@ -166,16 +159,13 @@ Section with_cpp. Definition use_ctor_B := [LINK] use_ctor_ok. #[local] Hint Resolve use_ctor_B : sl_opacity. - (** TODO a [specs_ok] gluing lemma, of the form - << - denoteModule source ** |> std.initializer_list.specs Tint - |-- il_size_spec ** il_first_spec ** use_size_spec ** use_first_spec - >> - in the style of [std.vector]'s. [work] does not discharge it as written: - it consumes [std.initializer_list.dtor] once, but all four client - functions need it, and neither destructing the bundle nor boxing it with - [|_|] made it reusable. Each client function above *is* separately - verified against the registered specifications, so this is a packaging - convenience rather than missing coverage. *) + (** 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. From a375b9ddc9ddd52f44166c7c6d737ec753262620 Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Thu, 10 Sep 2026 15:47:04 -0400 Subject: [PATCH 3/3] fix: repair hint after adding decltype.of_expr check upstream --- rocq-brick-libstdcpp/proof/initializer_list/hints.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/rocq-brick-libstdcpp/proof/initializer_list/hints.v b/rocq-brick-libstdcpp/proof/initializer_list/hints.v index 9e14e512..3912c9be 100644 --- a/rocq-brick-libstdcpp/proof/initializer_list/hints.v +++ b/rocq-brick-libstdcpp/proof/initializer_list/hints.v @@ -38,7 +38,9 @@ Section with_cpp. 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). - - done. + - (* 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.