1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
/// Falsifiable claim structure
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct FalsifiableClaim {
/// Human-readable hypothesis
pub hypothesis: String,
/// Method to attempt falsification
pub falsification_method: FalsificationMethod,
/// Evidence required to validate
pub evidence_required: EvidenceType,
/// Result of falsification attempt
pub result: Option<FalsificationResult>,
/// Optional override (requires justification AND ticket)
pub override_info: Option<OverrideInfo>,
}
/// Information for an override (Popperian "Immunizing Stratagem")
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct OverrideInfo {
/// Reason for the override
pub reason: String,
/// Mandatory ticket ID (e.g., DEBT-123)
pub ticket_id: String,
/// Timestamp of override
pub timestamp: chrono::DateTime<chrono::Utc>,
}
/// Methods for attempting to falsify claims
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
pub enum FalsificationMethod {
/// Try to find files in baseline missing from completion
ManifestIntegrity,
/// Try to find uncovered lines in changed code
DifferentialCoverage,
/// Try to find total coverage below threshold
AbsoluteCoverage,
/// Try to find TDG score regression
TdgRegression,
/// Try to find complexity regression
ComplexityRegression,
/// Try to find file size regression
FileSizeRegression,
/// Try to find spec score below threshold
SpecQuality,
/// Try to find roadmap not updated
RoadmapUpdate,
/// Try to find unpushed commits
GitHubSync,
/// Try to find #[cfg(not(coverage))] gaming
CoverageGaming,
/// Try to find vulnerable dependencies added (New in v1.1)
SupplyChainIntegrity,
/// Try to find flaws in the falsifier itself (Meta-Check) (New in v1.1)
MetaFalsification,
/// Try to find examples that don't compile/run (New in v1.2)
ExamplesCompile,
/// Try to find pmat-book validation failures (New in v1.2)
BookValidation,
/// Try to find new SATD markers (TODO/FIXME/HACK) (New in v2.6 - comply spec)
SatdDetection,
/// Try to find new dead code (unreachable functions/modules) (New in v2.6 - comply spec)
DeadCodeDetection,
/// Try to find files below 95% coverage threshold (New in v2.6 - comply spec)
PerFileCoverage,
/// Try to find lint failures (make lint) (New in v2.6 - comply spec)
LintPass,
/// Try to find untested match arm variants (New in v3.1 - defect churn)
VariantCoverage,
/// Try to find consecutive fix-commit chains (New in v3.1 - defect churn)
FixChainLimit,
/// Try to find cross-crate integration failures (New in v3.1 - defect churn)
CrossCrateParity,
/// Try to find performance regressions via benchmark gate (New in v3.1 - defect churn)
RegressionGate,
/// Try to find incomplete proofs (sorry) in Lean 4 projects (New in v4.0 - provable contracts)
FormalProofVerification,
/// Execute a specific falsification test from a provable-contracts YAML
/// (Component 29 §Schema Extension). Seeded automatically by Component 27
/// binding; manual additions/removals are blocked by CB-1624.
///
/// `expected` is canonical JSON of the YAML test's `expected` field at
/// bind time. CB-1621 compares it against the current YAML value to
/// detect silent drift.
ProvableContract {
/// Resolved YAML file, e.g. `contracts/rope-kernel-v1.yaml`.
yaml_path: std::path::PathBuf,
/// Equation key within the YAML, e.g. `rope`.
equation: String,
/// Test id from `falsification_tests[]`, e.g. `rope_periodicity_test`.
test_id: String,
/// Canonical JSON snapshot of the test's `expected` field.
expected: String,
},
}
/// Evidence types for falsification
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum EvidenceType {
/// Numeric comparison (actual vs threshold)
NumericComparison { actual: f64, threshold: f64 },
/// File list (missing/added/modified)
FileList(Vec<PathBuf>),
/// Concrete counter-example details (better than boolean)
CounterExample { details: String },
/// Boolean check (Legacy, prefer CounterExample)
BooleanCheck(bool),
/// Git state
GitState {
unpushed_commits: usize,
dirty_files: usize,
},
}
/// Result of a falsification attempt
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct FalsificationResult {
/// Did falsification succeed (found a problem)?
pub falsified: bool,
/// Evidence that caused falsification
pub evidence: Option<EvidenceType>,
/// Human-readable explanation
pub explanation: String,
}
impl FalsificationResult {
/// Create a passing result (hypothesis holds)
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn passed(explanation: impl Into<String>) -> Self {
Self {
falsified: false,
evidence: None,
explanation: explanation.into(),
}
}
/// Create a failing result (hypothesis falsified)
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn failed(explanation: impl Into<String>, evidence: EvidenceType) -> Self {
Self {
falsified: true,
evidence: Some(evidence),
explanation: explanation.into(),
}
}
}