agent_frame/
op.rs

1//! The operation algebra, mirrored from `formal/ContextOps/Basic.lean`.
2//!
3//! Every table here is exhaustive and carries **no wildcard arm**. That is
4//! deliberate: a `_` arm silently absorbs a future variant, and the whole point
5//! of this kernel is that adding an operation forces you to answer what it
6//! asserts, how it is checked, and whether it raises depth.
7//!
8//! Substitution — the untyped fusion of all three — is deliberately **not** a
9//! constructor. This kernel exists to make it unrepresentable.
10
11use serde::{Deserialize, Serialize};
12
13/// What was done to the source material.
14#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
15#[serde(rename_all = "snake_case")]
16pub enum Op {
17    /// Fewer words, same referents. Asserts nothing new; extractively checkable.
18    Concise,
19    /// Removed, marked, addressed. Asserts nothing at all.
20    Elide,
21    /// New sentences not present in the source. The only fabrication surface.
22    Generate,
23}
24
25/// How a unit can be verified by a party that did not run the build — the
26/// supply-chain reproducibility boundary.
27///
28/// Sealing invokes a model, so a packet is an artifact of a NON-reproducible
29/// build and verification cannot rest on re-derivation alone. The fidelity
30/// typing hands us the boundary for free: **only elision is deterministic.**
31#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
32#[serde(rename_all = "snake_case")]
33pub enum Check {
34    /// Deterministic selection: recompute and compare.
35    Rederive,
36    /// Model-generated but extractive: check against the sealed source.
37    Ground,
38    /// Model-generated and non-reproducible: grounding plus an attestation.
39    GroundAttest,
40}
41
42impl Op {
43    /// Whether this operation makes a content claim about the material it
44    /// replaces.
45    ///
46    /// Elision is the only one that does not, which is why it is the safe
47    /// default whenever grounding is uncertain.
48    #[must_use]
49    pub const fn asserts(self) -> bool {
50        match self {
51            Op::Concise => true,
52            Op::Elide => false,
53            Op::Generate => true,
54        }
55    }
56
57    /// The verifiability class of this operation.
58    #[must_use]
59    pub const fn check(self) -> Check {
60        match self {
61            Op::Elide => Check::Rederive,
62            Op::Concise => Check::Ground,
63            Op::Generate => Check::GroundAttest,
64        }
65    }
66
67    /// The depth produced by applying this operation to material already at
68    /// depth `d`.
69    ///
70    /// Concision and elision never raise generation depth; only generation
71    /// does. This is the arithmetic core of the depth bound.
72    #[must_use]
73    pub const fn depth_after(self, d: u32) -> u32 {
74        match self {
75            Op::Generate => d.saturating_add(1),
76            Op::Concise => d,
77            Op::Elide => d,
78        }
79    }
80}
agent_frame/op.rs

agent_frame/
op.rs
