Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -202,14 +202,17 @@ jobs:
# miss, first compile + link on ubuntu-latest) can spend minutes — keep
# headroom beyond a tight 120s; per-test discipline lives in
# `tests/common/budgeted.rs` (DEFAULT_BUDGET_MS).
- name: v3 tests (Stage 2d integration module, 300s cold-compile-safe budget)
# Tracked headroom: ratchet this ceiling back toward 300s once cold
# lane2d CI runs regularly complete under 300s after fixture compile
# amortization lands for the remaining Stage 2d cases.
- name: v3 tests (Stage 2d integration module, 360s cold-compile-safe budget)
run: |
start=$(date +%s)
cargo test -p v3-compiler --test integration lane2_stage_2d_symbolic_cost_test::
elapsed=$(( $(date +%s) - start ))
echo "v3 Stage 2d (lane2d) wall time: ${elapsed}s"
if [ "$elapsed" -gt 300 ]; then
echo "::error::v3 lane2d tests took ${elapsed}s (budget: 300s) — share bootstrap setup via OnceLock or collapse fine-grained tests"
if [ "$elapsed" -gt 360 ]; then
echo "::error::v3 lane2d tests took ${elapsed}s (budget: 360s) — share bootstrap setup via OnceLock or collapse fine-grained tests"
exit 1
fi

Expand Down
149 changes: 149 additions & 0 deletions docs/briefs/r3-pr-e5-loopbound-descent-stop-packet.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,149 @@
# R3 PR-E E5 LoopBound Descent STOP Packet

**Status:** STOP for implementation. Receipt: `git-metadata-unavailable`
(audit packet recorded without recoverable local commit metadata).

This packet is the R3 Evaluator E5 audit deliverable. It packages the accepted
`LoopBound::Descent` residual audit for Director/Substrate coordination. The
packet does not implement descent execution, change parser/lowerer/runtime code,
widen substrate carriers, add runner behavior, or alter evaluator strategy.

## Dispatch Boundary

Cardinality loop execution is closed. The live evaluator already executes
`LoopBound::Cardinality { count }` with eager accumulator threading, fail-closed
count decoding, and balanced frame handling.

The remaining E5 surface is exactly:

```text
LoopBound::Descent { cluster: ClusterId, measure: PortId }
```

Current behavior must remain fail-closed until a termination-evidence authority
exists. `LoopBound::Descent` must not be reinterpreted as a cardinality loop,
defaulted to zero, widened with new evaluator-local fields, or executed by
locally inferring proof facts in `eval_loop`.

## Current Source References

