creusot_std/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    fn core(self) -> Option<Self> {
63        match self {
64            None => Some(None),
65            Some(x) => Some(x.core()),
66        }
67    }
68
69    #[logic]
70    #[requires(self.core() != None)]
71    #[ensures({
72        let c = self.core().unwrap_logic();
73        c.op(c) == Some(c)
74    })]
75    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
76    fn core_idemp(self) {
77        self.core_total_idemp()
78    }
79
80    #[logic]
81    #[requires(i.op(i) == Some(i))]
82    #[requires(i.op(self) == Some(self))]
83    #[ensures(match self.core() {
84        Some(c) => i.incl(c),
85        None => false,
86    })]
87    fn core_is_maximal_idemp(self, i: Self) {
88        match (self, i) {
89            (Some(x), Some(i)) => x.core_is_maximal_idemp(i),
90            _ => (),
91        }
92    }
93}
94
95impl<T: RA> UnitRA for Option<T> {
96    #[logic(open)]
97    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
98    fn unit() -> Self {
99        None
100    }
101
102    #[logic(open)]
103    #[ensures(self.core() == Some(result))]
104    fn core_total(self) -> Self {
105        match self {
106            None => None,
107            Some(x) => x.core(),
108        }
109    }
110
111    #[logic]
112    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
113    #[ensures(self.core_total().op(self) == Some(self))]
114    fn core_total_idemp(self) {
115        let _ = T::core_idemp;
116    }
117}
118
119pub struct OptionUpdate<U>(pub U);
120
121impl<R: RA, U: Update<R>> Update<Option<R>> for OptionUpdate<U> {
122    type Choice = U::Choice;
123
124    #[logic(open)]
125    fn premise(self, from: Option<R>) -> bool {
126        match from {
127            Some(from) => self.0.premise(from),
128            None => false,
129        }
130    }
131
132    #[logic(open)]
133    #[requires(self.premise(from))]
134    fn update(self, from: Option<R>, ch: U::Choice) -> Option<R> {
135        match from {
136            Some(from) => Some(self.0.update(from, ch)),
137            None => None, /* Dummy */
138        }
139    }
140
141    #[logic]
142    #[requires(self.premise(from))]
143    #[requires(from.op(frame) != None)]
144    #[ensures(self.update(from, result).op(frame) != None)]
145    fn frame_preserving(self, from: Option<R>, frame: Option<R>) -> U::Choice {
146        match frame {
147            Some(frame) => self.0.frame_preserving(from.unwrap_logic(), frame),
148            None => such_that(|_| true),
149        }
150    }
151}
creusot_std/logic/ra/option.rs

creusot_std/logic/ra/
option.rs
