creusot_contracts/logic/ra/
option.rs

1#[cfg(creusot)]
2use crate::logic::such_that;
3use crate::{
4    logic::ra::{RA, UnitRA, update::Update},
5    prelude::*,
6};
7
8impl<T: RA> RA for Option<T> {
9    #[logic(open)]
10    fn op(self, other: Self) -> Option<Self> {
11        match (self, other) {
12            (None, _) => Some(other),
13            (_, None) => Some(self),
14            (Some(x), Some(y)) => x.op(y).map_logic(|z| Some(z)),
15        }
16    }
17
18    #[logic(open)]
19    #[ensures(match result {
20        Some(c) => factor.op(c) == Some(self),
21        None => forall<c: Self> factor.op(c) != Some(self),
22    })]
23    fn factor(self, factor: Self) -> Option<Self> {
24        match (self, factor) {
25            (x, None) => Some(x),
26            (None, _) => None,
27            (Some(x), Some(y)) => match x.factor(y) {
28                Some(z) => Some(Some(z)),
29                None => {
30                    if x == y {
31                        Some(None)
32                    } else {
33                        None
34                    }
35                }
36            },
37        }
38    }
39
40    #[logic(open(self), law)]
41    #[ensures(a.op(b) == b.op(a))]
42    fn commutative(a: Self, b: Self) {
43        let _ = <T as RA>::commutative;
44    }
45
46    #[logic(open(self), law)]
47    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
48    fn associative(a: Self, b: Self, c: Self) {
49        pearlite! {
50            match (a, b, c) {
51                (None, _, _) => {},
52                (_, None, _) => {},
53                (_, _, None) => {},
54                (Some(aa), Some(bb), Some(cc)) => {
55                    <T as RA>::associative(aa, bb, cc)
56                }
57            }
58        }
59    }
60
61    #[logic(open)]
62    #[ensures(match result {
63        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
64        None => true
65    })]
66    fn core(self) -> Option<Self> {
67        Some(self.core_total())
68    }
69
70    #[logic]
71    #[requires(i.op(i) == Some(i))]
72    #[requires(i.op(self) == Some(self))]
73    #[ensures(match self.core() {
74        Some(c) => i.incl(c),
75        None => false,
76    })]
77    fn core_is_maximal_idemp(self, i: Self) {
78        match (self, i) {
79            (Some(x), Some(i)) => x.core_is_maximal_idemp(i),
80            _ => (),
81        }
82    }
83}
84
85impl<T: RA> UnitRA for Option<T> {
86    #[logic(open)]
87    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
88    fn unit() -> Self {
89        None
90    }
91
92    #[logic(open)]
93    #[ensures(result.op(result) == Some(result))]
94    #[ensures(result.op(self) == Some(self))]
95    fn core_total(self) -> Self {
96        match self {
97            None => None,
98            Some(x) => x.core(),
99        }
100    }
101
102    #[logic]
103    #[ensures(self.core() == Some(self.core_total()))]
104    fn core_is_total(self) {}
105}
106
107pub struct OptionUpdate<U>(pub U);
108
109impl<R: RA, U: Update<R>> Update<Option<R>> for OptionUpdate<U> {
110    type Choice = U::Choice;
111
112    #[logic(open)]
113    fn premise(self, from: Option<R>) -> bool {
114        match from {
115            Some(from) => self.0.premise(from),
116            None => false,
117        }
118    }
119
120    #[logic(open)]
121    #[requires(self.premise(from))]
122    fn update(self, from: Option<R>, ch: U::Choice) -> Option<R> {
123        match from {
124            Some(from) => Some(self.0.update(from, ch)),
125            None => None, /* Dummy */
126        }
127    }
128
129    #[logic]
130    #[requires(self.premise(from))]
131    #[requires(from.op(frame) != None)]
132    #[ensures(self.update(from, result).op(frame) != None)]
133    fn frame_preserving(self, from: Option<R>, frame: Option<R>) -> U::Choice {
134        match frame {
135            Some(frame) => self.0.frame_preserving(from.unwrap_logic(), frame),
136            None => such_that(|_| true),
137        }
138    }
139}
creusot_contracts/logic/ra/option.rs

creusot_contracts/logic/ra/
option.rs
