diff --git a/spec-review/optional-unsigned-char/1-scope.md b/spec-review/optional-unsigned-char/1-scope.md new file mode 100644 index 00000000..fc77272a --- /dev/null +++ b/spec-review/optional-unsigned-char/1-scope.md @@ -0,0 +1,46 @@ +# Review scope + +This review covers only `std::optional` as implemented by +libstdc++ 12. It does not propose a generic `std::optional` specification. + +## Operation contracts + +The specification registers six operations: + +1. construction from `std::nullopt_t` produces a disengaged optional; +2. construction from an `unsigned char` rvalue copies the source byte and + preserves the source object; +3. construction from an `unsigned char` lvalue copies the source byte and + preserves the source object; +4. `has_value() const` reports engagement without changing the object; +5. `operator*() const &` requires engagement and returns a reference to the + byte contained in that optional; and +6. destruction consumes the optional and ends ownership of its contained byte. + +The abstract model is either `empty` or `engaged byte`, where `byte` is the +mathematical value represented by an `unsigned char`. + +## Selected clients + +### Positive: `arbitrary_byte_roundtrip` + +Constructs const optionals containing low and high nonzero byte values, checks +engagement, and reads the stored values. This is the ordinary positive example. + +### Positive: `rvalue_snapshot_not_alias` + +Constructs an optional from an rvalue source, changes the source afterward, and +checks that the optional retained the original value. This exercises source +preservation and independent storage. + +### Negative: `reference_outlives_optional` + +Keeps a pointer to the contained byte after the optional has been destroyed and +then attempts to read through it. Its proof is intentionally unable to close: +the destructor consumes the representation that justified access to the byte. + +## Out of scope + +This packet does not cover a generic element type, optional-to-optional copy or +move construction, assignment, `reset`, `emplace`, exceptions, comparisons, or +monadic operations. diff --git a/spec-review/optional-unsigned-char/README.md b/spec-review/optional-unsigned-char/README.md new file mode 100644 index 00000000..84bb156e --- /dev/null +++ b/spec-review/optional-unsigned-char/README.md @@ -0,0 +1,74 @@ +# Review artifacts — `std::optional` + +This packet presents a small, representative slice of one +specification-pipeline run for focused source review. + +Everything is under `spec-review/` and is wired into no Dune rule, so it cannot +affect `rocq-brick-libstdcpp/`. + +This packet deliberately contains the complete semantic specification but only +three of the run's client/proof pairs. The proof-automation implementation, +remaining clients, proof obligations, mutations, and execution records are +available separately; they are not needed for the initial judgement requested +here. + +## Reading order + +| Path | What to review | +|---|---| +| `1-scope.md` | The exact API surface and the three selected examples | +| `spec/model.v` | The abstract empty/engaged state | +| `spec/pred.v` | The concrete libstdc++ 12 representation predicate | +| `spec/spec.v` | The six registered operation contracts | +| `spec/inc_optional.cpp` | The concrete template instantiations used for binding generation | +| `clients/positive/` | Two clients whose verification must succeed | +| `clients/negative/` | One invalid client whose verification must fail | +| `proofs/positive/` | The two corresponding proofs ending in `Qed.` | +| `proofs/negative/` | The expected-failure proof committed with `Fail Qed.` and `Abort.` | + +There are ten substantive source files: four library files, three C++ +clients, and three Rocq proofs. + +## What feedback would help + +The requested judgement is narrow: + +- Is the abstract state and concrete representation the right shape for this + specialization? +- Do the six contracts express the intended ownership, value, and lifetime + behavior? +- Are the representation and contract definitions idiomatic for this + repository? +- Do the three selected proofs demonstrate useful consequences of the spec, + rather than merely restating it? + +No assessment of the pipeline, mutation campaign, or PBT harness is requested +in this PR. + +## Validation + +`SHA256SUMS` records the identities of the files in this packet. + +The complete optional proof family was checked with: + +```text +agent-foundation-devcontainer-cmake-3.30.9-v2:latest +sha256:7991a877c5297c564a524a4b3e3e6f260cc69d7ab0c4e23bf4ebc3e8f9d1c63f +opam exec -- dune build -j 32 @proof/optional/all @test/optional/all +``` + +The build exited 0 and produced all 23 optional proof objects. The proof +automation implementation and generated binding files are intentionally +omitted from this focused source review. + +## Deliberate omissions + +The completed run contains nineteen positive scenarios, six adversarial probes, +and eleven commissioned proof obligations. This packet selects only: + +- ordinary construction and observation; +- snapshot ownership after changing the constructor source; and +- rejection of a reference that outlives the optional. + +The smaller packet is intended to make the core design reviewable without +asking a maintainer to audit every generated evidence artifact. diff --git a/spec-review/optional-unsigned-char/SHA256SUMS b/spec-review/optional-unsigned-char/SHA256SUMS new file mode 100644 index 00000000..18c34ba9 --- /dev/null +++ b/spec-review/optional-unsigned-char/SHA256SUMS @@ -0,0 +1,10 @@ +48184db123ebc253e6f088b33932700b91c2f783bd5132ab4062796c1e94eaee clients/negative/reference_outlives_optional.cpp +ec47918b963ab7eddac14b1a5fe2cc0eec3a69ca4caf17545a1ec8be09c9e003 clients/positive/arbitrary_byte_roundtrip.cpp +fdc2adf644e3f132b1887d38217b879c9ebb8b8c137097e56d60699383cb62b5 clients/positive/rvalue_snapshot_not_alias.cpp +07c104b4f27b899050fa53d0533cc1ff7a41dd23fdeb8238d127c3ae1d6e1c8f proofs/negative/reference_outlives_optional_cpp_proof.v +4a744db2dd7b46245181a2acc19e38c6d2b25ab8882e596ce39edad17a711ebc proofs/positive/arbitrary_byte_roundtrip_cpp_proof.v +9b9322b7e8634a2f4a7b6c1d5076fd5160cecd4c996865ad1790163e058814e7 proofs/positive/rvalue_snapshot_not_alias_cpp_proof.v +08731e2ec98c58c3033a644453da0ea4803bbed96e44228011f9422879687816 spec/inc_optional.cpp +eea8fcb95dfbae8b133181b20b41af1085dd1c93ab11de758eb6c829b90959ae spec/model.v +5713f7fa398abf399284b252f061a97984331fcc86349c665433accc2cf012b1 spec/pred.v +a057d370d0b5be25e087fa2eb7c140aa33120546031c7d29e9db4e9f84d6384e spec/spec.v diff --git a/spec-review/optional-unsigned-char/clients/negative/reference_outlives_optional.cpp b/spec-review/optional-unsigned-char/clients/negative/reference_outlives_optional.cpp new file mode 100644 index 00000000..116d7691 --- /dev/null +++ b/spec-review/optional-unsigned-char/clients/negative/reference_outlives_optional.cpp @@ -0,0 +1,18 @@ +/** + * 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 +#include + +void +reference_outlives_optional() { + const unsigned char* retained = nullptr; + { + const std::optional value(static_cast(5)); + assert(value.has_value() == true); + retained = &*value; + } + assert(static_cast(*retained) == 5U); +} diff --git a/spec-review/optional-unsigned-char/clients/positive/arbitrary_byte_roundtrip.cpp b/spec-review/optional-unsigned-char/clients/positive/arbitrary_byte_roundtrip.cpp new file mode 100644 index 00000000..fe411695 --- /dev/null +++ b/spec-review/optional-unsigned-char/clients/positive/arbitrary_byte_roundtrip.cpp @@ -0,0 +1,17 @@ +/** + * 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 +#include + +void +arbitrary_byte_roundtrip() { + const std::optional low(static_cast(1)); + assert(low.has_value() == true); + assert(*low == 1U); + const std::optional high(static_cast(254)); + assert(high.has_value() == true); + assert(*high == 254U); +} diff --git a/spec-review/optional-unsigned-char/clients/positive/rvalue_snapshot_not_alias.cpp b/spec-review/optional-unsigned-char/clients/positive/rvalue_snapshot_not_alias.cpp new file mode 100644 index 00000000..7381ed83 --- /dev/null +++ b/spec-review/optional-unsigned-char/clients/positive/rvalue_snapshot_not_alias.cpp @@ -0,0 +1,17 @@ +/** + * 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 +#include +#include + +void +rvalue_snapshot_not_alias() { + unsigned char source = 5U; + const std::optional held(std::move(source)); + source = 7U; + assert(*held == 5U); + assert(source == 7U); +} diff --git a/spec-review/optional-unsigned-char/proofs/negative/reference_outlives_optional_cpp_proof.v b/spec-review/optional-unsigned-char/proofs/negative/reference_outlives_optional_cpp_proof.v new file mode 100644 index 00000000..2249dfc3 --- /dev/null +++ b/spec-review/optional-unsigned-char/proofs/negative/reference_outlives_optional_cpp_proof.v @@ -0,0 +1,27 @@ + +(* + * 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.proof. +Require Import skylabs.brick.libstdcpp.cassert.spec. +Require Import skylabs.brick.libstdcpp.optional.spec. +Require Import skylabs.brick.libstdcpp.test.optional.reference_outlives_optional_cpp. + +#[local] Set Default Goal Selector "!". + +Section with_cpp. + Context `{Σ : cpp_logic} `{MOD : source ⊧ σ}. + + cpp.spec "reference_outlives_optional()" default. + Lemma test_reference_outlives_optional : + verify[source] "reference_outlives_optional()". + Proof using MOD. + + verify_spec; go. + try (wpose (optionalR_value_view value_addr (1$m)%cQp 5); go). + + Fail Qed. + Abort. +End with_cpp. diff --git a/spec-review/optional-unsigned-char/proofs/positive/arbitrary_byte_roundtrip_cpp_proof.v b/spec-review/optional-unsigned-char/proofs/positive/arbitrary_byte_roundtrip_cpp_proof.v new file mode 100644 index 00000000..309e9ca2 --- /dev/null +++ b/spec-review/optional-unsigned-char/proofs/positive/arbitrary_byte_roundtrip_cpp_proof.v @@ -0,0 +1,26 @@ + +(* + * 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.proof. +Require Import skylabs.brick.libstdcpp.cassert.spec. +Require Import skylabs.brick.libstdcpp.optional.spec. +Require Import skylabs.brick.libstdcpp.test.optional.arbitrary_byte_roundtrip_cpp. + +#[local] Set Default Goal Selector "!". + +Section with_cpp. + Context `{Σ : cpp_logic} `{MOD : source ⊧ σ}. + + cpp.spec "arbitrary_byte_roundtrip()" default. + Lemma test_arbitrary_byte_roundtrip : + verify[source] "arbitrary_byte_roundtrip()". + Proof using MOD. verify_spec; go. + iExists (Vint 1); go. + - iExists (1$c)%cQp; go. + - iExists (Vint 254); go. + + iExists (1$c)%cQp; go. + Qed. +End with_cpp. diff --git a/spec-review/optional-unsigned-char/proofs/positive/rvalue_snapshot_not_alias_cpp_proof.v b/spec-review/optional-unsigned-char/proofs/positive/rvalue_snapshot_not_alias_cpp_proof.v new file mode 100644 index 00000000..5176adff --- /dev/null +++ b/spec-review/optional-unsigned-char/proofs/positive/rvalue_snapshot_not_alias_cpp_proof.v @@ -0,0 +1,26 @@ + +(* + * 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.proof. +Require Import skylabs.brick.libstdcpp.cassert.spec. +Require Import skylabs.brick.libstdcpp.optional.spec. +Require Import skylabs.brick.libstdcpp.test.optional.rvalue_snapshot_not_alias_cpp. + +#[local] Set Default Goal Selector "!". + +Section with_cpp. + Context `{Σ : cpp_logic} `{MOD : source ⊧ σ}. + + cpp.spec "std::move(unsigned char&)" from source inline. + + cpp.spec "rvalue_snapshot_not_alias()" default. + Lemma test_rvalue_snapshot_not_alias : + verify[source] "rvalue_snapshot_not_alias()". + Proof using MOD. verify_spec; go. + iExists (Vint 5); go. + iExists (1$c)%cQp; go. + Qed. +End with_cpp. diff --git a/spec-review/optional-unsigned-char/spec/inc_optional.cpp b/spec-review/optional-unsigned-char/spec/inc_optional.cpp new file mode 100644 index 00000000..6baa3d9f --- /dev/null +++ b/spec-review/optional-unsigned-char/spec/inc_optional.cpp @@ -0,0 +1,16 @@ +// Force the concrete class instance and both in-scope value-constructor forms. +#include + +template class std::optional; + +namespace { + +inline std::optional force_rvalue_ctor(unsigned char b) { + return std::optional(static_cast(b)); +} + +inline std::optional force_lvalue_ctor(unsigned char& b) { + return std::optional(b); +} + +} // namespace diff --git a/spec-review/optional-unsigned-char/spec/model.v b/spec-review/optional-unsigned-char/spec/model.v new file mode 100644 index 00000000..62180a51 --- /dev/null +++ b/spec-review/optional-unsigned-char/spec/model.v @@ -0,0 +1,22 @@ +(* + * 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.spec. + +Inductive state : Type := +| empty +| engaged (byte : Z). + +Definition has_value (s : state) : bool := + match s with + | empty => false + | engaged _ => true + end. + +Succeed Example empty_has_no_value : has_value empty = false := eq_refl. +Succeed Example engaged_zero_has_value : has_value (engaged 0) = true := eq_refl. +Succeed Example engaged_one_has_value : has_value (engaged 1) = true := eq_refl. +Succeed Example engaged_five_has_value : has_value (engaged 5) = true := eq_refl. +Succeed Example engaged_255_has_value : has_value (engaged 255) = true := eq_refl. diff --git a/spec-review/optional-unsigned-char/spec/pred.v b/spec-review/optional-unsigned-char/spec/pred.v new file mode 100644 index 00000000..6fc9185d --- /dev/null +++ b/spec-review/optional-unsigned-char/spec/pred.v @@ -0,0 +1,136 @@ +(* + * 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.optional.model. + +sl.lock +Definition empty_byteR `{Σ : cpp_logic, σ : genv} (q : cQp.t) : Rep := + structR "std::_Optional_payload_base::_Empty_byte" q. +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive empty_byteR. + +sl.lock +Definition storageR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) (s : state) : Rep := + match s with + | empty => + unionR + "std::_Optional_payload_base::_Storage" + q (Some 0%nat) ** + _field + "std::_Optional_payload_base::_Storage::_M_empty" + |-> empty_byteR q + | engaged byte => + unionR + "std::_Optional_payload_base::_Storage" + q (Some 1%nat) ** + _field + "std::_Optional_payload_base::_Storage::_M_value" + |-> ucharR q byte + end. +#[only(cfractional,timeless)] derive storageR. +#[global] Instance storageR_cfrac_valid `{Σ : cpp_logic, σ : genv} : + CFracValid1 storageR. +Proof. constructor. intros q s. rewrite storageR.unlock. destruct s; apply _. Qed. +#[global] Instance storageR_cfrac_splittable `{Σ : cpp_logic, σ : genv} : + CFracSplittable_1 storageR := {}. +#[only(lazy_unfold(export))] derive storageR. + +sl.lock +Definition payload_baseR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) (s : state) : Rep := + structR "std::_Optional_payload_base" q ** + _field "std::_Optional_payload_base::_M_payload" + |-> storageR q s ** + _field "std::_Optional_payload_base::_M_engaged" + |-> boolR q (has_value s). +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive payload_baseR. + +sl.lock +Definition payloadR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) (s : state) : Rep := + structR "std::_Optional_payload" q ** + _base "std::_Optional_payload" + "std::_Optional_payload_base" |-> payload_baseR q s. +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive payloadR. + +sl.lock +Definition optional_base_implR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) : Rep := + structR + "std::_Optional_base_impl>" + q. +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive optional_base_implR. + +sl.lock +Definition optional_baseR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) (s : state) : Rep := + structR "std::_Optional_base" q ** + _base "std::_Optional_base" + "std::_Optional_base_impl>" + |-> optional_base_implR q ** + _field "std::_Optional_base::_M_payload" + |-> payloadR q s. +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive optional_baseR. + +sl.lock +Definition enable_copy_moveR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) : Rep := + structR + "std::_Enable_copy_move<1b, 1b, 1b, 1b, std::optional>" + q. +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive enable_copy_moveR. + +sl.lock +Definition optionalR `{Σ : cpp_logic, σ : genv} + (q : cQp.t) (s : state) : Rep := + structR "std::optional" q ** + _base "std::optional" + "std::_Optional_base" |-> optional_baseR q s ** + _base "std::optional" + "std::_Enable_copy_move<1b, 1b, 1b, 1b, std::optional>" + |-> enable_copy_moveR q. +#[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive optionalR. + +(* Use [optional_value_ptr.unlock] when proving facts about the nested byte. *) +sl.lock +Definition optional_value_ptr `{σ : genv} (this : ptr) : ptr := + this ,, _base "std::optional" + "std::_Optional_base" + ,, _field "std::_Optional_base::_M_payload" + ,, _base "std::_Optional_payload" + "std::_Optional_payload_base" + ,, _field "std::_Optional_payload_base::_M_payload" + ,, _field + "std::_Optional_payload_base::_Storage::_M_value". + +#[global] Instance optionalR_learn `{Σ : cpp_logic, σ : genv} : + AtLearnEqF1 optionalR := ltac:(solve_learnable). + +#[global] Instance optionalR_agree `{Σ : cpp_logic, σ : genv} + q1 q2 s1 s2 : + Observe2 [| s1 = s2 |] (optionalR q1 s1) (optionalR q2 s2). +Proof. + apply observe_2_intro_only_provable. + rewrite !optionalR.unlock !optional_baseR.unlock !payloadR.unlock + !payload_baseR.unlock !storageR.unlock. + iIntros "(_ & Hbase1 & _) (_ & Hbase2 & _)". + iDestruct "Hbase1" as "(_ & _ & Hpayload1)". + iDestruct "Hbase2" as "(_ & _ & Hpayload2)". + iDestruct "Hpayload1" as "(_ & Hpayloadbase1)". + iDestruct "Hpayload2" as "(_ & Hpayloadbase2)". + iDestruct "Hpayloadbase1" as "(_ & Hstorage1 & Hengaged1)". + iDestruct "Hpayloadbase2" as "(_ & Hstorage2 & Hengaged2)". + destruct s1 as [|byte1], s2 as [|byte2]. + - done. + - iDestruct (observe_2 [| false = true |] + with "Hengaged1 Hengaged2") as %H. discriminate H. + - iDestruct (observe_2 [| true = false |] + with "Hengaged1 Hengaged2") as %H. discriminate H. + - iDestruct "Hstorage1" as "(_ & Hbyte1)". + iDestruct "Hstorage2" as "(_ & Hbyte2)". + iDestruct (observe_2 [| byte1 = byte2 |] + with "Hbyte1 Hbyte2") as %->. done. +Qed. diff --git a/spec-review/optional-unsigned-char/spec/spec.v b/spec-review/optional-unsigned-char/spec/spec.v new file mode 100644 index 00000000..b60c0f31 --- /dev/null +++ b/spec-review/optional-unsigned-char/spec/spec.v @@ -0,0 +1,46 @@ +(* + * 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.spec. +Require Export skylabs.brick.libstdcpp.optional.hints. +Require Import skylabs.brick.libstdcpp.optional.inc_optional_cpp. + +Section with_cpp. + Context `{Σ : cpp_logic, inc_optional_cpp.source ⊧ σ}. + + cpp.spec "std::optional::optional(std::nullopt_t)" + as nullopt_ctor_spec from inc_optional_cpp.source with (fun (this : ptr) => + \arg{tag} "#0" (Vptr tag) + \post this |-> optionalR 1$m empty). + + cpp.spec "std::optional::optional(unsigned char&&)" + as value_ctor_rvalue_spec from inc_optional_cpp.source with (fun (this : ptr) => + \arg{source} "__t" (Vref source) + \prepost{q byte} source |-> ucharR q byte + \post this |-> optionalR 1$m (engaged byte)). + + cpp.spec "std::optional::optional(unsigned char&)" + as value_ctor_lvalue_spec from inc_optional_cpp.source with (fun (this : ptr) => + \arg{source} "__t" (Vref source) + \prepost{q byte} source |-> ucharR q byte + \post this |-> optionalR 1$m (engaged byte)). + + cpp.spec "std::optional::has_value() const" + as has_value_spec from inc_optional_cpp.source with (fun (this : ptr) => + \prepost{q s} this |-> optionalR q s + \post[Vbool (has_value s)] emp). + + cpp.spec "std::optional::operator*() const &" + as deref_const_lvalue_spec from inc_optional_cpp.source with + (fun (this : ptr) => + \prepost{q byte} this |-> optionalR q (engaged byte) + \post[Vref (optional_value_ptr this)] emp). + + cpp.spec "std::optional::~optional()" + as destructor_spec from inc_optional_cpp.source with (fun (this : ptr) => + \pre{s} this |-> optionalR 1$m s + \post emp). + +End with_cpp.