Repository navigation
IR-364: specify non-completed V2 harness result - #578
Merged
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Scope
Resolve FR-002 OQ-2 for V2 harnesses. A non-completed clause oracle returns CG-owned
V2HarnessCaseResult::NonCompletedwith the original typedOutcomestop or outerClauseStop, the exact selected claim, and its accepted typed execution point. The generated campaign returnsV2HarnessCampaignResult::NonCompleted; no runtime verdict is constructed or recorded.FR-002-AC-16 is strengthened; AC-17/18 remain unchanged. New AC-24 defines the already-at-limit report case. TC-004 seeds every stop variant at both oracle positions, checks the selected identity and cause, and tests the at-limit summary observation. The strategy test matrix traces AC-24 to TC-004.
Accounting boundary
CampaignCounts::total()saturates on overflow, andCampaignSnapshot::at_limit()says the counters may already have saturated. For an unsaturated prior report, the CG V2 harness summary counts the stopped case once as attempted and non-completed while leaving runtime verdict counters unchanged. For an at-limit prior report, its exactattempted: Option<u64>isNoneandnon_completedis one; it does not invent a prior exact total. TC-004 exercises that branch through the internal runtime-snapshot read seam.FR-012-AC-4 belongs to the FR-011 numeric strategy/shrinking runner, which requires every oracle evaluation and shrink replay in its attempted count. FR-011 states its rate accessors are strategy-bundle-only and the harness summary is unchanged. This PR specifies a distinct FR-002 V2 pre/post subject-harness summary and does not change FR-011/FR-012 numeric accounting or RT. FR-011's existing at-limit rule makes its discard/rejection rates unavailable; it is not a source of an exact saturated history for this new harness.
Verification
quire validate --scope .over FR-002, TC-004, and strategytests.mdpassed (existing module warnings only).git diff --checkpassed.IR-364 stays open: V2 code and tests remain, with execution-point implementation blocked by QSL-1082 and IR-1013. This is a spec-only draft.