1Function Loop.f
2Function Loop.g
3Function f
4Function g
5Pseudo-Compiling.
6Compiling in Loop.f.
7Compiling in Loop.g.
8Compiling in g.
9Compiling in f.
10Checking.
11Proofs for g -> Loop.g
12 .. built problem, finding proof
13ProofNode ('Leaf', None, ())
14 .. proof found.
15Step 1: 
16  prove all verification conditions
17    .. proven.
18Refinement g -> Loop.g proven.
19Proofs for f -> Loop.f
20 .. built problem, finding proof
21ProofNode ('Split', ((30, (0, 1), [Expr ('Var', Type ("Word", 32), name = 'r13'), Expr ('Var', Type ("Word", 32), name = 'ret'), Expr ('Var', Type ("Word", 32), name = 'r9'), Expr ('Var', Type ("Word", 32), name = 'r8'), Expr ('Op', Type ("Word", 32), name = 'Plus', vals = [Expr ('Var', Type ("Word", 32), name = 'r5'), Expr ('Op', Type ("Word", 32), name = 'Times', vals = [Expr ('Op', Type ("Word", 32), name = 'Minus', vals = [Expr ('Num', Type ("Word", 32), val = 0), Expr ('Var', Type ("Word", 32), name = '%i')]), Expr ('Num', Type ("Word", 32), val = 4)])]), Expr ('Op', Type ("Word", 32), name = 'Plus', vals = [Expr ('Var', Type ("Word", 32), name = 'r4'), Expr ('Op', Type ("Word", 32), name = 'Times', vals = [Expr ('Op', Type ("Word", 32), name = 'Minus', vals = [Expr ('Num', Type ("Word", 32), val = 0), Expr ('Var', Type ("Word", 32), name = '%i')]), Expr ('Num', Type ("Word", 32), val = 1)])]), Expr ('Op', Type ('Builtin', 'Bool'), name = 'ROData', vals = [Expr ('Var', Type ('Builtin', 'Mem'), name = 'mem')]), Expr ('Var', Type ("Word", 32), name = 'r11'), Expr ('Var', Type ("Word", 32), name = 'r6'), Expr ('Var', Type ("Word", 32), name = 'r10'), Expr ('Var', Type ("Word", 32), name = 'r7'), Expr ('Op', Type ('Builtin', 'RelWrapper'), name = 'StackWrapper', vals = [Expr ('Op', Type ("Word", 32), name = 'Plus', vals = [Expr ('Var', Type ("Word", 32), name = 'r13'), Expr ('Num', Type ("Word", 32), val = 0)]), Expr ('Var', Type ('Builtin', 'Mem'), name = 'stack')])]), (8, (0, 1), [Expr ('Var', Type ("Word", 32), name = 'p#v'), Expr ('Op', Type ("Word", 32), name = 'Plus', vals = [Expr ('Var', Type ("Word", 32), name = 'loop#2#count'), Expr ('Op', Type ("Word", 32), name = 'Times', vals = [Expr ('Op', Type ("Word", 32), name = 'Minus', vals = [Expr ('Num', Type ("Word", 32), val = 0), Expr ('Var', Type ("Word", 32), name = '%i')]), Expr ('Num', Type ("Word", 32), val = 1)])]), Expr ('Op', Type ("Word", 32), name = 'Plus', vals = [Expr ('Var', Type ("Word", 32), name = 'i#v'), Expr ('Op', Type ("Word", 32), name = 'Times', vals = [Expr ('Op', Type ("Word", 32), name = 'Minus', vals = [Expr ('Num', Type ("Word", 32), val = 0), Expr ('Var', Type ("Word", 32), name = '%i')]), Expr ('Num', Type ("Word", 32), val = 1)])])]), [(Expr ('Var', Type ("Word", 32), name = 'r0'), Expr ('Var', Type ("Word", 32), name = 'ret__int#v')), (Expr ('Var', Type ('Builtin', 'Mem'), name = 'mem'), Expr ('Var', Type ('Builtin', 'Mem'), name = 'Mem'))], 2, 1), (ProofNode ('Restr', (30, ('Number', (0, 3))), (ProofNode ('Restr', (8, ('Number', (0, 3))), (ProofNode ('Leaf', None, ()),)),)), ProofNode ('Restr', (30, ('Offset', (0, 3))), (ProofNode ('Restr', (8, ('Offset', (0, 3))), (ProofNode ('Leaf', None, ()),)),))))
22 .. proof found.
23Step 1: 
24  prove visits to 30 related to visits to 8
25    with equalities
26      ((Word32) ('r0')) (@ addr 30)
27      = ((Word32) ('ret__int#v')) (@ addr 8)
28      ((Mem) ('mem')) (@ addr 30)
29      = ((Mem) ('Mem')) (@ addr 8)
30    and with invariants
31      ((Word32) ('r13')) (@ addr 30)
32      ((Word32) ('ret')) (@ addr 30)
33      ((Word32) ('r9')) (@ addr 30)
34      ((Word32) ('r8')) (@ addr 30)
35      ((Word32) (('r5' + ((0 - '#seq-visits') * 4)))) (@ addr 30)
36      ((Word32) (('r4' + ((0 - '#seq-visits') * 1)))) (@ addr 30)
37      ((Bool) (ROData('mem'))) (@ addr 30)
38      ((Word32) ('r11')) (@ addr 30)
39      ((Word32) ('r6')) (@ addr 30)
40      ((Word32) ('r10')) (@ addr 30)
41      ((Word32) ('r7')) (@ addr 30)
42      ((RelWrapper) (StackWrapper(((Word32) (('r13' + 0))), ((Mem) ('stack'))))) (@ addr 30)
43      ((Word32) ('p#v')) (@ addr 8)
44      ((Word32) (('loop#2#count' + ((0 - '#seq-visits') * 1)))) (@ addr 8)
45      ((Word32) (('i#v' + ((0 - '#seq-visits') * 1)))) (@ addr 8)
46    .. proven.
47Step 2: case in (1) where the length of the sequence < 2
48  Prove the number of visits to 30 is in {0 ..< 3}
49    .. proven.
50Step 3: 
51  Prove the number of visits to 8 is in {0 ..< 3}
52    .. proven.
53Step 4: 
54  prove all verification conditions
55    .. proven.
56Step 5: case in (1) where the length of the sequence is i + 2
57  Prove the number of visits to 30 is in {i + 0 ..< i + 3}
58    .. proven.
59Step 6: 
60  Prove the number of visits to 8 is in {i + 0 ..< i + 3}
61    .. proven.
62Step 7: 
63  prove all verification conditions
64    .. proven.
65Refinement f -> Loop.f proven.
66