Review std::optional<unsigned char> specification and proofs

spec-review/optional-unsigned-char/1-scope.md

@@ -0,0 +1,46 @@
+# Review scope
+
+This review covers only `std::optional<unsigned char>` as implemented by
+libstdc++ 12. It does not propose a generic `std::optional<T>` 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.

spec-review/optional-unsigned-char/README.md

@@ -0,0 +1,74 @@
+# Review artifacts — `std::optional<unsigned char>`
+
+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.

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

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 <cassert>
+#include <optional>
+
+void
+reference_outlives_optional() {
+    const unsigned char* retained = nullptr;
+    {
+        const std::optional<unsigned char> value(static_cast<unsigned char>(5));
+        assert(value.has_value() == true);
+        retained = &*value;
+    }
+    assert(static_cast<unsigned int>(*retained) == 5U);
+}

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 <cassert>
+#include <optional>
+
+void
+arbitrary_byte_roundtrip() {
+    const std::optional<unsigned char> low(static_cast<unsigned char>(1));
+    assert(low.has_value() == true);
+    assert(*low == 1U);
+    const std::optional<unsigned char> high(static_cast<unsigned char>(254));
+    assert(high.has_value() == true);
+    assert(*high == 254U);
+}

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 <cassert>
+#include <optional>
+#include <utility>
+
+void
+rvalue_snapshot_not_alias() {
+    unsigned char source = 5U;
+    const std::optional<unsigned char> held(std::move(source));
+    source = 7U;
+    assert(*held == 5U);
+    assert(source == 7U);
+}

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.

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.

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&>(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.

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 <optional>
+
+template class std::optional<unsigned char>;
+
+namespace {
+
+inline std::optional<unsigned char> force_rvalue_ctor(unsigned char b) {
+  return std::optional<unsigned char>(static_cast<unsigned char&&>(b));
+}
+
+inline std::optional<unsigned char> force_lvalue_ctor(unsigned char& b) {
+  return std::optional<unsigned char>(b);
+}
+
+} // namespace

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.