diff --git a/dsl/examples/time_affine_check/time_affine_check.dag b/dsl/examples/time_affine_check/time_affine_check.dag new file mode 100644 index 00000000000..abc1f6b7182 --- /dev/null +++ b/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) +} diff --git a/dsl/examples/time_affine_reject/instant_add_rejected.dag b/dsl/examples/time_affine_reject/instant_add_rejected.dag new file mode 100644 index 00000000000..a7812cacfd7 --- /dev/null +++ b/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 /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 +} diff --git a/dsl/std/time_affine.dag b/dsl/std/time_affine.dag new file mode 100644 index 00000000000..69f1ac8530c --- /dev/null +++ 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 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 +} diff --git a/scripts/time-affine-keystone-gate.sh b/scripts/time-affine-keystone-gate.sh new file mode 100755 index 00000000000..aab682b6493 --- /dev/null +++ b/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"