std.time_affine: affine-instant time carrier (#4883 TemporalAggregator unit fix candidate)

dsl/examples/time_affine_check/time_affine_check.dag

@@ -0,0 +1,34 @@
+// Compile-witness for std.time_affine: threads the affine TIME carrier
+// end-to-end (imports, struct-field access, fn-typed op dictionary) WITHOUT
+// value-level arithmetic (the executable lowering is the tracked deferral).
+// Proves the affine types resolve and emit against pinned std.
+//
+// Gate (from gunbc repo root, after `cargo build --release -p v2-compiler --bin gunbc`):
+//   ./target/release/gunbc compile \
+//     --source-root dsl/examples/time_affine_check \
+//     --source-root dsl/std \
+//     --output-dir /tmp/time-affine-out \
+//     --target rust \
+//   && cargo check --manifest-path /tmp/time-affine-out/Cargo.toml
+
+module examples.time_affine_check
+
+import std.time_affine { Instant, Milliseconds, DrainWindow, TimeAffine }
+
+// Field access: a DrainWindow exposes an affine coordinate ...
+fn window_first_failed(w: DrainWindow) -> Instant {
+  w.first_failed_at
+}
+
+// ... and an additive duration threshold.
+fn window_threshold(w: DrainWindow) -> Milliseconds {
+  w.min_down
+}
+
+// The torsor subtraction, applied through the op dictionary (no hand-rolled
+// body): now - first_failed_at -> Milliseconds. This is the typed core of the
+// drain predicate `(now - first_failed_at) >= min_down`; the `>=` comparison
+// is the deferred value-Measure lowering.
+fn elapsed_since_failure(ops: TimeAffine, now: Instant, w: DrainWindow) -> Milliseconds {
+  ops.difference(now, w.first_failed_at)
+}

dsl/examples/time_affine_reject/instant_add_rejected.dag

@@ -0,0 +1,25 @@
+// DISCRIMINATING NEGATIVE WITNESS for std.time_affine (snappy refinement 1):
+// the load-bearing affine law is that `instant + instant` is FORBIDDEN -- it is
+// the whole reason `Instant` is NOT a `Measure`. This file attempts exactly that
+// illegal addition. The witness PASSES when this file FAILS to type-check.
+//
+// Enforcement is STRUCTURAL, not by-convention: `Instant` carries no additive
+// structure (it emits as a payload-free `pub struct Instant;` with no `Add`
+// impl), so `a + b` cannot type-check. The two legitimate affine operations
+// (`instant - instant -> Milliseconds`, `instant + Milliseconds -> instant`)
+// are reached ONLY through the `TimeAffine` op dictionary -- never the bare `+`.
+//
+// Gate (from gunbc repo root): `gunbc compile` emits, then
+//   cargo check --manifest-path <out>/Cargo.toml
+// MUST FAIL with `error[E0369]: cannot add Instant to Instant`. If it ever
+// compiles clean, the affine law has regressed (Instant gained an Add impl) and
+// the gate fails.
+
+module examples.time_affine_reject
+
+import std.time_affine { Instant }
+
+// ILLEGAL: adding two affine coordinates. Must be rejected.
+fn instant_plus_instant_is_forbidden(a: Instant, b: Instant) -> Instant {
+  a + b
+}

dsl/std/time_affine.dag

@@ -0,0 +1,22 @@
+// std/time_affine.dag -- affine time coordinates over an elapsed-time vector.
+// Scope: Instant (affine coordinate), Milliseconds (vector), TimeAffine (ops), DrainWindow (#4883 consumer).
+
+module std.time_affine
+
+// 🟡 P-TIME-ELAPSED-CARRIER opaque ms vector; dissolve-on: re-point to Measure<Time,Milli> when consumable.
+type Milliseconds {}
+
+// 🟡 P-TIME-AFFINE affine coordinate (no Add: instant+instant is type-rejected); dissolve-on: snappy torsor lift.
+type Instant {}
+
+// 🟡 P-TIME-AFFINE-OPS concrete torsor ops difference(I,I)->Ms / translate(I,Ms)->I; dissolve-on: generic torsor lift.
+type TimeAffine {
+  difference: fn(Instant, Instant) -> Milliseconds
+  translate:  fn(Instant, Milliseconds) -> Instant
+}
+
+// 🟡 P-TIME-AFFINE-CONSUMER #4883 burn-in window (coordinate + vector); dissolve-on: relocated TemporalAggregator.
+type DrainWindow {
+  first_failed_at: Instant
+  min_down: Milliseconds
+}

scripts/time-affine-keystone-gate.sh

@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# Keystone gate for std.time_affine (affine-instant time carrier).
+#
+# Proves BOTH directions of the affine law, so the model can't pass while the
+# law silently regresses:
+#   POSITIVE: the carrier + witness consumer compile AND cargo-check clean.
+#   NEGATIVE: `instant + instant` is REJECTED (cannot add Instant to Instant).
+#
+# Run from the gunbc repo root after:
+#   cargo build --release -p v2-compiler --bin gunbc
+#
+# Env knobs (match scripts/v4-nat-semiring-rung-gate.sh so it works on the
+# self-hosted runner): output goes under $RUNNER_TEMP (co-located with the
+# runner's warm CARGO_HOME / registry config) so `cargo check` of the emitted
+# crate resolves OFFLINE from the cache the v2-compiler build populated. A
+# hardcoded /tmp output sits outside the runner's cargo config and fails to
+# resolve deps under the CI egress quarantine.
+set -uo pipefail
+cd "$(dirname "$0")/.." || exit 2
+BIN="${V2_COMPILER:-target/release/gunbc}"
+CARGO="${CARGO_BIN:-cargo}"
+OUT="${RUNNER_TEMP:-/tmp}/time-affine-gate"
+# The EMITTED crate is generated code: gunbc's v2_rt.rs uses
+# `#[cfg(feature = "text_lookup_work_counter")]` which the runner's `-D warnings`
+# promotes from the `unexpected_cfgs` lint into a hard error, failing an
+# otherwise-clean `cargo check`. Cap lints at `warn` for these checks so
+# generated-code lint noise can't fail the gate -- while REAL type errors (the
+# negative gate's E0369 `cannot add Instant`) are hard errors, NOT lints, so they
+# still fail as required.
+export RUSTFLAGS="${RUSTFLAGS:-} --cap-lints=warn"
+# Force monochrome cargo/rustc output: on the runner cargo emits ANSI color, which
+# splices escape codes (`\e[0m\e[1m`) BETWEEN `error[E0369]` and `: cannot add`, so a
+# concatenated grep silently misses the real diagnostic. `never` keeps neg-check.log
+# plain text so the code-anchored grep below matches in CI exactly as it does locally.
+export CARGO_TERM_COLOR=never
+[ -x "$BIN" ] || { echo "FAIL: build $BIN first (cargo build --release -p v2-compiler --bin gunbc)"; exit 2; }
+mkdir -p "$OUT"
+
+fail() { echo "GATE FAIL: $1"; exit 1; }
+
+echo "== POSITIVE: carrier + witness compile + cargo check =="
+"$BIN" compile --source-root dsl/examples/time_affine_check --source-root dsl/std \
+  --output-dir "$OUT/pos" --target rust 2>&1 | tail -1
+"$CARGO" check --manifest-path "$OUT/pos/Cargo.toml" >"$OUT/pos-check.log" 2>&1 \
+  || { echo "--- pos-check.log tail ---"; tail -20 "$OUT/pos-check.log"; fail "positive consumer did not cargo-check"; }
+echo "  OK: positive gate green"
+
+echo "== NEGATIVE: instant + instant must be rejected =="
+"$BIN" compile --source-root dsl/examples/time_affine_reject --source-root dsl/std \
+  --output-dir "$OUT/neg" --target rust 2>&1 | tail -1
+if "$CARGO" check --manifest-path "$OUT/neg/Cargo.toml" >"$OUT/neg-check.log" 2>&1; then
+  fail "instant + instant COMPILED — the affine law has regressed (Instant gained Add)"
+fi
+# Match the diagnostic CODE (error[E0369]) plus its message, not the bare
+# "cannot add" substring: E0369 is the structural "no Add impl" rejection we
+# require, so keying on the code can't be satisfied by an unrelated future
+# diagnostic that merely happens to contain the words "cannot add".
+grep -q 'error\[E0369\]' "$OUT/neg-check.log" && grep -q 'cannot add' "$OUT/neg-check.log" \
+  || { echo "--- neg-check.log tail ---"; tail -20 "$OUT/neg-check.log"; fail "negative gate failed for the wrong reason (expected E0369 'cannot add')"; }
+echo "  OK: instant + instant rejected ($(grep -m1 'error\[E0369\]' "$OUT/neg-check.log" | sed 's/^ *//'))"
+
+echo "GATE PASS"