1use std::collections::{BTreeMap, BTreeSet};
2
3use chrono::{DateTime, Utc};
4use serde::{Deserialize, Serialize};
5use serde_json::Value;
6use thiserror::Error;
7use uuid::Uuid;
8
9use crate::{SCHEMA_VERSION, hash_bytes, hash_json};
10
11#[derive(Debug, Clone, Copy, Default, Serialize, Deserialize, PartialEq, Eq)]
13#[serde(rename_all = "snake_case")]
14pub enum ClaimScope {
15 #[default]
17 Runtime,
18 Task,
20}
21
22#[derive(Debug, Clone, Copy, Default, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
24#[serde(rename_all = "snake_case")]
25pub enum AssuranceLevel {
26 #[default]
28 Recorded,
29 Observed,
31 Isolated,
33 IndependentlyReproduced,
35}
36
37#[derive(Debug, Clone, Copy, Default, Serialize, Deserialize, PartialEq, Eq)]
39#[serde(rename_all = "snake_case")]
40pub enum EvidenceFreshness {
41 #[default]
43 Any,
44 FinalWorkspaceGeneration,
46 FinalWorkspaceState,
48}
49
50#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
52#[serde(rename_all = "camelCase")]
53pub struct EvidenceRequirement {
54 #[serde(default)]
56 pub allowed_kinds: BTreeSet<EvidenceKind>,
57 #[serde(default)]
59 pub allowed_producers: BTreeSet<String>,
60 #[serde(default = "one")]
62 pub minimum_observations: u32,
63 #[serde(default)]
65 pub freshness: EvidenceFreshness,
66 #[serde(default)]
68 pub require_artifacts: bool,
69 #[serde(default = "one")]
71 pub minimum_independent_producers: u32,
72 #[serde(default)]
74 pub minimum_assurance: AssuranceLevel,
75}
76
77impl Default for EvidenceRequirement {
78 fn default() -> Self {
79 Self {
80 allowed_kinds: BTreeSet::new(),
81 allowed_producers: BTreeSet::new(),
82 minimum_observations: 1,
83 freshness: EvidenceFreshness::Any,
84 require_artifacts: false,
85 minimum_independent_producers: 1,
86 minimum_assurance: AssuranceLevel::Recorded,
87 }
88 }
89}
90
91impl EvidenceRequirement {
92 pub fn task() -> Self {
94 Self {
95 allowed_kinds: [EvidenceKind::Tool, EvidenceKind::Process, EvidenceKind::Git]
96 .into_iter()
97 .collect(),
98 minimum_assurance: AssuranceLevel::Observed,
99 ..Self::default()
100 }
101 }
102
103 pub fn runtime_completion() -> Self {
105 Self {
106 allowed_kinds: [EvidenceKind::Runtime].into_iter().collect(),
107 allowed_producers: ["proofborne.runtime".to_owned()].into_iter().collect(),
108 minimum_assurance: AssuranceLevel::Observed,
109 ..Self::default()
110 }
111 }
112}
113
114#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
116#[serde(rename_all = "camelCase")]
117pub struct TaskContract {
118 pub schema_version: String,
120 pub id: Uuid,
122 pub goal: String,
124 #[serde(default)]
126 pub claim_scope: ClaimScope,
127 #[serde(default)]
129 pub constraints: Vec<String>,
130 pub criteria: Vec<Criterion>,
132 pub created_at: DateTime<Utc>,
134 pub confirmed: bool,
136}
137
138impl TaskContract {
139 pub fn new(goal: impl Into<String>, criteria: Vec<Criterion>) -> Self {
141 Self {
142 schema_version: SCHEMA_VERSION.to_owned(),
143 id: Uuid::now_v7(),
144 goal: goal.into(),
145 claim_scope: ClaimScope::Task,
146 constraints: Vec::new(),
147 criteria,
148 created_at: Utc::now(),
149 confirmed: false,
150 }
151 }
152
153 pub fn automatic(goal: impl Into<String>) -> Self {
159 let mut runtime_criterion = Criterion::required(
160 "runtime_completed",
161 "The agent loop completed without an unhandled runtime error",
162 );
163 runtime_criterion.evidence_requirement = EvidenceRequirement::runtime_completion();
164 let mut contract = Self::new(goal, vec![runtime_criterion]);
165 contract.claim_scope = ClaimScope::Runtime;
166 contract.confirmed = true;
167 contract.constraints.push(
168 "Runtime completion evidence does not imply task or program correctness".to_owned(),
169 );
170 contract
171 }
172
173 pub fn validate(&self) -> Result<(), ProofError> {
175 if self.goal.trim().is_empty() {
176 return Err(ProofError::InvalidContract(
177 "goal must not be empty".to_owned(),
178 ));
179 }
180 if self.criteria.is_empty() {
181 return Err(ProofError::InvalidContract(
182 "at least one acceptance criterion is required".to_owned(),
183 ));
184 }
185 if !self.criteria.iter().any(|criterion| criterion.required) {
186 return Err(ProofError::InvalidContract(
187 "at least one required acceptance criterion is required".to_owned(),
188 ));
189 }
190
191 let mut ids = BTreeSet::new();
192 for criterion in &self.criteria {
193 if criterion.id.trim().is_empty() || criterion.description.trim().is_empty() {
194 return Err(ProofError::InvalidContract(
195 "criterion id and description must not be empty".to_owned(),
196 ));
197 }
198 if !ids.insert(&criterion.id) {
199 return Err(ProofError::DuplicateCriterion(criterion.id.clone()));
200 }
201 criterion.validate_requirement()?;
202 match (criterion.state, criterion.waiver.as_ref()) {
203 (CriterionState::Waived, Some(waiver))
204 if waiver.actor.trim().is_empty() || waiver.reason.trim().is_empty() =>
205 {
206 return Err(ProofError::InvalidContract(format!(
207 "criterion {} has incomplete waiver metadata",
208 criterion.id
209 )));
210 }
211 (CriterionState::Waived, None) => {
212 return Err(ProofError::InvalidContract(format!(
213 "criterion {} is waived without waiver metadata",
214 criterion.id
215 )));
216 }
217 (
218 CriterionState::Pending | CriterionState::Passed | CriterionState::Failed,
219 Some(_),
220 ) => {
221 return Err(ProofError::InvalidContract(format!(
222 "criterion {} has waiver metadata but is not waived",
223 criterion.id
224 )));
225 }
226 _ => {}
227 }
228 }
229
230 if self.claim_scope == ClaimScope::Task {
231 if !self
232 .criteria
233 .iter()
234 .filter(|criterion| criterion.required)
235 .any(|criterion| {
236 !criterion.evidence_requirement.allowed_kinds.is_empty()
237 && criterion
238 .evidence_requirement
239 .allowed_kinds
240 .iter()
241 .any(|kind| {
242 matches!(
243 kind,
244 EvidenceKind::Tool | EvidenceKind::Process | EvidenceKind::Git
245 )
246 })
247 })
248 {
249 return Err(ProofError::InvalidContract(
250 "a task-scoped contract requires task-capable evidence; runtime-only criteria cannot prove a task"
251 .to_owned(),
252 ));
253 }
254
255 for criterion in self.criteria.iter().filter(|criterion| criterion.required) {
256 if criterion.evidence_requirement.allowed_producers.is_empty() {
257 return Err(ProofError::InvalidContract(format!(
258 "required task criterion {} must name at least one allowed producer",
259 criterion.id
260 )));
261 }
262 if criterion.evidence_requirement.freshness == EvidenceFreshness::Any {
263 return Err(ProofError::InvalidContract(format!(
264 "required task criterion {} must bind evidence to the final workspace generation or state",
265 criterion.id
266 )));
267 }
268 }
269 }
270 Ok(())
271 }
272
273 pub fn waive(
275 &mut self,
276 criterion_id: &str,
277 actor: impl Into<String>,
278 reason: impl Into<String>,
279 ) -> Result<(), ProofError> {
280 let criterion = self
281 .criteria
282 .iter_mut()
283 .find(|criterion| criterion.id == criterion_id)
284 .ok_or_else(|| ProofError::UnknownCriterion(criterion_id.to_owned()))?;
285 let actor = actor.into();
286 if actor.trim().is_empty() {
287 return Err(ProofError::InvalidContract(
288 "waiver actor must not be empty".to_owned(),
289 ));
290 }
291 let reason = reason.into();
292 if reason.trim().is_empty() {
293 return Err(ProofError::EmptyWaiverReason);
294 }
295 criterion.state = CriterionState::Waived;
296 criterion.waiver = Some(Waiver {
297 actor,
298 reason,
299 at: Utc::now(),
300 });
301 Ok(())
302 }
303}
304
305#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
307#[serde(rename_all = "camelCase")]
308pub struct Criterion {
309 pub id: String,
311 pub description: String,
313 pub required: bool,
315 #[serde(default = "one")]
320 pub minimum_evidence: u32,
321 #[serde(default)]
323 pub evidence_requirement: EvidenceRequirement,
324 pub state: CriterionState,
326 #[serde(default)]
328 pub evidence_ids: Vec<Uuid>,
329 #[serde(skip_serializing_if = "Option::is_none")]
331 pub waiver: Option<Waiver>,
332}
333
334impl Criterion {
335 pub fn required(id: impl Into<String>, description: impl Into<String>) -> Self {
337 Self {
338 id: id.into(),
339 description: description.into(),
340 required: true,
341 minimum_evidence: 1,
342 evidence_requirement: EvidenceRequirement::task(),
343 state: CriterionState::Pending,
344 evidence_ids: Vec::new(),
345 waiver: None,
346 }
347 }
348
349 pub fn optional(id: impl Into<String>, description: impl Into<String>) -> Self {
351 Self {
352 required: false,
353 ..Self::required(id, description)
354 }
355 }
356
357 fn validate_requirement(&self) -> Result<(), ProofError> {
358 let requirement = &self.evidence_requirement;
359 if self.minimum_evidence == 0 || requirement.minimum_observations == 0 {
360 return Err(ProofError::InvalidContract(format!(
361 "criterion {} requires at least one observation",
362 self.id
363 )));
364 }
365 if requirement.minimum_independent_producers == 0 {
366 return Err(ProofError::InvalidContract(format!(
367 "criterion {} requires at least one independent producer",
368 self.id
369 )));
370 }
371 if requirement
372 .allowed_producers
373 .iter()
374 .any(|producer| producer.trim().is_empty())
375 {
376 return Err(ProofError::InvalidContract(format!(
377 "criterion {} contains an empty allowed producer",
378 self.id
379 )));
380 }
381 Ok(())
382 }
383}
384
385const fn one() -> u32 {
386 1
387}
388
389#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq)]
391#[serde(rename_all = "snake_case")]
392pub enum CriterionState {
393 Pending,
395 Passed,
397 Failed,
399 Waived,
401}
402
403#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
405#[serde(rename_all = "camelCase")]
406pub struct Waiver {
407 pub actor: String,
409 pub reason: String,
411 pub at: DateTime<Utc>,
413}
414
415#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
417#[serde(rename_all = "camelCase")]
418pub struct Evidence {
419 pub id: Uuid,
421 pub kind: EvidenceKind,
423 pub producer: String,
425 pub summary: String,
427 #[serde(skip_serializing_if = "Option::is_none")]
429 pub input_hash: Option<String>,
430 #[serde(skip_serializing_if = "Option::is_none")]
432 pub output_hash: Option<String>,
433 #[serde(skip_serializing_if = "Option::is_none")]
435 pub exit_code: Option<i32>,
436 pub success: bool,
438 pub started_at: DateTime<Utc>,
440 pub completed_at: DateTime<Utc>,
442 #[serde(default)]
444 pub artifacts: Vec<ArtifactRef>,
445 pub redacted: bool,
447 #[serde(default)]
449 pub metadata: Value,
450 #[serde(default)]
452 pub assurance_level: AssuranceLevel,
453 #[serde(default, skip_serializing_if = "Option::is_none")]
455 pub attempt_id: Option<Uuid>,
456 #[serde(default, skip_serializing_if = "Option::is_none")]
458 pub attempt_sequence: Option<u32>,
459 #[serde(default, skip_serializing_if = "Option::is_none")]
461 pub action_id: Option<String>,
462 #[serde(default, skip_serializing_if = "Option::is_none")]
464 pub workspace_generation: Option<u64>,
465 #[serde(default, skip_serializing_if = "Option::is_none")]
467 pub state_binding: Option<String>,
468 #[serde(default, skip_serializing_if = "Vec::is_empty")]
470 pub supersedes: Vec<Uuid>,
471}
472
473impl Evidence {
474 pub fn observed(
476 kind: EvidenceKind,
477 producer: impl Into<String>,
478 summary: impl Into<String>,
479 input: Option<&Value>,
480 output: Option<&[u8]>,
481 exit_code: Option<i32>,
482 success: bool,
483 ) -> Self {
484 let now = Utc::now();
485 Self {
486 id: Uuid::now_v7(),
487 kind,
488 producer: producer.into(),
489 summary: summary.into(),
490 input_hash: input.map(hash_json),
491 output_hash: output.map(hash_bytes),
492 exit_code,
493 success,
494 started_at: now,
495 completed_at: now,
496 artifacts: Vec::new(),
497 redacted: false,
498 metadata: Value::Object(serde_json::Map::new()),
499 assurance_level: AssuranceLevel::Observed,
500 attempt_id: None,
501 attempt_sequence: None,
502 action_id: None,
503 workspace_generation: None,
504 state_binding: None,
505 supersedes: Vec::new(),
506 }
507 }
508
509 #[must_use]
511 pub fn with_attempt(mut self, attempt_id: Uuid, sequence: u32) -> Self {
512 self.attempt_id = Some(attempt_id);
513 self.attempt_sequence = Some(sequence);
514 self
515 }
516
517 #[must_use]
519 pub fn with_action(mut self, action_id: impl Into<String>) -> Self {
520 self.action_id = Some(action_id.into());
521 self
522 }
523
524 #[must_use]
526 pub fn bound_to_workspace(mut self, generation: u64, state_binding: Option<String>) -> Self {
527 self.workspace_generation = Some(generation);
528 self.state_binding = state_binding;
529 self
530 }
531
532 #[must_use]
534 pub fn with_assurance(mut self, assurance_level: AssuranceLevel) -> Self {
535 self.assurance_level = assurance_level;
536 self
537 }
538
539 #[must_use]
541 pub fn superseding(mut self, evidence_ids: impl IntoIterator<Item = Uuid>) -> Self {
542 self.supersedes = evidence_ids.into_iter().collect();
543 self
544 }
545}
546
547#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
549#[serde(rename_all = "snake_case")]
550pub enum EvidenceKind {
551 Tool,
553 Context,
555 Routing,
557 Process,
559 Runtime,
561 Git,
563 Human,
565}
566
567#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
569#[serde(rename_all = "camelCase")]
570pub struct ArtifactRef {
571 pub hash: String,
573 pub name: String,
575 #[serde(skip_serializing_if = "Option::is_none")]
577 pub media_type: Option<String>,
578 pub size: u64,
580}
581
582#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
584#[serde(rename_all = "camelCase")]
585pub struct EvidenceLink {
586 pub evidence_id: Uuid,
588 pub criterion_id: String,
590 #[serde(skip_serializing_if = "Option::is_none")]
592 pub rationale: Option<String>,
593}
594
595#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
597#[serde(rename_all = "camelCase")]
598pub struct CriterionEvaluation {
599 pub criterion_id: String,
601 pub state: CriterionState,
603 pub evidence_ids: Vec<Uuid>,
605 pub active_evidence_ids: Vec<Uuid>,
607 pub qualifying_evidence_ids: Vec<Uuid>,
609 pub unresolved_counterevidence_ids: Vec<Uuid>,
611 pub unmet_requirements: Vec<String>,
613}
614
615#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
617#[serde(rename_all = "camelCase")]
618pub struct ProofEvaluation {
619 pub claim_scope: ClaimScope,
621 pub assurance_level: AssuranceLevel,
623 pub outcome: RunOutcome,
625 pub criteria: Vec<CriterionEvaluation>,
627}
628
629#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
631#[serde(rename_all = "camelCase")]
632pub struct ProofGraph {
633 pub schema_version: String,
635 pub contract_id: Uuid,
637 pub evidence: BTreeMap<Uuid, Evidence>,
639 pub links: Vec<EvidenceLink>,
641 #[serde(default, skip_serializing_if = "Option::is_none")]
643 pub final_workspace_generation: Option<u64>,
644 #[serde(default, skip_serializing_if = "Option::is_none")]
646 pub final_state_binding: Option<String>,
647 #[serde(default, skip_serializing_if = "Option::is_none")]
649 pub termination: Option<ProofTermination>,
650}
651
652impl ProofGraph {
653 pub fn new(contract_id: Uuid) -> Self {
655 Self {
656 schema_version: SCHEMA_VERSION.to_owned(),
657 contract_id,
658 evidence: BTreeMap::new(),
659 links: Vec::new(),
660 final_workspace_generation: None,
661 final_state_binding: None,
662 termination: None,
663 }
664 }
665
666 pub fn bind_final_workspace(&mut self, generation: u64, state_binding: Option<String>) {
668 self.final_workspace_generation = Some(generation);
669 self.final_state_binding = state_binding;
670 }
671
672 pub fn block(&mut self, reason: impl Into<String>) {
674 self.termination = Some(ProofTermination::Blocked {
675 reason: reason.into(),
676 });
677 }
678
679 pub fn cancel(&mut self, reason: impl Into<String>) {
681 self.termination = Some(ProofTermination::Cancelled {
682 reason: reason.into(),
683 });
684 }
685
686 pub fn record(&mut self, evidence: Evidence) -> Uuid {
688 let id = evidence.id;
689 self.evidence.insert(id, evidence);
690 id
691 }
692
693 pub fn link(
695 &mut self,
696 contract: &TaskContract,
697 evidence_id: Uuid,
698 criterion_id: impl Into<String>,
699 rationale: Option<String>,
700 ) -> Result<(), ProofError> {
701 if !self.evidence.contains_key(&evidence_id) {
702 return Err(ProofError::UnknownEvidence(evidence_id));
703 }
704 let criterion_id = criterion_id.into();
705 if !contract
706 .criteria
707 .iter()
708 .any(|criterion| criterion.id == criterion_id)
709 {
710 return Err(ProofError::UnknownCriterion(criterion_id));
711 }
712 if !self
713 .links
714 .iter()
715 .any(|link| link.evidence_id == evidence_id && link.criterion_id == criterion_id)
716 {
717 self.links.push(EvidenceLink {
718 evidence_id,
719 criterion_id,
720 rationale,
721 });
722 }
723 Ok(())
724 }
725
726 pub fn evaluate_detailed(
728 &self,
729 contract: &mut TaskContract,
730 ) -> Result<ProofEvaluation, ProofError> {
731 if self.contract_id != contract.id {
732 return Err(ProofError::ContractMismatch);
733 }
734 contract.validate()?;
735
736 let mut evaluations = Vec::with_capacity(contract.criteria.len());
737 for criterion in &mut contract.criteria {
738 if criterion.state == CriterionState::Waived {
739 let mut evaluation = self.evaluate_criterion(criterion);
740 evaluation.state = CriterionState::Waived;
741 criterion.evidence_ids.clone_from(&evaluation.evidence_ids);
742 evaluations.push(evaluation);
743 continue;
744 }
745
746 let evaluation = self.evaluate_criterion(criterion);
747 criterion.state = evaluation.state;
748 criterion.evidence_ids.clone_from(&evaluation.evidence_ids);
749 evaluations.push(evaluation);
750 }
751
752 let mut outcome = if let Some(termination) = &self.termination {
753 match termination {
754 ProofTermination::Blocked { .. } => RunOutcome::Blocked,
755 ProofTermination::Cancelled { .. } => RunOutcome::Cancelled,
756 }
757 } else {
758 outcome_for(contract.claim_scope, &contract.criteria)
759 };
760
761 if contract.claim_scope == ClaimScope::Task
762 && outcome == RunOutcome::Verified
763 && !has_machine_checkable_task_evidence(contract, &evaluations, &self.evidence)
764 {
765 outcome = RunOutcome::Blocked;
766 }
767
768 let assurance_level = contract
769 .criteria
770 .iter()
771 .filter(|criterion| criterion.required && criterion.state == CriterionState::Passed)
772 .filter_map(|criterion| {
773 evaluations
774 .iter()
775 .find(|evaluation| evaluation.criterion_id == criterion.id)
776 })
777 .flat_map(|evaluation| evaluation.qualifying_evidence_ids.iter())
778 .filter_map(|id| self.evidence.get(id))
779 .map(|evidence| evidence.assurance_level)
780 .min()
781 .unwrap_or(AssuranceLevel::Recorded);
782
783 Ok(ProofEvaluation {
784 claim_scope: contract.claim_scope,
785 assurance_level,
786 outcome,
787 criteria: evaluations,
788 })
789 }
790
791 pub fn evaluate(&self, contract: &mut TaskContract) -> Result<RunOutcome, ProofError> {
793 self.evaluate_detailed(contract)
794 .map(|evaluation| evaluation.outcome)
795 }
796
797 fn evaluate_criterion(&self, criterion: &Criterion) -> CriterionEvaluation {
798 let evidence_ids: Vec<_> = self
799 .links
800 .iter()
801 .filter(|link| link.criterion_id == criterion.id)
802 .map(|link| link.evidence_id)
803 .collect::<BTreeSet<_>>()
804 .into_iter()
805 .collect();
806 let linked_ids: BTreeSet<_> = evidence_ids.iter().copied().collect();
807 let superseded: BTreeSet<_> = evidence_ids
808 .iter()
809 .filter_map(|successor_id| self.evidence.get(successor_id))
810 .flat_map(|successor| {
811 successor
812 .supersedes
813 .iter()
814 .filter(|predecessor_id| {
815 linked_ids.contains(predecessor_id)
816 && valid_supersession(
817 successor,
818 self.evidence
819 .get(predecessor_id)
820 .expect("linked evidence exists"),
821 )
822 })
823 .copied()
824 })
825 .collect();
826 let active_evidence_ids: Vec<_> = evidence_ids
827 .iter()
828 .filter(|id| !superseded.contains(id))
829 .copied()
830 .collect();
831 let unresolved_counterevidence_ids: Vec<_> = active_evidence_ids
832 .iter()
833 .filter(|id| {
834 self.evidence
835 .get(id)
836 .is_some_and(|evidence| !evidence.success)
837 })
838 .copied()
839 .collect();
840 let qualifying_evidence_ids: Vec<_> = active_evidence_ids
841 .iter()
842 .filter(|id| {
843 self.evidence.get(id).is_some_and(|evidence| {
844 evidence.success
845 && evidence_qualifies(
846 evidence,
847 &criterion.evidence_requirement,
848 self.final_workspace_generation,
849 self.final_state_binding.as_deref(),
850 )
851 })
852 })
853 .copied()
854 .collect();
855
856 let minimum_observations = criterion
857 .minimum_evidence
858 .max(criterion.evidence_requirement.minimum_observations);
859 let distinct_producers = qualifying_evidence_ids
860 .iter()
861 .filter_map(|id| self.evidence.get(id))
862 .map(|evidence| evidence.producer.as_str())
863 .collect::<BTreeSet<_>>()
864 .len();
865 let mut unmet_requirements = Vec::new();
866 if qualifying_evidence_ids.len()
867 < usize::try_from(minimum_observations).unwrap_or(usize::MAX)
868 {
869 unmet_requirements.push(format!(
870 "requires {minimum_observations} qualifying observations, found {}",
871 qualifying_evidence_ids.len()
872 ));
873 }
874 if distinct_producers
875 < usize::try_from(criterion.evidence_requirement.minimum_independent_producers)
876 .unwrap_or(usize::MAX)
877 {
878 unmet_requirements.push(format!(
879 "requires {} independent producers, found {distinct_producers}",
880 criterion.evidence_requirement.minimum_independent_producers
881 ));
882 }
883 if !unresolved_counterevidence_ids.is_empty() {
884 unmet_requirements.push(format!(
885 "{} unresolved counterevidence observations remain",
886 unresolved_counterevidence_ids.len()
887 ));
888 }
889
890 let state = if !unresolved_counterevidence_ids.is_empty() {
891 CriterionState::Failed
892 } else if unmet_requirements.is_empty() {
893 CriterionState::Passed
894 } else {
895 CriterionState::Pending
896 };
897
898 CriterionEvaluation {
899 criterion_id: criterion.id.clone(),
900 state,
901 evidence_ids,
902 active_evidence_ids,
903 qualifying_evidence_ids,
904 unresolved_counterevidence_ids,
905 unmet_requirements,
906 }
907 }
908}
909
910fn outcome_for(claim_scope: ClaimScope, criteria: &[Criterion]) -> RunOutcome {
911 let required: Vec<_> = criteria
912 .iter()
913 .filter(|criterion| criterion.required)
914 .collect();
915 if required
916 .iter()
917 .any(|criterion| criterion.state == CriterionState::Failed)
918 {
919 return RunOutcome::Failed;
920 }
921 if required
922 .iter()
923 .any(|criterion| criterion.state == CriterionState::Pending)
924 {
925 return RunOutcome::Blocked;
926 }
927 if claim_scope == ClaimScope::Runtime {
931 return RunOutcome::Blocked;
932 }
933 if required
934 .iter()
935 .any(|criterion| criterion.state == CriterionState::Waived)
936 {
937 return RunOutcome::VerifiedWithWaivers;
938 }
939 RunOutcome::Verified
940}
941
942fn has_machine_checkable_task_evidence(
943 contract: &TaskContract,
944 evaluations: &[CriterionEvaluation],
945 evidence: &BTreeMap<Uuid, Evidence>,
946) -> bool {
947 contract
948 .criteria
949 .iter()
950 .filter(|criterion| criterion.required && criterion.state == CriterionState::Passed)
951 .filter_map(|criterion| {
952 evaluations
953 .iter()
954 .find(|evaluation| evaluation.criterion_id == criterion.id)
955 })
956 .flat_map(|evaluation| evaluation.qualifying_evidence_ids.iter())
957 .filter_map(|id| evidence.get(id))
958 .any(|evidence| {
959 matches!(
960 evidence.kind,
961 EvidenceKind::Tool | EvidenceKind::Process | EvidenceKind::Git
962 )
963 })
964}
965
966fn valid_supersession(successor: &Evidence, predecessor: &Evidence) -> bool {
967 if successor.id == predecessor.id {
968 return false;
969 }
970 matches!(
971 (
972 successor.attempt_id,
973 successor.attempt_sequence,
974 predecessor.attempt_id,
975 predecessor.attempt_sequence,
976 ),
977 (
978 Some(successor_id),
979 Some(successor_sequence),
980 Some(predecessor_id),
981 Some(predecessor_sequence),
982 ) if successor_id != predecessor_id && successor_sequence > predecessor_sequence
983 )
984}
985
986fn evidence_qualifies(
987 evidence: &Evidence,
988 requirement: &EvidenceRequirement,
989 final_workspace_generation: Option<u64>,
990 final_state_binding: Option<&str>,
991) -> bool {
992 if !requirement.allowed_kinds.is_empty() && !requirement.allowed_kinds.contains(&evidence.kind)
993 {
994 return false;
995 }
996 if !requirement.allowed_producers.is_empty()
997 && !requirement.allowed_producers.contains(&evidence.producer)
998 {
999 return false;
1000 }
1001 if requirement.require_artifacts && evidence.artifacts.is_empty() {
1002 return false;
1003 }
1004 if evidence.assurance_level < requirement.minimum_assurance {
1005 return false;
1006 }
1007 match requirement.freshness {
1008 EvidenceFreshness::Any => true,
1009 EvidenceFreshness::FinalWorkspaceGeneration => {
1010 final_workspace_generation.is_some()
1011 && evidence.workspace_generation == final_workspace_generation
1012 }
1013 EvidenceFreshness::FinalWorkspaceState => {
1014 final_workspace_generation.is_some()
1015 && final_state_binding.is_some()
1016 && evidence.workspace_generation == final_workspace_generation
1017 && evidence.state_binding.as_deref() == final_state_binding
1018 }
1019 }
1020}
1021
1022#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
1024#[serde(tag = "state", rename_all = "snake_case")]
1025pub enum ProofTermination {
1026 Blocked {
1028 reason: String,
1030 },
1031 Cancelled {
1033 reason: String,
1035 },
1036}
1037
1038#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq)]
1040#[serde(rename_all = "snake_case")]
1041pub enum RunOutcome {
1042 Verified,
1044 VerifiedWithWaivers,
1046 Failed,
1048 Blocked,
1050 Cancelled,
1052}
1053
1054#[derive(Debug, Error)]
1056pub enum ProofError {
1057 #[error("invalid task contract: {0}")]
1059 InvalidContract(String),
1060 #[error("duplicate criterion id: {0}")]
1062 DuplicateCriterion(String),
1063 #[error("unknown criterion: {0}")]
1065 UnknownCriterion(String),
1066 #[error("unknown evidence: {0}")]
1068 UnknownEvidence(Uuid),
1069 #[error("proof graph belongs to a different task contract")]
1071 ContractMismatch,
1072 #[error("waiver reason must not be empty")]
1074 EmptyWaiverReason,
1075}
1076
1077#[cfg(test)]
1078mod tests {
1079 use proptest::prelude::*;
1080 use serde_json::json;
1081
1082 use super::*;
1083
1084 fn evidence(kind: EvidenceKind, producer: &str, success: bool) -> Evidence {
1085 Evidence::observed(kind, producer, "observation", None, None, Some(0), success)
1086 .bound_to_workspace(1, None)
1087 }
1088
1089 fn task_criterion(id: &str, description: &str, producers: &[&str]) -> Criterion {
1090 let mut criterion = Criterion::required(id, description);
1091 criterion.evidence_requirement.allowed_producers = producers
1092 .iter()
1093 .map(|producer| (*producer).to_owned())
1094 .collect();
1095 criterion.evidence_requirement.freshness = EvidenceFreshness::FinalWorkspaceGeneration;
1096 criterion
1097 }
1098
1099 fn link_one(contract: &TaskContract, graph: &mut ProofGraph, evidence: Evidence) -> Uuid {
1100 if contract.claim_scope == ClaimScope::Task && graph.final_workspace_generation.is_none() {
1101 graph.bind_final_workspace(1, None);
1102 }
1103 let id = graph.record(evidence);
1104 graph.link(contract, id, "criterion", None).unwrap();
1105 id
1106 }
1107
1108 #[test]
1109 fn automatic_contract_is_runtime_scoped_only() {
1110 let mut contract = TaskContract::automatic("model returned text");
1111 let mut graph = ProofGraph::new(contract.id);
1112 let id = graph.record(evidence(EvidenceKind::Runtime, "proofborne.runtime", true));
1113 graph
1114 .link(&contract, id, "runtime_completed", None)
1115 .unwrap();
1116
1117 let evaluation = graph.evaluate_detailed(&mut contract).unwrap();
1118 assert_eq!(evaluation.outcome, RunOutcome::Blocked);
1119 assert_eq!(evaluation.claim_scope, ClaimScope::Runtime);
1120 assert_ne!(evaluation.claim_scope, ClaimScope::Task);
1121 }
1122
1123 #[test]
1124 fn runtime_only_criteria_cannot_be_relabelled_as_task_proof() {
1125 let mut contract = TaskContract::automatic("model returned text");
1126 contract.claim_scope = ClaimScope::Task;
1127 assert!(matches!(
1128 contract.validate(),
1129 Err(ProofError::InvalidContract(message))
1130 if message.contains("runtime-only criteria cannot prove a task")
1131 ));
1132 }
1133
1134 #[test]
1135 fn human_only_criterion_is_not_machine_checkable_task_proof() {
1136 let mut criterion = Criterion::required("human", "a person says it is done");
1137 criterion.evidence_requirement.allowed_kinds = [EvidenceKind::Human].into_iter().collect();
1138 criterion.evidence_requirement.allowed_producers =
1139 ["human.user".to_owned()].into_iter().collect();
1140 criterion.evidence_requirement.freshness = EvidenceFreshness::FinalWorkspaceGeneration;
1141 let contract = TaskContract::new("task", vec![criterion]);
1142 assert!(matches!(
1143 contract.validate(),
1144 Err(ProofError::InvalidContract(message)) if message.contains("task-capable evidence")
1145 ));
1146 }
1147
1148 #[test]
1149 fn mixed_requirement_cannot_use_runtime_observation_as_task_evidence() {
1150 let mut criterion = Criterion::required("criterion", "task result");
1151 criterion.evidence_requirement.allowed_kinds =
1152 [EvidenceKind::Runtime, EvidenceKind::Process]
1153 .into_iter()
1154 .collect();
1155 criterion.evidence_requirement.allowed_producers =
1156 ["proofborne.runtime".to_owned()].into_iter().collect();
1157 criterion.evidence_requirement.freshness = EvidenceFreshness::FinalWorkspaceGeneration;
1158 let mut contract = TaskContract::new("task", vec![criterion]);
1159 let mut graph = ProofGraph::new(contract.id);
1160 link_one(
1161 &contract,
1162 &mut graph,
1163 evidence(EvidenceKind::Runtime, "proofborne.runtime", true),
1164 );
1165 assert!(contract.validate().is_ok());
1166 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Blocked);
1167 assert_eq!(contract.criteria[0].state, CriterionState::Passed);
1168 }
1169
1170 #[test]
1171 fn task_contract_rejects_wildcard_producer() {
1172 let mut criterion = Criterion::required("criterion", "task result");
1173 criterion.evidence_requirement.freshness = EvidenceFreshness::FinalWorkspaceGeneration;
1174 let contract = TaskContract::new("task", vec![criterion]);
1175 assert!(matches!(
1176 contract.validate(),
1177 Err(ProofError::InvalidContract(message)) if message.contains("allowed producer")
1178 ));
1179 }
1180
1181 #[test]
1182 fn task_contract_rejects_evidence_not_bound_to_final_workspace() {
1183 let mut criterion = Criterion::required("criterion", "task result");
1184 criterion.evidence_requirement.allowed_producers =
1185 ["proofborne.verify".to_owned()].into_iter().collect();
1186 let contract = TaskContract::new("task", vec![criterion]);
1187 assert!(matches!(
1188 contract.validate(),
1189 Err(ProofError::InvalidContract(message)) if message.contains("final workspace")
1190 ));
1191 }
1192
1193 #[test]
1194 fn failed_evidence_prevents_verified_outcome() {
1195 let mut contract = TaskContract::automatic("test");
1196 let mut graph = ProofGraph::new(contract.id);
1197 let evidence = evidence(EvidenceKind::Runtime, "proofborne.runtime", false);
1198 let id = graph.record(evidence);
1199 graph
1200 .link(&contract, id, "runtime_completed", None)
1201 .unwrap();
1202 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Failed);
1203 assert_eq!(contract.criteria[0].state, CriterionState::Failed);
1204 }
1205
1206 #[test]
1207 fn explicit_later_attempt_supersedes_failure_but_preserves_history() {
1208 let mut contract = TaskContract::new(
1209 "fix it",
1210 vec![task_criterion("criterion", "tests pass", &["test"])],
1211 );
1212 let mut graph = ProofGraph::new(contract.id);
1213 let first_attempt = Uuid::now_v7();
1214 let failed = evidence(EvidenceKind::Process, "test", false).with_attempt(first_attempt, 1);
1215 let failed_id = link_one(&contract, &mut graph, failed);
1216 let passed = evidence(EvidenceKind::Process, "test", true)
1217 .with_attempt(Uuid::now_v7(), 2)
1218 .superseding([failed_id]);
1219 let passed_id = link_one(&contract, &mut graph, passed);
1220
1221 let evaluation = graph.evaluate_detailed(&mut contract).unwrap();
1222 assert_eq!(evaluation.outcome, RunOutcome::Verified);
1223 assert_eq!(graph.evidence.len(), 2);
1224 assert_eq!(
1225 evaluation.criteria[0].evidence_ids,
1226 vec![failed_id, passed_id]
1227 );
1228 assert_eq!(evaluation.criteria[0].active_evidence_ids, vec![passed_id]);
1229 assert!(
1230 evaluation.criteria[0]
1231 .unresolved_counterevidence_ids
1232 .is_empty()
1233 );
1234 }
1235
1236 #[test]
1237 fn failure_without_valid_later_attempt_remains_counterevidence() {
1238 let mut contract = TaskContract::new(
1239 "fix it",
1240 vec![task_criterion("criterion", "tests pass", &["test"])],
1241 );
1242 let mut graph = ProofGraph::new(contract.id);
1243 let failed = evidence(EvidenceKind::Process, "test", false).with_attempt(Uuid::now_v7(), 2);
1244 let failed_id = link_one(&contract, &mut graph, failed);
1245 let earlier_success = evidence(EvidenceKind::Process, "test", true)
1246 .with_attempt(Uuid::now_v7(), 1)
1247 .superseding([failed_id]);
1248 link_one(&contract, &mut graph, earlier_success);
1249
1250 let evaluation = graph.evaluate_detailed(&mut contract).unwrap();
1251 assert_eq!(evaluation.outcome, RunOutcome::Failed);
1252 assert_eq!(
1253 evaluation.criteria[0].unresolved_counterevidence_ids,
1254 vec![failed_id]
1255 );
1256 }
1257
1258 #[test]
1259 fn typed_requirement_filters_kind_producer_artifact_and_assurance() {
1260 let mut criterion = task_criterion("criterion", "verified output", &["trusted.test"]);
1261 criterion.evidence_requirement.allowed_kinds =
1262 [EvidenceKind::Process].into_iter().collect();
1263 criterion.evidence_requirement.allowed_producers =
1264 ["trusted.test".to_owned()].into_iter().collect();
1265 criterion.evidence_requirement.require_artifacts = true;
1266 criterion.evidence_requirement.minimum_assurance = AssuranceLevel::Isolated;
1267 let mut contract = TaskContract::new("verify", vec![criterion]);
1268 let mut graph = ProofGraph::new(contract.id);
1269 link_one(
1270 &contract,
1271 &mut graph,
1272 evidence(EvidenceKind::Process, "trusted.test", true),
1273 );
1274 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Blocked);
1275
1276 let mut qualifying = evidence(EvidenceKind::Process, "trusted.test", true)
1277 .with_assurance(AssuranceLevel::Isolated);
1278 qualifying.artifacts.push(ArtifactRef {
1279 hash: "abc".to_owned(),
1280 name: "report.xml".to_owned(),
1281 media_type: Some("application/xml".to_owned()),
1282 size: 3,
1283 });
1284 link_one(&contract, &mut graph, qualifying);
1285 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Verified);
1286 }
1287
1288 #[test]
1289 fn freshness_requires_final_generation_and_state_binding() {
1290 let mut criterion = task_criterion("criterion", "fresh tests", &["test"]);
1291 criterion.evidence_requirement.freshness = EvidenceFreshness::FinalWorkspaceState;
1292 let mut contract = TaskContract::new("verify", vec![criterion]);
1293 let mut graph = ProofGraph::new(contract.id);
1294 graph.bind_final_workspace(2, Some("final-hash".to_owned()));
1295 link_one(
1296 &contract,
1297 &mut graph,
1298 evidence(EvidenceKind::Process, "test", true)
1299 .bound_to_workspace(1, Some("old-hash".to_owned())),
1300 );
1301 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Blocked);
1302
1303 link_one(
1304 &contract,
1305 &mut graph,
1306 evidence(EvidenceKind::Process, "test", true)
1307 .bound_to_workspace(2, Some("final-hash".to_owned())),
1308 );
1309 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Verified);
1310 }
1311
1312 #[test]
1313 fn independent_producers_are_counted_by_identity() {
1314 let mut criterion =
1315 task_criterion("criterion", "independent checks", &["test-a", "test-b"]);
1316 criterion.evidence_requirement.minimum_observations = 2;
1317 criterion.evidence_requirement.minimum_independent_producers = 2;
1318 let mut contract = TaskContract::new("verify", vec![criterion]);
1319 let mut graph = ProofGraph::new(contract.id);
1320 link_one(
1321 &contract,
1322 &mut graph,
1323 evidence(EvidenceKind::Process, "test-a", true),
1324 );
1325 link_one(
1326 &contract,
1327 &mut graph,
1328 evidence(EvidenceKind::Process, "test-a", true),
1329 );
1330 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Blocked);
1331
1332 link_one(
1333 &contract,
1334 &mut graph,
1335 evidence(EvidenceKind::Process, "test-b", true),
1336 );
1337 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Verified);
1338 }
1339
1340 #[test]
1341 fn waiver_is_visible_in_outcome() {
1342 let mut contract = TaskContract::new(
1343 "test",
1344 vec![task_criterion("criterion", "task result", &["test"])],
1345 );
1346 contract
1347 .waive("criterion", "user", "accepted manually")
1348 .unwrap();
1349 let graph = ProofGraph::new(contract.id);
1350 assert_eq!(
1351 graph.evaluate(&mut contract).unwrap(),
1352 RunOutcome::VerifiedWithWaivers
1353 );
1354 }
1355
1356 #[test]
1357 fn runtime_waiver_still_cannot_produce_exit_zero_outcome() {
1358 let mut contract = TaskContract::automatic("test");
1359 contract
1360 .waive("runtime_completed", "user", "accepted manually")
1361 .unwrap();
1362 let graph = ProofGraph::new(contract.id);
1363 assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Blocked);
1364 }
1365
1366 #[test]
1367 fn old_json_defaults_to_runtime_scope_and_conservative_assurance() {
1368 let id = Uuid::now_v7();
1369 let contract: TaskContract = serde_json::from_value(json!({
1370 "schemaVersion": SCHEMA_VERSION,
1371 "id": id,
1372 "goal": "old contract",
1373 "criteria": [{
1374 "id": "criterion",
1375 "description": "old criterion",
1376 "required": true,
1377 "minimumEvidence": 2,
1378 "state": "pending",
1379 "evidenceIds": []
1380 }],
1381 "createdAt": "2026-07-29T00:00:00Z",
1382 "confirmed": true
1383 }))
1384 .unwrap();
1385 assert_eq!(contract.claim_scope, ClaimScope::Runtime);
1386 assert_eq!(
1387 contract.criteria[0]
1388 .evidence_requirement
1389 .minimum_observations,
1390 1
1391 );
1392 assert_eq!(contract.criteria[0].minimum_evidence, 2);
1393 }
1394
1395 #[test]
1396 fn old_evidence_json_gets_backward_safe_metadata_defaults() {
1397 let evidence = evidence(EvidenceKind::Process, "legacy", true);
1398 let mut value = serde_json::to_value(evidence).unwrap();
1399 let object = value.as_object_mut().unwrap();
1400 object.remove("assuranceLevel");
1401 object.remove("attemptId");
1402 object.remove("attemptSequence");
1403 object.remove("actionId");
1404 object.remove("workspaceGeneration");
1405 object.remove("stateBinding");
1406 object.remove("supersedes");
1407
1408 let restored: Evidence = serde_json::from_value(value).unwrap();
1409 assert_eq!(restored.assurance_level, AssuranceLevel::Recorded);
1410 assert_eq!(restored.attempt_id, None);
1411 assert_eq!(restored.workspace_generation, None);
1412 assert!(restored.supersedes.is_empty());
1413 }
1414
1415 #[test]
1416 fn public_json_uses_camel_case_fields() {
1417 let contract = TaskContract::automatic("json");
1418 let value = serde_json::to_value(contract).unwrap();
1419 assert_eq!(value["claimScope"], "runtime");
1420 assert!(value["criteria"][0].get("evidenceRequirement").is_some());
1421 assert!(
1422 value["criteria"][0]["evidenceRequirement"]
1423 .get("minimumObservations")
1424 .is_some()
1425 );
1426 }
1427
1428 proptest! {
1429 #[test]
1430 fn unresolved_failure_always_beats_any_number_of_successes(successes in 0_usize..32) {
1431 let mut contract = TaskContract::new(
1432 "property",
1433 vec![task_criterion("criterion", "must hold", &["test"])],
1434 );
1435 let mut graph = ProofGraph::new(contract.id);
1436 link_one(
1437 &contract,
1438 &mut graph,
1439 evidence(EvidenceKind::Process, "test", false),
1440 );
1441 for _ in 0..successes {
1442 link_one(
1443 &contract,
1444 &mut graph,
1445 evidence(EvidenceKind::Process, "test", true),
1446 );
1447 }
1448 prop_assert_eq!(graph.evaluate(&mut contract).unwrap(), RunOutcome::Failed);
1449 }
1450
1451 #[test]
1452 fn minimum_observation_count_is_enforced(required in 1_u32..16, present in 0_u32..16) {
1453 let mut criterion = task_criterion("criterion", "counted", &["test"]);
1454 criterion.minimum_evidence = required;
1455 criterion.evidence_requirement.minimum_observations = required;
1456 let mut contract = TaskContract::new("property", vec![criterion]);
1457 let mut graph = ProofGraph::new(contract.id);
1458 for _ in 0..present {
1459 link_one(
1460 &contract,
1461 &mut graph,
1462 evidence(EvidenceKind::Process, "test", true),
1463 );
1464 }
1465 let outcome = graph.evaluate(&mut contract).unwrap();
1466 prop_assert_eq!(outcome == RunOutcome::Verified, present >= required);
1467 }
1468 }
1469}