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

use crate::expressions::Expression;
use crate::identifier::Identifier;
use crate::package::{OracleDef, OracleSig, Package, PackageInstance};
use crate::statement::{CodeBlock, Statement};
use crate::types::Type;
use std::collections::HashMap;

use crate::block;

pub fn key_pkg(params: &HashMap<String, String>) -> PackageInstance {
    PackageInstance {
        name: "key".to_string(),
        params: params.clone(),
        pkg: Package {
            params: vec![("n".to_string(), Type::new_scalar("int"))],
            state: vec![("k".to_string(), Type::Maybe(Box::new(Type::new_bits("n"))))],
            oracles: vec![
                OracleDef {
                    sig: OracleSig {
                        name: "Set".to_string(),
                        args: vec![("k_".to_string(), Type::new_bits("n"))],
                        tipe: Type::Empty,
                    },
                    code: block! {
                        Statement::IfThenElse(
                            Expression::new_equals(vec![
                                &(Identifier::new_scalar("k").to_expression()),
                                &Expression::None(Type::new_bits("n")),
                            ]),
                            block! {
                                Statement::Assign(Identifier::new_scalar("k_sample"),
                                                  Expression::Sample(Type::new_bits("n")),
                                ),
                                Statement::Assign(Identifier::new_scalar("k"),
                                                  Expression::Some(Box::new(Identifier::new_scalar("k_sample").to_expression())),
                                )
                            },
                            block! {
                                Statement::Abort
                            },
                        )
                    },
                },
                OracleDef {
                    sig: OracleSig {
                        name: "Get".to_string(),
                        args: vec![],
                        tipe: Type::new_bits("n"),
                    },
                    code: block! {
                        Statement::IfThenElse(
                            Expression::new_equals(vec![
                                &(Identifier::new_scalar("k").to_expression()),
                                &Expression::None(Type::new_bits("n")),
                            ]),
                            block! {Statement::Abort},
                            block! {},
                        ),
                        Statement::Return(Some(Expression::Unwrap(Box::new(Identifier::new_scalar("k").to_expression()))))
                    },
                },
            ],
        },
    }
}