CCGRID26_code/dfunction.ath at main · FLAGlab/CCGRID26_code · GitHub

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
111
112
113
114
115
116
117
118
119
120
load "dpair.ath"
load "function.ath"
define lAlive := Location.alive


module DFunction {
    open Function
    assert (theory-axioms Function.theory)
    ############################## Declarations
    declare alive: (D,R) [(DPr (fn D R) (fn D R))] -> Boolean

    declare apply: (D,R) [(DPr (fn D R) (fn D R)) D] -> (Option R)

    declare functionReplica: (D,R) [(fn D R) Location Location]
                                   -> (DPr (fn D R) (fn D R))

    declare replicaComposition: (A, B, C) [(DPr (fn A B) (fn A B)) (DPr (fn B C) (fn B C))]
                                          -> (DPr (fn A C) (fn A C))

    ############################## Definitions

    define [f g x l1 l0 lg lg0 lg1 lf0 lf1] :=
           [?f:(fn 'D 'R) ?g:(fn 'R 'O) ?x:'D ?l1:Location ?l0:Location
            ?lg:Location ?lg0:Location ?lg1:Location ?lf0:Location ?lf1:Location]

    define rComp :=
            (replicaComposition (functionReplica f lf0 lf1) (functionReplica g lg0 lg1))
            # g(f(x))

    ############################## Asserts

    assert* alive_axiom := (iff (alive (dpr l1 f l0 f)) ((lAlive l1) or (lAlive l0)))

    assert* function_replica_axiom := ((functionReplica f l1 l0) = (dpr l1 f l0 f))

    assert apply_axioms :=
    (fun [
        (apply (functionReplica f l1 l0) x) =
            [
                (SOME (f at x)) when (alive (functionReplica f l1 l0))
                NONE            when (~(alive (functionReplica f l1 l0)))
            ]

    ])

    assert apply_composition_axiom :=
    (fun [
        (apply rComp x) =
            [
                (apply (functionReplica g lg0 lg1 ) (f at x))  when (alive (functionReplica f lf0 lf1))
                NONE                         when (~(alive (functionReplica f l1 l0)))
            ]
    ])


    ############################## Theorem Definitions

    define fault_tolerance_correctness :=
    (forall x f l1 l0 .
        (if
            ((lAlive l1) or (lAlive l0))
            ((apply (functionReplica f l1 l0) x) = (SOME (f at x)))
        )
    )

    define fault_tolerance_correctness_composition :=
    (forall x f g lg0 lg1 lf0 lf1 .
        (if
            (((lAlive lf0) or (lAlive lf1)) and ((lAlive lg0) or (lAlive lg1)))
            ((apply rComp x) = (SOME (g o f) at x))
            # g(f(x))
        )
    )

    ############################## Theorem Proofs

    conclude fault_tolerance_correctness
        pick-any x:'D f:(fn 'D 'R) l1:Location l0:Location
            assume((lAlive l1) or (lAlive l0))
                let {
                    _ :=
                        (!chain<- [
                            (alive (functionReplica f l1 l0))
                            <== (alive (dpr l1 f l0 f))           [function_replica_axiom]
                            <== ((lAlive l1) or (lAlive l0))                 [alive_axiom]
                        ])
                }
                (!chain [
                    (apply (functionReplica f l1 l0) x)
                    = (SOME (f at x))                                       [apply_axioms]
                ])

    conclude fault_tolerance_correctness_composition
        pick-any x:'D f:(fn 'D 'R) g:(fn 'R 'O) lg0:Location lg1:Location lf0:Location lf1:Location
            assume hyp := (((lAlive lf0) or (lAlive lf1)) and ((lAlive lg0) or (lAlive lg1)))
                let {
                    alive_functionReplica_f :=
                        (!chain<- [
                            (alive (functionReplica f lf0 lf1))
                            <== (alive (dpr lf0 f lf1 f))         [function_replica_axiom]
                            <== ((lAlive lf0) or (lAlive lf1))               [alive_axiom]
                        ]);
                    alive_functionReplica_g :=
                        (!chain<- [
                            (alive (functionReplica g lg0 lg1))
                            <== (alive (dpr lg0 g lg1 g))         [function_replica_axiom]
                            <== ((lAlive lg0) or (lAlive lg1))               [alive_axiom]
                        ])
                }
                (!chain [
                    (apply (replicaComposition (functionReplica f lf0 lf1) (functionReplica g lg0 lg1)) x)
                    =
                    (apply (functionReplica g lg0 lg1) (f at x))           [apply_composition_axiom]
                    =
                    (SOME (g at (f at x)))                                            [apply_axioms]
                    =
                    (SOME ((g o f) at x))                                       [compose-definition]
                ])

}