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
103
104
105
106
107
108
109
110
//! An example of a very simple machine-check system.
//!
//! The used structs and implementations must be enclosed
//! within a module on which the machine_description macro
//! is applied.
#[machine_check::machine_description]
mod machine_module {
// Currently, all used non-global paths must be imported
// within the machine_description macro.
//
// Only machine-check types and traits, plus a few std
// traits, can be used.
use ::machine_check::{BitvectorArray, Ext, Unsigned};
use ::std::{
clone::Clone,
cmp::{Eq, PartialEq},
fmt::Debug,
hash::Hash,
};
// It is required to derive the following traits
// on the structs that will be used for machine-check
// verification.
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub struct Input {
increment: Unsigned<1>,
unused: BitvectorArray<16, 8>,
}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub struct Param {}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub struct State {
value: Unsigned<8>,
unused: BitvectorArray<16, 8>,
}
// The system can contain data that will be unchanging,
// but usable within the machine-stepping functions.
//
// This one does not contain any such data.
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub struct System {}
// Machine implementation makes it possible to formally
// verify the system.
impl ::machine_check::Machine for System {
// The type of inputs to the finite-state machine.
type Input = Input;
// The type of parameters of the finite-state machine.
type Param = Param;
// The type of states of the finite-state machine.
type State = State;
// Machine initialization. Given an input, a state is generated.
// The function must be pure, i.e. give the same result with the
// same parameters.
//
// Here, the value is initialized to zero, and the unused array
// is taken from the input, i.e. can have any values.
fn init(&self, input: &Input, _param: &Param) -> State {
State {
value: Unsigned::<8>::new(0),
unused: Clone::clone(&input.unused),
}
}
// Machine step. Given a state and an input, the next state is generated.
// Again, the function must be pure.
//
// Here, the value is incremented if input increment field is 1.
// If it reaches 157, it is immediately reset to 0. The unused array
// is again taken from the input, i.e. can have any values, and the
// values do not have to match the previous ones.
fn next(&self, state: &State, input: &Input, _param: &Param) -> State {
// The increment is extended to 8 bits (zero-extension because
// it is Unsigned), then added to the value in the current state.
// Currently, it must be called using associated function call,
// i.e. Ext::<8>::ext(a), rather than method call input.increment.ext()
let mut next_value = state.value + Ext::<8>::ext(input.increment);
// If the next value is 157, it is immediately set to 0.
if next_value == Unsigned::<8>::new(157) {
next_value = Unsigned::<8>::new(0);
}
// The clone function is one of the few std functions supported
// by machine-check. Currently, the functions can only be called
// using associated function call, i.e. Clone::clone(&a),
// rather than the usually used method call a.clone().
let unused = Clone::clone(&input.unused);
// The new state is constructed with the new value and unused fields.
State {
value: next_value,
unused,
}
}
}
}
// Main entry point of the executable.
fn main() {
// Construct the system. This one has no unchanging data.
let system = machine_module::System {};
// Run machine-check with the constructed system.
machine_check::run(system);
}