pipecircuit-cli 0.0.2

Command-line architectural tools for Pipecircuit programs
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

use crate::domain_primitives::{Amount, Count};
use pipecircuit::{StateMachine, StepInputOf};

pub struct Counter {
    count: Count,
}

impl Counter {
    pub const fn new(count: Count) -> Self {
        Self { count }
    }
}

impl StateMachine for Counter {}

pub struct Add {
    pub amount: Amount,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum AddOutcome {
    Added { before: Count, after: Count },
    Overflow { current: Count, requested: Amount },
}

impl StepInputOf<Counter> for Add {
    type Outcome = AddOutcome;

    fn step(self, counter: &mut Counter) -> Self::Outcome {
        let before = counter.count;
        match before.get().checked_add(self.amount.get()) {
            Some(value) => {
                let after = Count::new(value);
                counter.count = after;
                AddOutcome::Added { before, after }
            }
            None => AddOutcome::Overflow {
                current: before,
                requested: self.amount,
            },
        }
    }
}

pub struct Read;

impl StepInputOf<Counter> for Read {
    type Outcome = Count;

    fn step(self, counter: &mut Counter) -> Self::Outcome {
        counter.count
    }
}

#[cfg(kani)]
mod proofs;
#[cfg(test)]
mod tests;

#[cfg(test)]
mod architecture;