A Formal Proof of a Unix Path Resolution Algorithm
A Path Resolution Algorithm is shown terminating, correct and complete. The design of the formal specification and the implementation of the algorithm is described in the report A Formal Proof of a Unix Path Resolution Algorithm
Authors: Claude Marché / Martin Clochard / Ran Chen
Topics: Inductive predicates
Tools: Why3
References: CoLiS project / ProofInUse joint laboratory
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
A Formal Proof of an Unix Path Resolution Algorithm
Formalization of File Systems and Path Resolution
module FileSystem use import int.Int use import int.MinMax use export list.List use export option.Option
Pathnames
type filename type pathcomponent = Down filename | Up | Here
Up denotes ".." and Here denotes "."
type path = list pathcomponent
File System
type dirnode type child = | Absent | Dir dirnode | AbsLink path | RelLink path constant root : dirnode function lookup dirnode filename : child function parent dirnode : dirnode axiom parent_root: parent root = root axiom parent_non_root: forall d1 f d2. lookup d1 f = Dir d2 -> parent d2 = d1
Resolution Predicates
inductive resolve_to dirnode path dirnode = | ResolveNil : forall d. resolve_to d Nil d | ResolveDir : forall d1 fn d2 p d3. lookup d1 fn = Dir d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons (Down fn) p) d3 | ResolveAbsLink : forall d1 fn ps pr d2 d3. lookup d1 fn = AbsLink ps -> resolve_to root ps d2 -> resolve_to d2 pr d3 -> resolve_to d1 (Cons (Down fn) pr) d3 | ResolveRelLink : forall d1 fn ps pr d2 d3. lookup d1 fn = RelLink ps -> resolve_to d1 ps d2 -> resolve_to d2 pr d3 -> resolve_to d1 (Cons (Down fn) pr) d3 | ResolveUp: forall d1 d2 d3 p. parent d1 = d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons Up p) d3 | ResolveHere: forall d1 p d2. resolve_to d1 p d2 -> resolve_to d1 (Cons Here p) d2 inductive resolve_with_height dirnode path (option (dirnode,int)) = | ResolveHeightAbsent: forall d p. (forall d1. not resolve_to d p d1) -> resolve_with_height d p None | ResolveHeightNil : forall d. resolve_with_height d Nil (Some (d,0)) | ResolveHeightDir : forall d1 fn d2 p d3 h. lookup d1 fn = Dir d2 -> resolve_with_height d2 p (Some(d3,h)) -> resolve_with_height d1 (Cons (Down fn) p) (Some (d3,h + 1)) | ResolveHeightAbsLink : forall d1 fn ps pr d2 d3 h1 h2. lookup d1 fn = AbsLink ps -> resolve_with_height root ps (Some (d2,h1)) -> resolve_with_height d2 pr (Some (d3,h2)) -> resolve_with_height d1 (Cons (Down fn) pr) (Some (d3, max h1 h2 + 1)) | ResolveHeightRelLink : forall d1 fn ps pr d2 d3 h1 h2. lookup d1 fn = RelLink ps -> resolve_with_height d1 ps (Some (d2,h1)) -> resolve_with_height d2 pr (Some (d3,h2)) -> resolve_with_height d1 (Cons (Down fn) pr) (Some (d3,max h1 h2 + 1)) | ResolveHeightUp : forall d1 d2 d3 p h. parent d1 = d2 -> resolve_with_height d2 p (Some(d3, h)) -> resolve_with_height d1 (Cons Up p) (Some (d3,h + 1)) | ResolveHeightHere : forall d1 p d2 h. resolve_with_height d1 p (Some (d2,h)) -> resolve_with_height d1 (Cons Here p) (Some (d2,h + 1)) lemma resolve_height_resolve : forall d1 p d2 h. resolve_with_height d1 p (Some(d2, h)) -> resolve_to d1 p d2 lemma resolve_height_pos : forall d1 p d2 h. resolve_with_height d1 p (Some (d2,h)) -> h >= 0 lemma resolve_make_height : forall d1 p d2. resolve_to d1 p d2 -> exists h. resolve_with_height d1 p (Some(d2, h)) end
Conformance with POSIX informal definition
module POSIX_resolution use import FileSystem use import list.Append lemma resolve_to_append : forall d1 d2 d3 p q. ("induction" resolve_to d1 p d2) -> resolve_to d2 q d3 -> resolve_to d1 (p ++ q) d3 lemma resolve_to_cons : forall d1 d2 d3 c p. resolve_to d1 (Cons c Nil) d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons c p) d3 let lemma resolve_to_decomp (d1 d3:dirnode) (c:pathcomponent) (p2:path) requires { resolve_to d1 (Cons c p2) d3 } ensures { exists d2. resolve_to d1 (Cons c Nil) d2 /\ resolve_to d2 p2 d3 } = () let lemma resolve_to_decomposition (p1 p2:path) (d1 d3:dirnode) requires { resolve_to d1 (p1 ++ p2) d3 } ensures { exists d2. resolve_to d1 p1 d2 /\ resolve_to d2 p2 d3 } = () inductive resolve_to_POSIX dirnode path dirnode = | ResolveNilPOSIX : forall d. resolve_to_POSIX d Nil d | ResolveDirPOSIX : forall d1 fn d2 p d3. lookup d1 fn = Dir d2 -> resolve_to_POSIX d2 p d3 -> resolve_to_POSIX d1 (Cons (Down fn) p) d3 | ResolveAbsLinkPOSIX : forall d1 fn ps pr d2. lookup d1 fn = AbsLink ps -> resolve_to_POSIX root (ps ++ pr) d2 -> resolve_to_POSIX d1 (Cons (Down fn) pr) d2 | ResolveRelLinkPOSIX : forall d1 fn ps pr d2. lookup d1 fn = RelLink ps -> resolve_to_POSIX d1 (ps ++ pr) d2 -> resolve_to_POSIX d1 (Cons (Down fn) pr) d2 | ResolveUpPOSIX: forall d1 d2 d3 p. parent d1 = d2 -> resolve_to_POSIX d2 p d3 -> resolve_to_POSIX d1 (Cons Up p) d3 | ResolveHerePOSIX: forall d1 p d2. resolve_to_POSIX d1 p d2 -> resolve_to_POSIX d1 (Cons Here p) d2 lemma resolve_to_POSIX_append: forall d1 d2 p1. resolve_to_POSIX d1 p1 d2 -> forall p2 d3. resolve_to_POSIX d2 p2 d3 -> resolve_to_POSIX d1 (p1 ++ p2) d3 lemma resolve_to_equivalence: forall d1 d2 p. resolve_to_POSIX d1 p d2 <-> resolve_to d1 p d2 end
Determinism of Path Resolution
theory Determinism use import int.Int use import FileSystem lemma resolve_unique : forall d1 p d2. resolve_to d1 p d2 -> forall d3. resolve_to d1 p d3 -> d2 = d3 lemma resolve_with_height_unique: forall d p h1. resolve_with_height d p h1 -> forall h2. resolve_with_height d p h2 -> h1 = h2 by match h1, h2 with | None, None -> true | _, None | None, _ -> false | Some(_,u), Some(_,v) -> u = v end lemma resolve_with_height_exists : forall d p. exists h. resolve_with_height d p h end
Path Resolution Algorithm
module Resolution use import int.Int use import FileSystem use Determinism
obvious technical lemmas, but needed to help provers
lemma resolve_height_absLink: forall d x p r h ps d' h'. resolve_with_height d (Cons (Down x) p) (Some(r, h)) -> lookup d x = AbsLink ps -> resolve_with_height root ps (Some(d', h')) -> h' <= h lemma resolve_height_relLink: forall d x p r h ps d' h'. resolve_with_height d (Cons (Down x) p) (Some(r, h)) -> lookup d x = RelLink ps -> resolve_with_height d ps (Some(d', h')) -> h' <= h use import set.Fset use import map.Map type lnk = (dirnode,filename) constant alllinks : set lnk axiom alllinks_in : forall d fn ps. lookup d fn = AbsLink ps \/ lookup d fn = RelLink ps -> mem (d,fn) alllinks exception Error let rec aux_resolve (d: dirnode) (p:path) (active:set lnk) : dirnode requires { subset active alllinks } requires { forall d1 fn ps d2. mem (d1, fn) active -> lookup d1 fn = AbsLink ps -> resolve_to root ps d2 -> exists r. resolve_to d p r} requires { forall d1 fn ps d2. mem (d1, fn) active -> lookup d1 fn = RelLink ps -> resolve_to d1 ps d2 -> exists r. resolve_to d p r} requires { forall d1 fn ps d2 h1 d' h. mem (d1,fn) active -> lookup d1 fn = AbsLink ps -> resolve_with_height root ps (Some(d2, h1)) -> resolve_with_height d p (Some(d', h)) -> h <= h1 } requires { forall d1 fn ps d2 h1 d' h. mem (d1,fn) active -> lookup d1 fn = RelLink ps -> resolve_with_height d1 ps (Some(d2, h1)) -> resolve_with_height d p (Some (d',h)) -> h <= h1 } ensures { resolve_to d p result } raises { Error -> forall d'. not resolve_to d p d' } variant { cardinal alllinks - cardinal active, p } = assert {exists h. resolve_with_height d p h }; (* to help provers *) match p with | Nil -> d | Cons Up pr -> let d' = parent d in aux_resolve d' pr active | Cons Here pr -> aux_resolve d pr active | Cons (Down fn) pr -> match lookup d fn with | Absent -> raise Error | Dir d' -> aux_resolve d' pr active | AbsLink ps -> if mem (d,fn) active then raise Error else begin let actadd = add (d,fn) active in let d' = aux_resolve root ps actadd in aux_resolve d' pr active end | RelLink ps -> if mem (d, fn) active then raise Error else begin let actadd = add (d, fn) active in let d' = aux_resolve d ps actadd in aux_resolve d' pr active end end end let resolve (d: dirnode) (p:path) : dirnode ensures { resolve_to d p result } raises { Error -> forall d2. not resolve_to d p d2 } = aux_resolve d p empty end
Why3 Proof Results for Project "path_resolution"
Theory "path_resolution.FileSystem": fully verified in 25.88 s
Obligations | Alt-Ergo (1.01) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Z3 (4.4.1) | resolve_height_resolve | --- | --- | --- | --- | --- |
induction_pr | 1. | --- | --- | --- | --- | --- | |
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.04 | 0.02 | 0.02 | |
2. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.03 | 0.04 | 0.17 | 0.01 | |
3. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.04 | 0.06 | 0.05 | 6.44 | 0.02 | |
4. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 1.06 | Timeout (10s) | 0.06 | 6.10 | 0.02 | |
5. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 1.00 | Timeout (10s) | 0.05 | Timeout (10s) | 0.02 | |
6. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.03 | 0.03 | 0.04 | 0.17 | 0.02 | |
7. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.04 | 0.16 | 0.02 | resolve_height_pos | --- | --- | --- | --- | --- |
induction_pr | 1. | --- | --- | --- | --- | --- | |
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.04 | 0.02 | 0.01 | |
2. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.03 | 0.16 | 0.01 | |
3. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.04 | 0.03 | 0.16 | 0.01 | |
4. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.02 | 0.03 | 0.04 | 0.18 | 0.04 | |
5. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.03 | 0.18 | 0.03 | |
6. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.03 | 0.17 | 0.02 | |
7. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.01 | 0.02 | 0.04 | 0.17 | 0.02 | resolve_make_height | --- | --- | --- | --- | --- |
induction_pr | 1. | --- | --- | --- | --- | --- | |
simplify_trivial_quantification_in_goal | 1. | 0.02 | Timeout (10s) | 4.98 | 0.06 | Timeout (10s) | |
2. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.03 | Timeout (10s) | 0.05 | 1.26 | 0.01 | |
3. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | Timeout (10s) | Timeout (10s) | 0.13 | 2.55 | 0.02 | |
4. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | Timeout (10s) | Timeout (10s) | 0.12 | 3.57 | 0.02 | |
5. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.04 | Timeout (10s) | 0.05 | 0.17 | 0.02 | |
6. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.02 | 0.03 | 0.05 | 0.17 | 0.01 |
Theory "path_resolution.POSIX_resolution": fully verified in 24.09 s
Obligations | Alt-Ergo (1.01) | CVC3 (2.4.1) | CVC4 (1.4) | Coq (8.5pl1) | Eprover (1.8-001) | Z3 (4.4.1) | resolve_to_append | --- | --- | --- | --- | --- | --- |
induction_pr | 1. | 0.01 | 0.03 | 0.05 | --- | 0.02 | 0.01 | |
2. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.21 | Timeout (10s) | ||
3. | Timeout (10s) | Timeout (10s) | 0.05 | --- | 0.52 | Timeout (10s) | ||
4. | Timeout (10s) | Timeout (10s) | 0.07 | --- | 0.23 | Timeout (10s) | ||
5. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.20 | Timeout (10s) | ||
6. | 0.13 | Timeout (10s) | 0.05 | --- | 0.20 | Timeout (10s) | resolve_to_cons | Timeout (10s) | 2.62 | 0.05 | --- | 0.22 | 0.04 | VC for resolve_to_decomp | --- | --- | --- | --- | --- | --- |
induction_pr | 1. VC for resolve_to_decomp | 0.01 | 0.02 | 0.07 | --- | 0.02 | 0.02 | |
2. VC for resolve_to_decomp | Timeout (10s) | Timeout (10s) | Timeout (10s) | --- | 0.26 | Timeout (10s) | ||
3. VC for resolve_to_decomp | Timeout (10s) | Timeout (10s) | Timeout (10s) | --- | 0.67 | 0.04 | ||
4. VC for resolve_to_decomp | Timeout (10s) | Timeout (10s) | Timeout (10s) | --- | 0.83 | 0.04 | ||
5. VC for resolve_to_decomp | Timeout (10s) | Timeout (10s) | 1.14 | --- | 0.20 | Timeout (10s) | ||
6. VC for resolve_to_decomp | 1.20 | 0.08 | 0.71 | --- | 0.19 | 0.05 | VC for resolve_to_decomposition | --- | --- | --- | --- | --- | --- |
induction_ty_lex | 1. VC for resolve_to_decomposition | --- | --- | --- | --- | --- | --- | |
split_goal_wp | 1. postcondition | 0.15 | 0.03 | 0.09 | --- | 0.16 | 0.03 | |
2. postcondition | Timeout (10s) | Timeout (10s) | 7.22 | 1.61 | Timeout (10s) | Timeout (10s) | resolve_to_POSIX_append | --- | --- | --- | --- | --- | --- |
induction_pr | 1. | 0.02 | 0.03 | 0.05 | --- | 0.02 | 0.03 | |
2. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.43 | Timeout (10s) | ||
3. | Timeout (10s) | Timeout (10s) | 2.10 | --- | 0.42 | Timeout (10s) | ||
4. | Timeout (10s) | Timeout (10s) | 1.23 | --- | 0.36 | Timeout (10s) | ||
5. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.28 | Timeout (10s) | ||
6. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.28 | 3.14 | resolve_to_equivalence | --- | --- | --- | --- | --- | --- |
split_goal_wp | 1. | --- | --- | --- | --- | --- | --- | |
induction_pr | 1. | 0.02 | 0.03 | 0.04 | --- | 0.02 | 0.02 | |
2. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.27 | Timeout (10s) | ||
3. | Timeout (10s) | Timeout (10s) | 0.06 | --- | Timeout (10s) | Timeout (10s) | ||
4. | Timeout (10s) | Timeout (10s) | 0.08 | --- | Timeout (10s) | Timeout (10s) | ||
5. | Timeout (10s) | Timeout (10s) | 0.07 | --- | 0.27 | Timeout (10s) | ||
6. | 0.02 | 0.04 | 0.04 | --- | 0.26 | 0.03 | ||
2. | --- | --- | --- | --- | --- | --- | ||
induction_pr | 1. | 0.02 | 0.03 | 0.04 | --- | 0.03 | 0.02 | |
2. | Timeout (10s) | Timeout (10s) | 0.04 | --- | 0.28 | Timeout (10s) | ||
3. | Timeout (10s) | Timeout (10s) | 0.05 | --- | 0.29 | Timeout (10s) | ||
4. | Timeout (10s) | Timeout (10s) | 0.05 | --- | 0.31 | Timeout (10s) | ||
5. | Timeout (10s) | Timeout (10s) | 0.05 | --- | 0.27 | Timeout (10s) | ||
6. | 0.02 | 0.04 | 0.03 | --- | 0.26 | 0.03 |
Theory "path_resolution.Determinism": fully verified in 34.98 s
Obligations | Alt-Ergo (1.01) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Z3 (4.4.1) | resolve_unique | --- | --- | --- | --- | --- |
induction_pr | 1. | --- | --- | --- | --- | --- | ||
simplify_trivial_quantification_in_goal | 1. | 0.03 | Timeout (10s) | 7.00 | 0.17 | Timeout (10s) | ||
2. | --- | --- | --- | --- | --- | |||
simplify_trivial_quantification_in_goal | 1. | Timeout (10s) | 0.85 | Timeout (10s) | Timeout (10s) | Timeout (10s) | ||
3. | --- | --- | --- | --- | --- | |||
simplify_trivial_quantification_in_goal | 1. | --- | --- | --- | --- | --- | ||
inversion_pr | 1. | 0.01 | 0.02 | 0.04 | 0.02 | 0.01 | ||
2. | 0.01 | 0.02 | 0.04 | 0.17 | 0.02 | |||
3. | Timeout (10s) | 0.78 | 1.63 | 0.17 | 0.07 | |||
4. | 0.01 | 0.02 | 0.03 | 0.17 | 0.01 | |||
5. | 0.01 | 0.03 | 0.04 | 0.06 | 0.02 | |||
6. | 0.02 | 0.06 | 0.04 | 0.06 | 0.02 | |||
4. | --- | --- | --- | --- | --- | |||
simplify_trivial_quantification_in_goal | 1. | --- | --- | --- | --- | --- | ||
inversion_pr | 1. | 0.01 | 0.02 | 0.04 | 0.02 | 0.02 | ||
2. | 0.01 | 0.03 | 0.04 | 0.18 | 0.02 | |||
3. | 0.01 | 0.02 | 0.04 | 0.18 | 0.02 | |||
4. | Timeout (10s) | 0.06 | 1.31 | 0.18 | 0.06 | |||
5. | 0.01 | 0.02 | 0.04 | 0.06 | 0.02 | |||
6. | 0.01 | 0.07 | 0.04 | 0.06 | 0.02 | |||
5. | --- | --- | --- | --- | --- | |||
simplify_trivial_quantification_in_goal | 1. | 4.08 | 0.91 | 6.28 | Timeout (10s) | Timeout (10s) | ||
6. | --- | --- | --- | --- | --- | |||
simplify_trivial_quantification_in_goal | 1. | 3.52 | 0.31 | 4.09 | Timeout (10s) | Timeout (10s) | resolve_with_height_unique | --- | --- | --- | --- | --- |
split_goal_wp | 1. | 0.03 | Timeout (10s) | Timeout (10s) | Timeout (10s) | Timeout (10s) | ||
2. | 0.05 | Timeout (10s) | Timeout (10s) | 7.87 | Timeout (10s) | |||
3. | --- | --- | --- | --- | --- | |||
induction_pr | 1. | --- | --- | --- | --- | --- | ||
inversion_pr | 1. | 0.02 | 0.02 | 0.04 | 0.02 | 0.02 | ||
2. | 0.02 | 0.02 | 0.03 | 0.02 | 0.02 | |||
3. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | |||
4. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | |||
5. | 0.02 | 0.03 | 0.04 | 0.01 | 0.02 | |||
6. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | |||
7. | 0.02 | 0.03 | 0.14 | 0.02 | 0.02 | |||
2. | 0.01 | Timeout (10s) | Timeout (10s) | 0.17 | Timeout (10s) | |||
3. | --- | --- | --- | --- | --- | |||
inversion_pr | 1. | 0.02 | 0.03 | 0.05 | 0.02 | 0.02 | ||
2. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | |||
3. | Timeout (10s) | Timeout (10s) | 0.05 | 0.24 | Timeout (10s) | |||
4. | 0.02 | 0.03 | 0.05 | 0.24 | 0.02 | |||
5. | 0.02 | 0.03 | 0.05 | 0.19 | 0.02 | |||
6. | 0.02 | 0.02 | 0.04 | 0.18 | 0.02 | |||
7. | 0.02 | 0.08 | 0.04 | 0.18 | 0.02 | |||
4. | --- | --- | --- | --- | --- | |||
inversion_pr | 1. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | ||
2. | 0.02 | 0.03 | 0.05 | 0.02 | 0.03 | |||
3. | 0.02 | 0.03 | 0.06 | 0.19 | 0.02 | |||
4. | Timeout (10s) | Timeout (10s) | 0.12 | Timeout (10s) | Timeout (10s) | |||
5. | 0.02 | 0.04 | 0.05 | 0.18 | 0.02 | |||
6. | 0.02 | 0.03 | 0.05 | 0.19 | 0.02 | |||
7. | 0.02 | 0.15 | 0.05 | 0.19 | 0.02 | |||
5. | --- | --- | --- | --- | --- | |||
inversion_pr | 1. | 0.02 | 0.03 | 0.05 | 0.02 | 0.02 | ||
2. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | |||
3. | 0.02 | 0.03 | 0.05 | 0.18 | 0.02 | |||
4. | 0.02 | 0.03 | 0.06 | 0.18 | 0.03 | |||
5. | Timeout (10s) | Timeout (10s) | 0.13 | Timeout (10s) | Timeout (10s) | |||
6. | 0.02 | 0.03 | 0.05 | 0.11 | 0.03 | |||
7. | 0.02 | 0.20 | 0.05 | 0.19 | 0.02 | |||
6. | --- | --- | --- | --- | --- | |||
inversion_pr | 1. | 0.02 | 0.02 | 0.04 | 0.02 | 0.02 | ||
2. | 0.02 | 0.02 | 0.04 | 0.02 | 0.02 | |||
3. | 0.02 | 0.02 | 0.05 | 0.17 | 0.03 | |||
4. | 0.02 | 0.03 | 0.05 | 0.18 | 0.02 | |||
5. | 0.02 | 0.03 | 0.05 | 0.18 | 0.02 | |||
6. | Timeout (10s) | Timeout (10s) | 0.14 | 0.20 | Timeout (10s) | |||
7. | 0.02 | 0.08 | 0.04 | 0.18 | 0.02 | |||
7. | --- | --- | --- | --- | --- | |||
inversion_pr | 1. | 0.02 | 0.03 | 0.04 | 0.02 | 0.02 | ||
2. | 0.02 | 0.03 | 0.04 | 0.01 | 0.02 | |||
3. | 0.02 | 0.08 | 0.03 | 0.17 | 0.02 | |||
4. | 0.02 | 0.14 | 0.05 | 0.18 | 0.02 | |||
5. | 0.02 | 0.14 | 0.05 | 0.18 | 0.02 | |||
6. | 0.02 | 0.09 | 0.04 | 0.18 | 0.03 | |||
7. | Timeout (10s) | Timeout (10s) | 0.04 | 0.21 | Timeout (10s) | |||
4. | 0.18 | Timeout (10s) | 0.05 | 0.18 | 0.03 | resolve_with_height_exists | 0.02 | Timeout (10s) | 0.03 | 0.17 | Timeout (10s) |
Theory "path_resolution.Resolution": fully verified in 91.32 s
Obligations | Alt-Ergo (1.01) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Z3 (4.4.1) | resolve_height_absLink | Timeout (10s) | 0.18 | Timeout (10s) | Timeout (10s) | Timeout (10s) | resolve_height_relLink | Timeout (10s) | 0.16 | Timeout (10s) | Timeout (10s) | Timeout (10s) | VC for aux_resolve | --- | --- | --- | --- | --- |
split_goal_wp | 1. assertion | 0.05 | Timeout (10s) | 4.74 | 0.12 | Timeout (10s) |
2. postcondition | 0.01 | 0.04 | 0.06 | 0.03 | 0.03 | |
3. variant decrease | 0.01 | 0.04 | 0.07 | 0.23 | 0.03 | |
4. precondition | 0.01 | 0.04 | 0.06 | 0.07 | 0.03 | |
5. precondition | 0.23 | 0.24 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
6. precondition | 0.21 | 0.24 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
7. precondition | Timeout (10s) | Timeout (10s) | 0.14 | Timeout (10s) | 0.03 | |
8. precondition | Timeout (10s) | Timeout (10s) | 0.14 | Timeout (10s) | 0.04 | |
9. postcondition | 0.02 | 0.04 | 0.07 | 0.08 | 0.03 | |
10. exceptional postcondition | 0.11 | 0.11 | 4.76 | Timeout (10s) | 2.33 | |
11. variant decrease | 0.02 | 0.04 | 0.06 | 0.22 | 0.04 | |
12. precondition | 0.02 | 0.04 | 0.05 | 0.07 | 0.03 | |
13. precondition | 0.19 | 0.24 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
14. precondition | 0.19 | 0.23 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
15. precondition | 2.45 | Timeout (10s) | 0.15 | Timeout (10s) | 0.03 | |
16. precondition | 2.16 | Timeout (10s) | 0.14 | Timeout (10s) | 0.03 | |
17. postcondition | 0.02 | 0.04 | 0.07 | 0.25 | 0.02 | |
18. exceptional postcondition | 0.10 | 0.11 | 4.66 | Timeout (10s) | 2.29 | |
19. exceptional postcondition | 0.04 | 0.08 | Timeout (10s) | Timeout (10s) | 1.71 | |
20. variant decrease | 0.02 | 0.04 | 0.06 | 0.23 | 0.04 | |
21. precondition | 0.02 | 0.03 | 0.05 | 0.07 | 0.02 | |
22. precondition | 0.15 | 0.28 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
23. precondition | 0.13 | 0.27 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
24. precondition | Timeout (10s) | Timeout (10s) | 0.12 | Timeout (10s) | 0.03 | |
25. precondition | Timeout (10s) | Timeout (10s) | 0.13 | Timeout (10s) | 0.04 | |
26. postcondition | 0.02 | 0.04 | 0.06 | 0.26 | 0.03 | |
27. exceptional postcondition | 0.05 | 0.12 | 7.92 | Timeout (10s) | Timeout (10s) | |
28. exceptional postcondition | 4.50 | Timeout (10s) | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
29. variant decrease | 0.03 | 0.05 | 0.07 | Timeout (10s) | 0.03 | |
30. precondition | Timeout (10s) | 0.13 | 0.07 | Timeout (10s) | 0.02 | |
31. precondition | 0.55 | 0.34 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
32. precondition | 0.45 | 0.37 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
33. precondition | 8.17 | Timeout (10s) | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
34. precondition | 3.90 | Timeout (10s) | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
35. variant decrease | 0.03 | 0.05 | 0.07 | 0.24 | Timeout (10s) | |
36. precondition | 0.02 | 0.04 | 0.05 | 0.08 | 0.02 | |
37. precondition | Timeout (10s) | 1.65 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
38. precondition | Timeout (10s) | 1.81 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
39. precondition | Timeout (10s) | Timeout (10s) | 2.37 | Timeout (10s) | 4.80 | |
40. precondition | Timeout (10s) | Timeout (10s) | 2.35 | Timeout (10s) | 1.46 | |
41. postcondition | 0.03 | Timeout (10s) | 0.07 | Timeout (10s) | 0.03 | |
42. exceptional postcondition | Timeout (10s) | 0.96 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
43. exceptional postcondition | 0.05 | 0.24 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
44. exceptional postcondition | 1.62 | Timeout (10s) | Timeout (10s) | Timeout (10s) | 6.25 | |
45. variant decrease | 0.03 | 0.04 | 0.07 | Timeout (10s) | 0.03 | |
46. precondition | 0.03 | Timeout (10s) | 4.79 | Timeout (10s) | Timeout (10s) | |
47. precondition | 0.48 | 0.31 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
48. precondition | 0.47 | 0.31 | 6.07 | Timeout (10s) | Timeout (10s) | |
49. precondition | 4.27 | Timeout (10s) | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
50. precondition | 7.45 | Timeout (10s) | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
51. variant decrease | 0.03 | 0.04 | 0.08 | 0.25 | 0.30 | |
52. precondition | 0.02 | 0.04 | 0.06 | 0.07 | 0.03 | |
53. precondition | Timeout (10s) | 1.92 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
54. precondition | Timeout (10s) | 2.89 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
55. precondition | Timeout (10s) | Timeout (10s) | 2.04 | Timeout (10s) | 3.09 | |
56. precondition | Timeout (10s) | Timeout (10s) | 1.73 | Timeout (10s) | 0.47 | |
57. postcondition | 0.03 | Timeout (10s) | 0.08 | 0.29 | 0.02 | |
58. exceptional postcondition | Timeout (10s) | 0.94 | Timeout (10s) | Timeout (10s) | Timeout (10s) | |
59. exceptional postcondition | 0.16 | 0.23 | Timeout (10s) | Timeout (10s) | Timeout (10s) | VC for resolve | --- | --- | --- | --- | --- |
split_goal_wp | 1. precondition | 0.03 | 0.03 | 0.06 | 0.21 | 0.03 |
2. precondition | 0.02 | 0.04 | 0.05 | 0.02 | 0.02 | |
3. precondition | 0.01 | 0.04 | 0.06 | 0.02 | 0.02 | |
4. precondition | 0.03 | 0.04 | 0.05 | 0.02 | 0.03 | |
5. precondition | 0.03 | 0.03 | 0.06 | 0.03 | 0.03 | |
6. postcondition | 0.03 | 0.03 | 0.05 | 0.03 | 0.01 | |
7. exceptional postcondition | 0.03 | 0.04 | 0.07 | 0.03 | 0.00 |