3f-temporal Minimal temporal core — past[n], rose, fell, stable

Scope trimmed by ruling 2026-07-10. The temporal library is now a minimal core of four operators, each a pure function lowering to flops with no new semantics:

• past[n](x) — the compiler inserts n flops. Synthesizable (usable anywhere).
• rose(x) / fell(x) / stable(x) — pure functions of x and past(x) (rose = x && !past(x) etc.); verification contexts only (test/formal blocks and the asserts inside them), as before — they never appear in synthesized datapath.

Dropped from scope (git history keeps the old page): next[n] (non-causal), windowed eventually[w]/always[w] (bounded liveness — a future discussion once the core proves out), changed (spell it !stable), and the .[rising]/.[falling]/ .[changed] attribute sugar. The docs (09-verification.md, 15-tbd.md, quick-intro tags) must be trimmed to match — TBD marks drop only for the minimal core when it lands.

Today

• A partial past lowering exists (prp_builtins.hpp past_builtin_delay) but fails the LEC acceptance below; rose/fell/stable have no semantic handling anywhere (tolg-error "no hardware lowering yet").
• Fail-by-design regression: prp-tbd-temporal_past (inou/prp/tests/fixme/) — flips green and sheds its fixme tag when past lands.

Depends on

2f-verify — proving the assertions these operators feed uses the landed incremental BMC + verdict-ladder engine; the operators here only produce cond signals (flop cones), which that engine already handles. No engine work is needed for the minimal core.

Acceptance (unchanged)

// delay2.prp
mod delay2(a:u8) -> (out:u8@[2]) {
  out = past[2](a)
}

// delay2.v — must LEC-match
module delay2(input clk, input reset, input [7:0] a, output reg [7:0] out);
  reg [7:0] t1;
  always @(posedge clk) begin
    if (reset) begin t1 <= 8'b0; out <= 8'b0; end
    else       begin t1 <= a;    out <= t1;   end
  end
endmodule

Done when: delay2 LECs against the golden Verilog; rose/fell/stable evaluate in test blocks and prove via formal blocks; the docs' TBD marks for the minimal core are dropped and the dropped operators are removed from the docs.

Docs

• docs/pyrope/09-verification.md — trim the "Temporal library" section to the minimal core
• docs/pyrope/15-tbd.md