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