Add fixture-level formal compliance tests for Monte Carlo forecast engine (FC-P3/P4/P6/P8/P9/P10) - #48936
Merged
Conversation
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Copilot
AI
changed the title
[WIP] Update formal model and test suite for compliance fixtures
Add fixture-level formal compliance tests for Monte Carlo forecast engine (FC-P3/P4/P6/P8/P9/P10)
Jul 29, 2026
pelikhan
marked this pull request as ready for review
July 29, 2026 16:15
Contributor
There was a problem hiding this comment.
Pull request overview
Adds formal fixture-level compliance tests for Monte Carlo forecast inputs.
Changes:
- Validates zero-, high-ET, and failed-run fixtures.
- Adds serialization, timestamp-ordering, and input-completeness checks.
- Documents FC-P3/P4/P6/P8/P9/P10 predicates.
Show a summary per file
| File | Description |
|---|---|
pkg/cli/forecast_compliance_fixtures_formal_test.go |
Adds fixture compliance tests and predicate documentation. |
Review details
Tip
Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Files reviewed: 1/1 changed files
- Comments generated: 3
- Review effort level: Medium
Comment on lines
+517
to
+528
| assert.Equal(t, original.CLIVersion, roundTripped.CLIVersion, | ||
| "FC-P8: CLIVersion must survive round-trip") | ||
| assert.Equal(t, original.RunID, roundTripped.RunID, | ||
| "FC-P8: RunID must survive round-trip") | ||
| assert.Equal(t, original.ProcessedAt.UTC(), roundTripped.ProcessedAt.UTC(), | ||
| "FC-P8: ProcessedAt must survive round-trip") | ||
| assert.Equal(t, original.Run.Conclusion, roundTripped.Run.Conclusion, | ||
| "FC-P8: Run.Conclusion must survive round-trip") | ||
| assert.Equal(t, original.Run.StartedAt.UTC(), roundTripped.Run.StartedAt.UTC(), | ||
| "FC-P8: Run.StartedAt must survive round-trip") | ||
| assert.Equal(t, original.Run.UpdatedAt.UTC(), roundTripped.Run.UpdatedAt.UTC(), | ||
| "FC-P8: Run.UpdatedAt must survive round-trip") |
Comment on lines
+551
to
+554
| startedStr, ok := run["run_started_at"].(string) | ||
| require.True(t, ok, "FC-P9: run.run_started_at must be a string in %s", name) | ||
| updatedStr, ok := run["updated_at"].(string) | ||
| require.True(t, ok, "FC-P9: run.updated_at must be a string in %s", name) |
Comment on lines
+601
to
+603
| runID, ok := runIDRaw.(float64) | ||
| require.True(t, ok, "FC-P10: run_id must be a number in %s", tc.name) | ||
| assert.NotEqual(t, 0.0, runID, "FC-P10: run_id must be non-zero in %s", tc.name) |
Contributor
|
🎉 This pull request is included in a new release. Release: |
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.
The formal spec (issue #48935) identified six fixture-level predicates from the behavioral coverage map that were absent from the existing
forecast_compliance_fixtures_formal_test.gotest suite — which covered Monte Carlo engine internals (P1–P13) but never directly loaded and validated the four JSON fixture files themselves.Added tests
Six new
TestFormal_FC_P*tests appended to the existing file, all in packagecli:TestFormal_FC_P3_ZeroETFixturerun_summary_zero_et.json→total_effective_tokens == 0TestFormal_FC_P4_HighETFixturerun_summary_high_et.json→total_effective_tokens >= 1,000,000TestFormal_FC_P6_FailedRunFixturerun_summary_failed.json→run.conclusion == "failure"TestFormal_FC_P8_RunSummaryRoundTripRunSummaryJSON marshal → unmarshal is losslessTestFormal_FC_P9_TimestampOrderingrun_started_at ≤ updated_atacross all four fixturesTestFormal_FC_P10_MonteCarloInputCompletenessrun_id,run.conclusion, andtotal_aic; skips gracefully if a fixture file is missingUpdated the package-level comment to document the new FC-P* predicate group alongside the existing TLA+/F*/Z3 families.