forjar 1.4.2

Rust-native Infrastructure as Code — bare-metal first, BLAKE3 state, provenance tracing
Documentation 
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

//! FJ-1385: Proof obligation taxonomy — classify resource operations formally.
//!
//! Every resource operation is classified as one of:
//! - **Idempotent**: `apply(apply(s)) == apply(s)` — safe to re-run
//! - **Monotonic**: only adds state, never removes — safe to layer
//! - **Convergent**: `apply` always reaches the same fixed point from any starting state
//! - **Destructive**: removes state that cannot be reconstructed

use crate::core::types::{PlanAction, ResourceType};

/// Formal proof obligation category for a resource operation.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ProofObligation {
    /// `f(f(x)) = f(x)` — safe to re-run without side effects.
    Idempotent,
    /// Only adds state; never removes or modifies existing state.
    Monotonic,
    /// Reaches same fixed point from any reachable starting state.
    Convergent,
    /// Removes state that may not be reconstructable.
    Destructive,
}

/// Classify a resource type + action pair into its proof obligation category.
pub fn classify(rtype: &ResourceType, action: &PlanAction) -> ProofObligation {
    match action {
        PlanAction::NoOp => ProofObligation::Idempotent,
        PlanAction::Create => classify_create(rtype),
        PlanAction::Update => classify_update(rtype),
        PlanAction::Destroy => classify_destroy(rtype),
    }
}

/// Create operations: file/service/package are idempotent; model is monotonic.
fn classify_create(rtype: &ResourceType) -> ProofObligation {
    match rtype {
        ResourceType::File => ProofObligation::Idempotent,
        ResourceType::Package => ProofObligation::Idempotent,
        ResourceType::Service => ProofObligation::Convergent,
        ResourceType::Mount => ProofObligation::Idempotent,
        ResourceType::User => ProofObligation::Idempotent,
        ResourceType::Cron => ProofObligation::Idempotent,
        ResourceType::Network => ProofObligation::Convergent,
        ResourceType::Docker | ResourceType::Pepita => ProofObligation::Convergent,
        ResourceType::Gpu => ProofObligation::Convergent,
        ResourceType::Model => ProofObligation::Monotonic,
        ResourceType::Recipe => ProofObligation::Convergent,
        ResourceType::Task => ProofObligation::Convergent,
        ResourceType::WasmBundle | ResourceType::Image => ProofObligation::Idempotent,
        ResourceType::Build => ProofObligation::Convergent,
        ResourceType::GithubRelease => ProofObligation::Idempotent,
    }
}

/// Update operations: generally convergent (reach desired state from any current).
fn classify_update(rtype: &ResourceType) -> ProofObligation {
    match rtype {
        ResourceType::File => ProofObligation::Idempotent,
        ResourceType::Package => ProofObligation::Convergent,
        ResourceType::Service => ProofObligation::Convergent,
        _ => ProofObligation::Convergent,
    }
}

/// Destroy operations: service/package are convergent; file/user/model are destructive.
fn classify_destroy(rtype: &ResourceType) -> ProofObligation {
    match rtype {
        ResourceType::Service => ProofObligation::Convergent,
        ResourceType::Package => ProofObligation::Convergent,
        ResourceType::Cron => ProofObligation::Idempotent,
        ResourceType::Mount => ProofObligation::Convergent,
        ResourceType::File => ProofObligation::Destructive,
        ResourceType::User => ProofObligation::Destructive,
        ResourceType::Model => ProofObligation::Destructive,
        ResourceType::Docker | ResourceType::Pepita => ProofObligation::Convergent,
        ResourceType::Network => ProofObligation::Convergent,
        ResourceType::Gpu => ProofObligation::Convergent,
        ResourceType::Recipe => ProofObligation::Convergent,
        ResourceType::Task => ProofObligation::Destructive,
        ResourceType::WasmBundle | ResourceType::Image => ProofObligation::Destructive,
        ResourceType::Build => ProofObligation::Convergent,
        ResourceType::GithubRelease => ProofObligation::Convergent,
    }
}

/// Human-readable label for a proof obligation.
pub fn label(po: &ProofObligation) -> &'static str {
    match po {
        ProofObligation::Idempotent => "idempotent",
        ProofObligation::Monotonic => "monotonic",
        ProofObligation::Convergent => "convergent",
        ProofObligation::Destructive => "destructive",
    }
}

/// Returns true if the obligation is safe to re-run without confirmation.
pub fn is_safe(po: &ProofObligation) -> bool {
    matches!(
        po,
        ProofObligation::Idempotent | ProofObligation::Monotonic | ProofObligation::Convergent
    )
}