Skip to content

InputEnvelope: first-class bounded input for WorkDemand + CI corpus instance - #5801

Merged
briansrls merged 5 commits into
mainfrom
input-envelope-p1
Jun 25, 2026
Merged

briansrls merged 5 commits into
mainfrom
input-envelope-p1

Conversation

@briansrls

@briansrls briansrls commented Jun 25, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Models the InputEnvelope as a first-class fact on WorkDemand, mirroring DescentEvidence from std/induction.dag. An unbounded input is the data-side of a non-terminating Loop; a WorkDemand without a declared input ceiling is therefore fail-open by construction. BoundedInput is the declared ceiling (analog of Strict); EnvelopeUnknown is the honest fail-closed bottom (analog of DescentUnknown).

What changed

  • InputSizeAxis closed enum: WitnessCount | SourceNodeCount | CorpusNodeCount
  • InputBound record: axis: InputSizeAxis, max: Measure<Count, One, Nat>
  • InputEnvelope coproduct: BoundedInput { bounds: List<InputBound> } | EnvelopeUnknown
  • AdmissionVerdict: Admitted | RefusedOverEnvelope { axis } | RefusedUndeclared
  • input_admitted fn: EnvelopeUnknown => RefusedUndeclared; undeclared axis and over-ceiling both => RefusedOverEnvelope; all within => Admitted
  • WorkDemand.input_envelope required field added; all 4 existing WorkDemand data declarations updated to carry EnvelopeUnknown (honest: ceiling not yet declared)
  • gunbc_ci_corpus_envelope: CI corpus as first BoundedInput instance (P1 scaffold — ceilings are operator-set operating-point values, NOT derived quantities; P2 derives them)
  • input_envelope_admission_test.dag: 6 test functions, all green by execution
  • input_envelope_roadmap.dag: grounds the P1/P2 plan as a .dag Plan authority

Ceiling values (P1 scaffold — operator sign-off needed before P2 locks them)

Axis Ceiling value Disposition
WitnessCount 2000 Scaffold — operator-set ceiling, not derived
SourceNodeCount 500000 Scaffold — operator-set ceiling, not derived
CorpusNodeCount 5000000 Scaffold — operator-set ceiling, not derived

Test plan

# All 6 test fns run green by execution:
./target/release/gunbc run --source-root dsl --source-root src/v2 \
  --entry dsl/test/claim/input_envelope_admission_test.dag \
  --function admitted_when_actual_at_envelope --claim-run   # true
./target/release/gunbc run ... --function refused_when_actual_over_envelope --claim-run   # true
./target/release/gunbc run ... --function refused_when_actual_axis_not_declared --claim-run  # true
./target/release/gunbc run ... --function refused_undeclared_when_envelope_unknown --claim-run  # true
./target/release/gunbc run ... --function red_on_revert_bound_change --claim-run  # true
./target/release/gunbc run ... --function ci_corpus_envelope_is_bounded --claim-run  # true

# Full compile: 604 files emitted, 0 diagnostics
./target/release/gunbc compile --output-dir /tmp/out --dependency-pool-index primary-precedence \
  --source-root dsl --source-root src/v2

Kept draft: ceiling values need operator sign-off before locking (per brief from sharp-stag-782).

@gunbai-bot gunbai-bot Bot changed the title P1: InputEnvelope fact + CI corpus envelope InputEnvelope: first-class bounded input for WorkDemand + CI corpus instance Jun 25, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 25, 2026 03:57
@gunbai-bot gunbai-bot Bot mentioned this pull request Jun 25, 2026
6 tasks
Brian Searls and others added 3 commits June 25, 2026 04:04
…alues

The ceiling values (2000/500000/5000000) are operator-set P1 scaffolds; P2
derives them from corpus discovery. Since .dag has no comment syntax, add an
explicit Scaffold Disposition data declaration bound to the input_envelope_roadmap
plan so the values are not read as authoritative measurements.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
input_bound was defined but not called anywhere in the diff;
test file constructs InputBound records directly.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls
briansrls merged commit e789f34 into main Jun 25, 2026
1 of 2 checks passed
@briansrls
briansrls deleted the input-envelope-p1 branch June 25, 2026 04:43
briansrls added a commit that referenced this pull request Jun 25, 2026
…locks fleet) (#5821)

* Fix main CI floor: orphan-doc reachability + inline-shell roster (unblocks fleet)

Two discovery witnesses are RED on main, inherited by every PR (jointly,
not from any single PR's own diff):

1. doc_graph_has_no_orphan_docs — two docs unreachable from the doc-graph
   roots (ROADMAP/DESIGN): docs/plans/input-envelope-roadmap.md (#5801) and
   docs/plans/resource-aware-scheduler.md. Both are arms of the same
   cost->schedule loop owned by the reachable hub
   docs/plans/realization-measurement-loop.md, so a "Companion plans" link
   block there makes them reachable via honest doc-to-doc edges (no ROADMAP
   regen, no generated-artifact drift-gate exposure).

2. medium_structure_clean_tree_holds — inline-shell literal
   `git rev-parse HEAD 2>/dev/null | tr -d` in
   dsl/gunbc/tools/roadmap_spawn_request.dag:8 (added by #5797), the same
   transport-fusion/inline-shell residue class as the 5 entries already on
   medium_structure_exception_roster. Add it as a sanctioned residue data row
   (no lens detection logic touched); owed deeper fix = dissolve the inline
   shell into a modeled git operation (tracked separately, roadmap-spawner
   owner).

Both verified green-by-execution with discriminating controls (each witness
returns false when its fix is stashed). Greens main's floor → unblocks #5808
and #5772.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* Fix main floor: cite orphan plan docs via .dag authority + roster the roadmap-spawn shell leak

Two discovery witnesses are RED on main and inherited fleet-wide:

1. doc_graph_has_no_orphan_docs — resource-aware-scheduler.md and
   input-envelope-roadmap.md were unreachable from the doc-graph roots.
   Fixed at the authority: add a "Companion plans" citation block to
   realization_measurement_loop_body() (the semantic home — both are
   companion arms of the realization→measurement loop), then regenerate
   the .md byte-faithfully via `main_wet`. Editing the generated .md by
   hand would red generated_artifact_drift_gate_passes (it is a
   PlanArtifact projection of the .dag authority).

2. medium_structure_clean_tree_holds — roadmap_spawn_request.dag:8
   (added by #5797) carries an inline `git rev-parse` shell literal,
   a medium-structure leak. Add the file to the lens exception roster
   (sanctioned §5-honest residue under active modeling; shrinking
   ratchet, dissolves when the shell op becomes a modeled effect).

Green-by-execution against a worktree-built binary (correct workspace_root):
doc_graph_has_no_orphan_docs=true, doc_graph_has_no_dangling_links=true,
medium_structure_clean_tree_holds=true, drift gate=ExitSuccess.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant