WIP on agent-generated ctime specs

output/ctime-repair/memory.md

@@ -0,0 +1,17 @@
+# ctime-repair
+
+- Active proof target: `rocq-brick-libstdcpp/test/ctime/proof.v`
+- Current reproduced failure from `dune build ./test/ctime/proof.vo`:
+  - non-fatal missing-spec diagnostics for POD repro lemmas via `verify?`
+  - earlier fatal proof failure at `test_mktime_ptr_ok`
+- Live replay in `dune rocq top test/ctime/proof.v` found the wrapper-spec issue:
+  - using `\pre{q tm_in}` was still too strong and left a half-fraction ownership mismatch
+  - the correct wrapper statement uses `\prepost{q tm_in} tm_p |-> tmR q tm_in`
+    and makes the explicit post ask only for the pure `mktime_result` witness plus
+    `tm_p |-> tmR (cQp.scale (1 / 2) q) tm_out`
+  - under that statement, `verify_spec; go.` leaves only
+    `∃ t0 : time_t_model, [| mktime_result tm_in t t0 |]`
+  - `iExists _. go.` closes the proof
+- Current repair choice:
+  - keep the `test_mktime_ptr_ok` proof as
+    `verify_spec. go. iExists _. go. Qed.`

rocq-brick-libstdcpp/output/ctime-pod-dtor-repro/memory.md

@@ -0,0 +1 @@
+- Restoring stack-local tm/timespec validation clients to reproduce synthetic destructor proof failures.

rocq-brick-libstdcpp/proof/ctime/design.md

@@ -0,0 +1,33 @@
+# `<ctime>` BRiCk Spec Design
+
+## 1. Summary
+
+1. Add a new `proof/ctime` folder and a companion `test/ctime` folder.
+2. Cover the standard `<ctime>` surface from cppreference and C11 7.27, with `difftime` deferred because BRiCk does not currently support doubles.
+3. Use an abstract-but-accurate design: explicit ownership for writable outputs, borrowed resources for static return objects, and abstract model relations for time conversion and formatting.
+
+## 2. Public API and Representation Changes
+
+1. The proof folder contains `inc_ctime.cpp`, `pred.v`, `model.v`, and `spec.v`.
+2. Specs target the unqualified names emitted by `cpp2v`: `clock`, `time`, `mktime`, `gmtime`, `localtime`, `asctime`, `ctime`, `strftime`, and `timespec_get`.
+3. V1 remains standard-only and excludes glibc and POSIX extensions visible in the generated AST.
+4. The model layer exports `tm_model` and `timespec_model`.
+5. `tmR` hides non-standard `tm_gmtoff` and `tm_zone` fields behind `tmR_hidden`, while `timespecR` tracks only `tv_sec` and `tv_nsec`.
+
+## 3. Specification Design
+
+1. `clock` and `time` are modeled as abstract current-time queries over signed integer results.
+2. `timespec_get` is only specified for `TIME_UTC = 1`.
+3. `mktime`, `gmtime`, and `localtime` use abstract conversion and normalization relations instead of a concrete calendar algorithm.
+4. `asctime` and `ctime` return borrowed C strings with explicit close obligations, matching the existing static-storage style used elsewhere in the repo.
+5. `strftime` writes into a caller-owned `cstring.bufR` buffer and returns either `0` or the produced string length.
+
+## 4. Validation Plan
+
+1. `test/ctime/test.cpp` exercises `std::time`, `std::timespec_get`, `std::mktime`, `std::gmtime`, `std::localtime`, `std::asctime`, `std::ctime`, `std::strftime`, and repeated static-return calls.
+2. `test/ctime/proof.v` proves representative client lemmas against the new specs.
+3. The test clients use `std::`-qualified calls so the proof confirms those names resolve against the unqualified spec entries produced by `cpp2v`.
+
+## 5. Known Deviation
+
+1. `difftime` is intentionally deferred until BRiCk has a supported story for `double` values in specs and proofs.

rocq-brick-libstdcpp/proof/ctime/inc_ctime.cpp

@@ -0,0 +1 @@
+#include <ctime>

rocq-brick-libstdcpp/proof/ctime/model.v

