1use kodept_ast::graph::GenericNodeKey;
2use crate::conc_cache::ConcSecSlotMap;
3use crate::operator_desugaring::{AccessExpander, BinaryOperatorExpander, UnaryOperatorExpander};
4
5mod convert_model;
6mod node_family;
7pub mod operator_desugaring;
8mod scope;
9pub mod semantic_analyzer;
10mod symbol;
11pub mod type_checker;
12mod conc_cache;
13
14#[derive(Copy, Clone)]
15pub struct Witness(());
16
17impl Witness {
18 pub fn fact(_: AccessExpander, _: BinaryOperatorExpander, _: UnaryOperatorExpander) -> Witness {
19 Witness(())
20 }
21
22 pub fn prove<T>(self) -> T {
23 panic!("Cannot prove contract")
24 }
25}
26
27pub(crate) type Path = String;
28
29pub type Cache<T> = ConcSecSlotMap<GenericNodeKey, T>;