krabka_verified/
audit.rs

1//! Pure admission and sync-cadence arithmetic for the audit spool.
2
3use creusot_std::prelude::*;
4
5/// State transition for one attempted audit-spool append.
6#[krabka_macros::model_type]
7pub struct SpoolAppendDecision {
8    pub accepted: bool,
9    pub new_bytes: u64,
10    pub sync: bool,
11    pub next_unsynced: u64,
12}
13
14/// Admission result for a signed audit checkpoint at the current chain head.
15#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
16pub enum AuditCheckpointAdmission {
17    Admit,
18    RejectSignature,
19    RejectHead,
20    RejectSequence,
21}
22
23/// Admission result for a records-lost marker.
24#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
25pub enum AuditLossMarkerAdmission {
26    /// The marker is accepted and `generation` becomes the last accepted one.
27    Admit {
28        generation: u64,
29    },
30    Reject,
31}
32
33/// Fail-open audit losses: the pending count `PendingLosses` holds, or the
34/// batch a durable records-lost marker reports. `generation` is the
35/// `loss_generation` a marker for these losses names.
36#[krabka_macros::model_type(runtime(Clone, Copy, Debug, Default, PartialEq, Eq, Hash))]
37pub struct AuditLosses {
38    pub generation: u64,
39    pub count: u64,
40}
41
42mod spool_append_decision;
43pub use spool_append_decision::{
44    audit_checkpoint_admission, audit_loss_marker_admission, settle_loss_batch,
45    spool_append_decision,
46};
47
48#[cfg(test)]
49mod tests;
krabka_verified/audit.rs

krabka_verified/
audit.rs