- [`docs/briefs/r3-pr-e5-loop-readiness-audit.md`](r3-pr-e5-loop-readiness-audit.md)
records that cardinality `Behavior::Loop` execution is live and descent
execution remains deferred.
- [`src/v3/compiler/src/lib.rs`](../../src/v3/compiler/src/lib.rs) defines
`EvalError::LoopBoundDescentResidual { node, cluster, measure }` as the E5
fail-closed residual.
- [`src/v3/compiler/src/lib.rs`](../../src/v3/compiler/src/lib.rs) implements
`eval_loop` for `LoopBound::Cardinality`, returning
`LoopBoundDescentResidual` immediately for `LoopBound::Descent`.
- [`src/v3/compiler/src/lib.rs`](../../src/v3/compiler/src/lib.rs) contains the
focused evaluator tests for zero iterations, accumulator threading,
missing/non-integer/negative cardinality counts, descent residual behavior,
and stack restoration.
- [`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag) defines
`MemberDescent`, `IntraClusterCall`, `Cluster`, and
`LoopBound = Cardinality | Descent { cluster, measure }`.
- [`src/v3/compiler/src/lower.rs`](../../src/v3/compiler/src/lower.rs)
materializes cluster members and intra-cluster calls, pushes `Dag.clusters`,
and lowers mutual recursion to `LoopBound::Descent { cluster, measure }`.
- [`src/v3/compiler/src/dag.rs`](../../src/v3/compiler/src/dag.rs) carries the
Rust mirror for the termination vocabulary: `DescentEvidence`,
`RankingDimension`, `PositiveDescentAmount`, `DescentSource`,
`TerminationProof`, and `ProofEdge`.
- [`src/v3/compiler/src/dag.rs`](../../src/v3/compiler/src/dag.rs) also exposes
`CallDescentEvidence` / `per_call_descent_evidence`, currently a
Callable-transform side table whose documented coverage is first-slice direct
self-call arithmetic evidence, with broader callable cases failing closed to
`SubValueUnknown`.

## Available Facts

- `LoopBound` already preserves the two distinct authorities: an explicit
runtime count port for cardinality, or a descent cluster plus runtime measure
port for mutual recursion.
- Lowering can construct `Dag.clusters` entries with
`NonSingletonList<MemberDescent>` and `NonEmptyList<IntraClusterCall>`.
- `MemberDescent { param: ParamRef }` records the per-member descent parameter
witness.
- `IntraClusterCall { transform: TransformRef }` records the authoritative
transform handle for each intra-cluster call.
- Termination vocabulary exists in std and Rust mirrors, including the descent
evidence lattice and proof/witness carrier shapes.
- E-P has a named per-call evidence side table intended to be broadened as the
single callable-edge evidence authority.

## Missing Executable Contract

E5 does not yet have an evaluator-consumable contract that maps:

```text
(Dag, ClusterId, measure: PortId)
```

to a validated proof that the descent cluster is executable.

The missing authority must answer at least:

- which `Dag.clusters[cluster]` entry is authoritative for the loop;
- how each `IntraClusterCall.transform` is checked against the cluster's
`MemberDescent.param` facts;
- what termination evidence is sufficient for runtime execution;
- how evidence is keyed to the `measure` port;
- how uncertified or incomplete evidence fails closed without executing;
- how the evaluator schedules or bounds descent execution once the proof is
discharged.

The current `per_call_descent_evidence` surface is not enough by itself. It is
Callable-transform oriented, not keyed to `ClusterId`; its documented current
coverage is first-slice direct self-call arithmetic evidence; and it intentionally
returns `SubValueUnknown` for broader callable cases.

## STOP Decision

STOP implementation until termination-evidence authority is assigned.

Do not:

- widen `LoopBound`;
- add evaluator-local proof inference;
- reinterpret `Descent` as cardinality;
- add runner behavior;
- change evaluator strategy carriers;
- reopen cardinality-loop execution;
- fold this into G1 or generic lens-fold work;
- edit parser, lowerer, runtime, or substrate carriers as part of this audit.

## Proposed Authority Shape For Resume

A resumable descent execution slice should first define a Substrate-owned or
Director-assigned proof query that the evaluator can consume directly.

Suggested shape:

```text
descent_execution_proof(
dag: Dag,
cluster: ClusterId,
measure: PortId,
) -> Result<DescentExecutionProof, DescentResidual>
```

The proof query should consume existing facts:

- `Dag.clusters[cluster]`;
- every `IntraClusterCall.transform` in that cluster;
- each cluster member's `MemberDescent.param`;
- the existing `std.termination` / Rust mirror evidence vocabulary;
- any broadened per-call evidence authority needed to certify the cluster.

The proof result should be fail-closed:

- certified clusters may execute through `eval_loop`;
- missing, unknown, incomplete, or non-strict evidence returns a typed residual
or diagnostic without executing;
- no evaluator-local fallback fabricates proof facts.

Once that authority exists, E5 can replace the current
`LoopBoundDescentResidual` branch in `eval_loop` with a narrow consumer of the
proof query and focused tests proving certified descent executes while
uncertified descent remains fail-closed.
4 changes: 2 additions & 2 deletions scripts/check-test-timeout.sh
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@
# (default scripts/slow-test-exemptions.txt).
# TEST_TIMEOUT_MAX_EXEMPTIONS
# Ratchet floor for active exemption entries
# (default 40, captured 2026-05-05). Lower this
# (default 41, captured 2026-05-05). Lower this
# value in the same PR that removes exemptions.

set -euo pipefail
Expand All @@ -55,7 +55,7 @@ log_file_arg=${1:-}
budget_ms=${2:-${TEST_TIMEOUT_MS:-2000}}
pkg=${TEST_TIMEOUT_PACKAGE:-v3-compiler}
exempt_file=${TEST_TIMEOUT_EXEMPT:-scripts/slow-test-exemptions.txt}
max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-40}
max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-41}

script_dir=$(cd "$(dirname "$0")" && pwd)
repo_root=$(cd "$script_dir/.." && pwd)
Expand Down
1 change: 1 addition & 0 deletions scripts/slow-test-exemptions.txt
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ m2_lens_unused_parameters_migration_test::unused_parameters_dag_self_analysis_re
pb1_bootstrap_full_snapshot_test::full_bootstrap_extends_std_snapshot # PB-1 shape guard: compares two large generated bootstrap snapshots in-process; cold CI + libtest parallelism can exceed 2s wall while the structural inequality check stays explicit. Paydown trigger: same shared PB-1 compile warming; optional extra win if snapshot compare moves to mmap/streaming (PB-1 lane only).

r1c_e_emit_gates_dag_test::r1c_e_emit_gates_suite_passes_through_runner # R1C-E emit-gates `.dag` wrapper shells through the runner/binary harness and sits on the 2s CI edge (2166ms on PR #1233); paydown owned by R1C-E emit-gates runner/shared-setup work, not this impossible-bugs row-removal slice.
r3_verification_l4_l7_l5_skeleton_test::r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval # R3-V L4 W1 direct consumer fixture runs the full emit-vs-eval suite through TestRunner and can sit just above 2s on CI (2072ms on PR #1799); paydown owned by R3-V L4/L7 direct harness shared runner setup, see docs/briefs/r3-v-l4-l7-direct-w1-consumer-spec.md.

bootstrap::tests::kernel_bool_path_a_attaches_diagnostic_when_boolean_algebra_unresolvable # Lane 1e-2b Path A regression: two `Dag::new()` paths + mutation; can exceed 2s wall on cold ubuntu-latest when compiled alongside heavy integration neighbors — keep explicit bootstrap diagnostic coverage. Paydown trigger: when the Bool/`BooleanAlgebra` kernel bootstrap bridge dissolves into `dsl/std/types.dag` (see `bootstrap.rs` + `dsl/std/types.dag` dissolution notes), collapse fixtures and/or adopt shared `Dag::new` warming; re-measure and remove if under 2s.

Expand Down
3 changes: 2 additions & 1 deletion src/v3/compiler/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,7 @@ mod t_demo_fixture_test {
use std::fs;
use std::path::PathBuf;

use crate::common::cached_compile_to_dag;
use v3_compiler::compile_to_dag;
use v3_compiler::dag::Dag;
use v3_compiler::test_runner::{ClaimResult, TestRunner};
Expand All @@ -224,7 +225,7 @@ mod t_demo_fixture_test {
}

fn compile_fixture(source: &str) -> Dag {
crate::common::cached_compile_to_dag(source, FIXTURE)
cached_compile_to_dag(source, FIXTURE)
}

#[test]
Expand Down
Loading