@@ -0,0 +1,64 @@
+(*
+ * Copyright (c) 2025 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.cpp.string.
+
+#[local] Set Primitive Projections.
+#[local] Open Scope Z_scope.
+
+Record tm_t := {
+  tm_model_sec : Z;
+  tm_model_min : Z;
+  tm_model_hour : Z;
+  tm_model_mday : Z;
+  tm_model_mon : Z;
+  tm_model_year : Z;
+  tm_model_wday : Z;
+  tm_model_yday : Z;
+  tm_model_isdst : Z;
+}.
+
+Record timespec_t := {
+  timespec_model_sec : Z;
+  timespec_model_nsec : Z;
+}.
+
+Definition TIME_UTC : Z := 1.
+
+Definition clock_t := Z.
+Definition time_t := Z.
+
+Parameter abs_time_t : Type.
+Parameter abs_time_of_N : N -> abs_time_t.
+Parameter abs_time_diff_t : Type.
+
+Definition timespec_wf (ts : timespec_t) : Prop :=
+  0 <= timespec_model_nsec ts < 1000000000.
+
+Parameter time_t_to_abs_time : time_t -> abs_time_t -> Prop.
+Parameter timespec_to_abs_time : timespec_t -> abs_time_t -> Prop.
+Parameter clock_t_to_abs_time_diff : clock_t -> abs_time_diff_t -> Prop.
+Parameter abs_time_plus_diff : abs_time_t -> abs_time_diff_t -> abs_time_t -> Prop.
+
+Parameter utc_time_to_tm : time_t -> tm_t -> Prop.
+Parameter local_time_to_tm : time_t -> tm_t -> Prop.
+Parameter mktime_result : tm_t -> tm_t -> time_t -> Prop.
+Parameter asctime_text_of : tm_t -> cstring.t -> Prop.
+Parameter strftime_text_of : cstring.t -> tm_t -> cstring.t -> Prop.
+
+Definition ctime_text_of (t : time_t) (out : cstring.t) : Prop :=
+  exists tm, local_time_to_tm t tm /\ asctime_text_of tm out.
+
+Axiom asctime_text_of_len :
+  forall tm out,
+    asctime_text_of tm out ->
+    cstring.size out = 25.
+
+Axiom strftime_text_of_fit :
+  forall fmt tm out bound,
+    strftime_text_of fmt tm out ->
+    bound = cstring.size out ->
+    0 <= bound.

rocq-brick-libstdcpp/proof/ctime/plan2.md

@@ -0,0 +1,76 @@
+# `<ctime>` Refactor And Proof-Repair Plan
+
+## Summary
+
+1. Keep both client styles in `test/ctime`: green wrapper clients for normal validation and stack-local POD repro clients for the `tm::~tm()` / `timespec::~timespec()` verifier completeness bug.
+2. Refactor the `ctime` proof stack so `model.v` is pure-only and `pred.v` owns all separation predicates, including `later_than`, `tmR`, and `timespecR`.
+3. Rework `tmR` with `sl.lock` and `#[only(lazy_unfold)] derive` so it stays abstract in client proofs while hiding non-standard `tm` fields.
+4. Repair as many non-repro proofs as possible, using `dune coq top` / `dune rocq top` for live replay, while keeping the POD repro lemmas explicit and buildable.
+
+## Key Changes
+
+1. Refactor the layer split.
+   `model.v` will contain only pure definitions and `Prop`-valued relations.
+   Move `tm_model` and `timespec_model` into `model.v`.
+   Keep `TIME_UTC`, `clock_t_model`, `time_t_model`, `clock_result`, `timespec_get_result`, `utc_time_to_tm`, `local_time_to_tm`, `mktime_result`, `asctime_text_of`, `strftime_text_of`, and `ctime_text_of` in `model.v`.
+   `pred.v` will import `model.v` and define all `Rep` / `mpred`-valued abstractions.
+
+2. Replace `current_time_result` with `later_than` in `pred.v`.
+   Remove `current_time_result` entirely.
+   Define `later_than` as a `Parameter`, not by copy-pasting the class-based NOVA code.
+   Add the needed supporting declarations in parameter/axiom form: `Knowledge1 later_than`, `Timeless1 later_than`, `WeaklyObjective1 later_than`, and the down-closed law.
+   Do not add `Hint Opaque later_than` or `Arguments later_than : simpl never.`, since `later_than` is a parameter and those lines would add no value.
+   Update the `time` spec so success returns the integer time value and `later_than` for that value, and `time(&t)` also writes the same integer to `*t`.
+
+3. Rework `tmR` to match the intended public contract.
+   Publicly expose only the 9 ISO C `tm` fields via `tm_model`.
+   Keep `tm_gmtoff` and `tm_zone` hidden inside `tmR_hidden`.
+   Do not decide now whether `tm_zone` is owned, borrowed, or ignored; hide that choice inside `tmR_hidden` and add a TODO comment for later investigation.
+   Implement the exported `tmR` through a locked wrapper.
+   Prefer `sl.lock` and `#[only(lazy_unfold)] derive` to solve the current transparency issue instead of ad hoc opacity hints.
+   Apply the same style to any other exported rep that needs abstraction control in client proofs.
+
+4. Keep `timespecR` simple and standard-facing.
+   `timespecR` continues to describe only `tv_sec` and `tv_nsec`.
+   If abstraction control is needed for `timespecR`, use the same locked/lazy-unfold pattern as `tmR`.
+
+5. Update the client suite to include both green and repro paths.
+   Add pointer-wrapper clients for `timespec_get` and `mktime` so those APIs have green proof-backed coverage without local POD cleanup.
+   Keep stack-local POD repro clients for both `std::timespec` and `std::tm`.
+   Keep direct green clients for `gmtime`, `localtime`, `asctime`, `ctime`, `strftime`, and repeated static-return calls, unless proof replay shows a strictly better shape.
+   Keep `main()` on the green path only so `main_ok` remains part of the normal successful build.
+
+6. Update `test/ctime/proof.v` to reflect the split.
+   Fully prove the green clients where feasible.
+   Keep the POD repro lemmas under `verify?` and explicitly `Admitted` if the destructor-spec bug still blocks them.
+   Add short comments stating that those lemmas intentionally preserve a verifier completeness repro.
+   For non-repro lemmas, do not stop at the first failure: try to repair each proof, or leave the most-progress script if full discharge is still blocked.
+
+## Proof Repair Strategy
+
+1. First fix the representation-level blocker.
+   Refactor `tmR` and `timespecR` so client proofs no longer fail on transparent rep expansion.
+
+2. Then replay each non-repro client proof individually.
+   Use `dune coq top` or `dune rocq top` from the `rocq-brick-libstdcpp` project root as the default live environment.
+   Prefer dune-managed tops over plain `coqtop` for proof inspection and debugging.
+   Keep proof edits local and minimal; do not introduce broad infrastructure unless repeated failures show it is necessary.
+
+3. Treat the POD destructor repros separately.
+   Preserve isolated repro lemmas for local `tm` and local `timespec`.
+   Keep them buildable through explicit admissions if the verifier still insists on destructor specs without bodies.
+
+## Validation Plan
+
+1. Rebuild `./test/ctime/proof.vo` as the main acceptance target.
+2. Confirm the green path proves successfully, including `main()`.
+3. Confirm the POD repro lemmas remain present and documented.
+4. Confirm the generated `test_cpp.v` still contains local `tm` and `timespec` objects for the repro cases.
+5. Re-run proof replay on every non-repro lemma and retain the strongest checked script reached for each one.
+
+## Assumptions And Defaults
+
+1. The final `ctime` test theory should stay buildable even if POD repro lemmas remain admitted.
+2. `later_than` is a local `ctime` abstraction in `pred.v`, not an import of NOVA’s shared predicate framework.
+3. The `tm_zone` ownership question is intentionally deferred and hidden inside `tmR_hidden`.
+4. `difftime` remains deferred.

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

@@ -0,0 +1,109 @@
+(*
+ * Copyright (c) 2025 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 Import skylabs.auto.cpp.elpi.derive.
+Require Export skylabs.cpp.string.
+Require Export skylabs.brick.libstdcpp.iostream.pred.
+
+Require Export skylabs.brick.libstdcpp.ctime.model.
+Require Import skylabs.brick.libstdcpp.ctime.inc_ctime_cpp.
+
+#[local] Set Primitive Projections.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Parameter later_than : abs_time_t -> mpred.
+  #[global] Declare Instance later_than_knowledge : Knowledge1 later_than.
+  #[global] Declare Instance later_than_timeless : Timeless1 later_than.
+  #[global] Declare Instance later_than_weakly_objective : WeaklyObjective1 later_than.
+  Axiom later_than_down_closed :
+    forall t1 t2,
+      (t1 <= t2)%N ->
+      later_than (abs_time_of_N t2) |-- later_than (abs_time_of_N t1).
+
+  Parameter system_start_at : abs_time_t -> mpred.
+  #[global] Declare Instance system_start_at_knowledge : Knowledge1 system_start_at.
+  #[global] Declare Instance system_start_at_timeless : Timeless1 system_start_at.
+  #[global] Declare Instance system_start_at_weakly_objective : WeaklyObjective1 system_start_at.
+
+  (** Correctness of a [time] result, relative to the current-time world. *)
+  Definition time_result (t : time_t) : mpred :=
+    [| 0 <= t |] **
+    Exists now,
+      [| time_t_to_abs_time t now |] **
+      later_than now.
+  #[global] Hint Opaque time_result : typeclass_instances sl_opacity.
+  #[global] Arguments time_result : simpl never.
+
+  (** Correctness of a [timespec_get] result, relative to current absolute time. *)
+  Definition timespec_get_result (ts : timespec_t) : mpred :=
+    [| timespec_wf ts |] **
+    Exists now,
+      [| timespec_to_abs_time ts now |] **
+      later_than now.
+  #[global] Hint Opaque timespec_get_result : typeclass_instances sl_opacity.
+  #[global] Arguments timespec_get_result : simpl never.
+
+  (** Correctness of a [clock] result as duration since system start. *)
+  Definition clock_result (ticks : clock_t) : mpred :=
+    [| 0 <= ticks |] **
+    Exists diff start now,
+      [| clock_t_to_abs_time_diff ticks diff |] **
+      system_start_at start **
+      [| abs_time_plus_diff start diff now |] **
+      later_than now.
+  #[global] Hint Opaque clock_result : typeclass_instances sl_opacity.
+  #[global] Arguments clock_result : simpl never.
+
+  (** Representation of the hidden, non-standard tail of [struct tm].
+
+      This predicate is the only place where the glibc-specific fields
+      [tm_gmtoff] and [tm_zone] may appear. It is meant to describe those
+      fields relative to the enclosing [tm] object while keeping their exact
+      ownership story abstract from clients of [tmR].
+
+      This predicate is intentionally unindexed: a provisional equation for a
+      dummy hidden model would become part of the interface and make later
+      refinements breaking changes. If clients eventually need semantic facts
+      about the non-standard tail, introduce that model deliberately then.
+
+      TODO: investigate whether [tm_zone] should be owned, borrowed, or
+      abstracted away by this hidden representation. *)
+  Parameter tmR_hidden : cQp.t -> Rep.
+  #[only(cfracsplittable)] derive tmR_hidden.
+
+  Parameter timespecR_raw : cQp.t -> timespec_t -> Rep.
+  #[only(type_ptr="timespec", cfracsplittable)] derive timespecR_raw.
+End with_cpp.
+
+sl.lock
+Definition tmR `{Σ : cpp_logic} {σ : genv} (q : cQp.t) (tm : tm_t) : Rep :=
+  structR "tm" q **
+  _field "tm::tm_sec" |-> primR Tint q (Vint tm.(tm_model_sec)) **
+  _field "tm::tm_min" |-> primR Tint q (Vint tm.(tm_model_min)) **
+  _field "tm::tm_hour" |-> primR Tint q (Vint tm.(tm_model_hour)) **
+  _field "tm::tm_mday" |-> primR Tint q (Vint tm.(tm_model_mday)) **
+  _field "tm::tm_mon" |-> primR Tint q (Vint tm.(tm_model_mon)) **
+  _field "tm::tm_year" |-> primR Tint q (Vint tm.(tm_model_year)) **
+  _field "tm::tm_wday" |-> primR Tint q (Vint tm.(tm_model_wday)) **
+  _field "tm::tm_yday" |-> primR Tint q (Vint tm.(tm_model_yday)) **
+  _field "tm::tm_isdst" |-> primR Tint q (Vint tm.(tm_model_isdst)) **
+  tmR_hidden q.
+#[only(lazy_unfold)] derive tmR.
+#[only(type_ptr,cfracsplittable)] derive tmR.
+
+sl.lock
+Definition timespecR `{Σ : cpp_logic} {σ : genv} (q : cQp.t) (ts : timespec_t) : Rep :=
+  timespecR_raw q ts.
+#[only(lazy_unfold)] derive timespecR.
+#[only(type_ptr,cfracsplittable)] derive timespecR.
+
+#[global] Instance tmR_learnable `{Σ : cpp_logic} {σ : genv} : LearnEqF1 tmR :=
+  ltac:(solve_learnable).
+
+#[global] Instance timespecR_learnable `{Σ : cpp_logic} {σ : genv} : LearnEqF1 timespecR :=
+  ltac:(solve_learnable).