IR-496: Generate bounded flat function schedules

reviews/ir-496-code-review.md

@@ -4,7 +4,7 @@ title: "IR-496 PR 367 code review and Rust lane"
 type: SpecReview
 analysis: code-review
 review_set: subset
-scope: "agent-ix/quire-contract-codegen@0ce345ff1fb66f6bd9c5a445aeb6411cb9720a4b; src/lib.rs, src/oracle/function/mod.rs, src/oracle/function/schedule.rs, tests/checked_package_support/rekey.rs, tests/it/exact_function_generation.rs; FR-021-AC-24..27, AC-34"
+scope: "agent-ix/quire-contract-codegen@fc150dc6aa02e022ab63d4097b3eeb78c1adc1eb; src/lib.rs, src/oracle/function/mod.rs, src/oracle/function/schedule.rs, tests/checked_package_support/rekey.rs, tests/it/exact_function_generation.rs; FR-021-AC-24..27, AC-34"
 relationships:
   - { target: "ix://agent-ix/quire-contract-codegen/FR-021", type: references }
 ---
@@ -38,3 +38,13 @@ Reviewed public PR #367 at `0ce345ff1fb66f6bd9c5a445aeb6411cb9720a4b` against `o
 - FND-006: fixed at `6b61567cea79b1e246d6a87eb5941979c6e650a`.
 
 The same-reviewer delta review of `6b61567cea79b1e246d6a87eb5941979c6e650a` found all six findings fixed. This scoped seed does not claim FR-021-AC-7's 100K schedule acceptance or AC-28.
+
+## Current-head review record
+
+Reviewed exact clean head `fc150dc6aa02e022ab63d4097b3eeb78c1adc1eb` against `origin/main` at `701ac65f8b8360236b1b48ca3f549d726a180100`. The diff contains `src/lib.rs`, `src/oracle/function/mod.rs`, `src/oracle/function/schedule.rs`, and `tests/it/exact_function_generation.rs`. The merged IR-764 checked-package support is base context, not a changed file.
+
+**Current-head verdict: PASS — no new code or Rust findings.** The original FND-001..006 rows and their fixed dispositions above are historical and remain unchanged. Source review confirms the current public path meters projection node/edge work before scheduling; preserves scalar literal values and equality operation identities; sorts claims by declaration identity before names and deduplicates requests; and includes explicit charge-boundary control-flow operations. The new source-limit path checks total root-plus-module bytes before returning a generation result, enforces per-artifact and bundle ceilings, and partitions large schedules into deterministic ordinal modules. The 100,000-call tests include exact and one-less work/query/source controls, a 512 KiB worker stack, and generated-crate compilation assertions.
+
+Current acceptance criteria examined: FR-021-AC-7 (deep 100K schedule, raised source limit and compile), AC-15 (constant-size location records and charged path query), AC-24 (claim ordering/deduplication), AC-25 (pre-action charges and all-or-nothing schedule), AC-26 (left-stop charge order), AC-27 (bound calls/cycle/shared-node refusals), AC-28 (source ceiling and raised-limit outputs), AC-29 (linear parent-chain path), and AC-34 (strict-reader chain control). AC-18 was read as context only; its QSL agreement leg remains outside this diff.
+
+No Cargo, Kani, integration test, or other gate was run, per dispatch. This is source review only; assertions in the test source were inspected but not executed.

reviews/ir-496-gap-analysis.md

@@ -3,7 +3,7 @@ id: SR-8641
 title: "IR-496 PR 367 gap analysis"
 type: SpecReview
 analysis: gap-analysis
-scope: "agent-ix/quire-contract-codegen@0ce345ff1fb66f6bd9c5a445aeb6411cb9720a4b; spec/, src/, tests/"
+scope: "agent-ix/quire-contract-codegen@fc150dc6aa02e022ab63d4097b3eeb78c1adc1eb; spec/, src/, tests/"
 review_set: subset
 relationships:
   - { target: "ix://agent-ix/quire-contract-codegen/FR-021", type: references }
@@ -22,6 +22,7 @@ Planless repository matrix and reverse-gap audit, with focused source/test inspe
 | ID | Severity | Summary | Refs |
 | --- | --- | --- | --- |
 | FND-001 | high | The computed matrix has 323 untagged criteria; the changed FR-021 slice leaves AC-26 and AC-28 without a bound test | FR-021-AC-26, FR-021-AC-28 |
+| FND-002 | high | The repository-wide computed matrix has 318 untagged criteria; AC-18 remains an untagged QSL-owned planned criterion outside this diff, and no changed-scope FR-021 criterion is untagged | computed matrix; FR-021-AC-18 |
 
 ## Coverage
 
@@ -36,3 +37,17 @@ Planless repository matrix and reverse-gap audit, with focused source/test inspe
 - Changed-scope AC-26: fixed at `6b61567cea79b1e246d6a87eb5941979c6e650a`; explicit charge-before-action branches and denied-charge-to-Stop behavior are covered.
 - AC-28: deferred outside this scoped seed PR. The source ceiling remains unchanged, and this PR does not claim raised-limit/deep-body acceptance.
 - Repository-wide matrix: the original 323-untagged-criteria FAIL is retained from the review baseline and was not recomputed for this delta. It is not evidence that this scoped PR introduces 323 gaps.
+
+## Current-head audit record
+
+Exact clean head `fc150dc6aa02e022ab63d4097b3eeb78c1adc1eb` was audited against base `701ac65f8b8360236b1b48ca3f549d726a180100`; production change scope is the function schedule generator and its integration/unit coverage. The computed Quoin matrix has 738 criteria: 368 tagged, 318 untagged, 11 tagged-by-ignored-test, and 41 method-without-symbol. This aggregate remains a repository-wide FAIL, with many untagged criteria outside the changed feature. The historical FND-001 count of 323 and its disposition above are preserved as the PR #367 baseline record.
+
+**Current changed-scope assessment: PASS for the reviewed FR-021 schedule slice.** The current computed matrix tags FR-021-AC-7, AC-15, AC-24, AC-25, AC-26, AC-27, AC-28, AC-29, and AC-34. AC-18 is still untagged, but its QSL-owned agreement is explicitly PLANNED and this diff does not claim that leg. The new public integration test directly exercises AC-7/AC-28 with an authentic checked graph, a 512 KiB generation worker, default source-limit refusal, caller-raised exact source limit, exact/one-less limits, module artifact ceilings, and compilation assertions. Static review confirms the tagged test builds the graph through strict admission and invokes the public API.
+
+The original changed-scope AC-26 disposition remains fixed at `6b61567cea79b1e246d6a87eb5941979c6e650a`; AC-28's prior deferred disposition is superseded for this current head by the new AC-28 coverage in this changed scope. The global matrix result is still FAIL; current changed-scope gaps identified: none. Reverse-gap source review: new public limits/API and module output behavior are owned by FR-021; changed source/test stubs found: 0.
+
+- Reconciliation evidence: `quoin matrix --repo /home/peter/dev/worktrees/ir496-deep-schedule --json` (captured as `/tmp/ir496-review-fc150dc/quoin-matrix.json`) and `quire coverage --scope /home/peter/dev/worktrees/ir496-deep-schedule --json` (captured as `/tmp/ir496-review-fc150dc/quire-coverage.json`). Quoin reports no run evidence.
+- Reverse-gap inventory was bounded to the changed public API, implementation and test paths; no unowned changed behavior or stubs were identified.
+- Plan completion: not assessed
+- Semantic review: skipped; not requested.
+- No Cargo/Kani/tests/full gates were run.

src/lib.rs

@@ -76,24 +76,26 @@ pub use oracle::equality::{
 };
 
 pub use oracle::function::{
-    generate_exact_function_oracles, generate_function_schedules, CallPointKind, ExactFunctionBody,
-    ExactFunctionClaim, ExactFunctionDeclaration, ExactFunctionItem, ExactFunctionOracles,
-    ExactFunctionRefusal, FunctionParameter, FunctionScheduleClaim, FunctionScheduleDeclaration,
+    generate_exact_function_oracles, generate_function_schedules,
+    generate_function_schedules_with_limits, CallPointKind, ExactFunctionBody, ExactFunctionClaim,
+    ExactFunctionDeclaration, ExactFunctionItem, ExactFunctionOracles, ExactFunctionRefusal,
+    FunctionParameter, FunctionScheduleClaim, FunctionScheduleDeclaration,
     FunctionScheduleDisposition, FunctionScheduleGeneration, FunctionScheduleItem,
-    FunctionScheduleParameter, GeneratedExactFunctionClaim, LocationMapEntry, RecordedLocation,
-    RecordedOrigin, RefusedFunctionBody, ScheduledFunctionBody, EXACT_FUNCTION_CRATE_NAME,
-    EXACT_FUNCTION_LOWERING_WORK_LIMIT,
+    FunctionScheduleLimits, FunctionScheduleParameter, GeneratedExactFunctionClaim,
+    LocationMapEntry, RecordedLocation, RecordedOrigin, RefusedFunctionBody, ScheduledFunctionBody,
+    EXACT_FUNCTION_CRATE_NAME, EXACT_FUNCTION_LOWERING_WORK_LIMIT,
 };
 
 pub use oracle::function::schedule::{
     BlockId as FunctionScheduleBlockId, ControlAction as FunctionScheduleControlAction,
     ControlBlock as FunctionScheduleControlBlock, ControlEdge as FunctionScheduleControlEdge,
     EdgeCondition as FunctionScheduleEdgeCondition, Instruction as FunctionScheduleInstruction,
+    LocationQueryRefusal as FunctionScheduleLocationQueryRefusal,
     LocationRecord as FunctionScheduleLocation, Occurrence as FunctionScheduleOccurrence,
     Operand as FunctionScheduleOperand, Operation as FunctionScheduleOperation,
     Schedule as FunctionBodySchedule, ScheduleRefusal as FunctionScheduleRefusal,
     ScheduledOperation as FunctionScheduledOperation, SsaSlot as FunctionScheduleSlot,
-    ValueKind as FunctionScheduleValueKind,
+    ValueKind as FunctionScheduleValueKind, DEFAULT_GENERATION_WORK_LIMIT,
 };
 
 pub use evidence::bound_coverage::{