INForum 2024

Installation & Configuration

To install both Cameleer and Gospel, one should use a specific branch of a fork. Start by cloning Cameleer and Gospel, and checkout to the origin/iteration branch on both forks.

I recommend making a new opam switch (naming it inforum, for example) with the 4.14.0 base compiler:

opam switch inforum 4.14.0
eval $(opam env --switch=inforum)

Then, one should first install Gospel and Cameleer (on the origin/iteration branches), with the following command in both directories:

opam pin add . kind=path
eval $(opam env)

If everything was successful, one should now be able to run cameleer.

Code and Specification

A zip with the full list of examples can be found here. One strategy that can be used, in Why3, is to select a Verification Condition or Module and press R, this will re-run the saved session.

Statistics (Per Module)

Seq

Why3 Proof Results for Project "seq"

Theory "seq.Seq": fully verified

Obligations		Alt-Ergo 2.5.4	CVC4 1.7	CVC5 1.2.0
List.T.Fold.permitted_empty		---	---	---
split_vc
	permitted_empty.0	0.06	---	---
List.T.Iter.permitted_empty		---	---	---
split_vc
	permitted_empty.0	0.08	---	---
List.T.Map.permitted_empty		0.07	---	---
List.T.Filter.permitted_empty		0.08	---	---
VC for sum_of_seq		---	---	---
split_vc
	loop invariant init	0.10	---	---
	precondition	0.08	---	---
	precondition	0.09	---	---
	loop variant decrease	0.08	---	---
	loop invariant preservation	8.89	---	---
	postcondition	4.16	---	---
VC for stack_of_seq		4.99	---	---
VC for queue_of_seq		---	---	---
split_vc
	loop invariant init	0.12	---	---
	precondition	0.10	---	---
	precondition	0.09	---	---
	loop variant decrease	0.11	---	---
	loop invariant preservation	0.19	---	---
	postcondition	0.13	---	---
VC for filter_seq		0.66	---	---
VC for map_seq		0.21	---	---
VC for gt_seq		---	---	---
split_vc
	loop invariant init	0.12	---	---
	precondition	0.10	---	---
	precondition	0.09	---	---
	loop variant decrease	0.12	---	---
	loop invariant preservation	0.29	---	---
	loop variant decrease	0.11	---	---
	loop invariant preservation	0.28	---	---
	postcondition	---	12.24	12.83

Oper

Why3 Proof Results for Project "oper"

Theory "oper.Oper": fully verified

Obligations			Alt-Ergo 2.5.4	CVC4 1.7	CVC5 1.2.0
equal_hashes_COMPARABLE			0.06	---	---
VC for gt			---	---	---
exists (empty1: fset t)
	gt'vc.0		---	---	---
	exists (fun (_: t) -> empty1: fset t)
		gt'vc.0.0	---	---	0.17
Oper.G.Fold_vertex.permitted_empty			0.09	---	---
Oper.G.Fold_succ.permitted_empty			0.09	---	---
Oper.G.Fold_succ_e.permitted_empty			0.10	---	---
Oper.G.Fold_edges.permitted_empty			0.10	---	---
VC for copy_vertices			---	---	---
split_vc
	loop invariant init		0.13	---	---
	precondition		0.11	---	---
	precondition		0.09	---	---
	loop variant decrease		0.15	---	---
	loop invariant preservation		0.29	---	---
	postcondition		0.14	---	---
	postcondition		0.11	---	---
VC for intersect			---	---	---
split_vc
	loop invariant init		0.14	---	---
	precondition		0.09	---	---
	precondition		0.07	---	---
	loop invariant init		0.47	---	---
	precondition		0.10	---	---
	precondition		0.09	---	---
	loop variant decrease		0.24	---	---
	loop invariant preservation		0.97	---	---
	loop variant decrease		0.21	---	---
	loop invariant preservation		0.19	---	---
	loop variant decrease		0.15	---	---
	loop invariant preservation		0.39	---	---
	postcondition		0.20	---	---
	postcondition		0.11	---	---
VC for mirror			---	---	---
split_vc
	loop invariant init		0.14	---	---
	precondition		0.11	---	---
	precondition		0.09	---	---
	loop variant decrease		0.17	---	---
	loop invariant preservation		---	1.21	---
	postcondition		0.14	---	---
	postcondition		0.12	---	---
VC for complement			---	---	---
split_vc
	loop invariant init		0.31	---	---
	precondition		0.11	---	---
	precondition		0.09	---	---
	loop invariant init		0.88	---	---
	precondition		0.11	---	---
	precondition		0.10	---	---
	loop variant decrease		0.20	---	---
	loop invariant preservation		1.99	---	---
	loop variant decrease		0.18	---	---
	loop invariant preservation		0.42	---	---
	postcondition		0.13	---	---
	postcondition		0.12	---	---
	postcondition		0.12	---	---
VC for union			---	---	---
split_vc
	loop invariant init		0.26	---	---
	precondition		0.11	---	---
	precondition		0.09	---	---
	loop invariant init		1.13	---	---
	precondition		0.12	---	---
	precondition		0.09	---	---
	loop variant decrease		0.23	---	---
	loop invariant preservation		1.28	---	---
	loop variant decrease		0.21	---	---
	loop invariant preservation		0.36	---	---
	postcondition		0.13	---	---
	postcondition		---	0.60	---

Path

Why3 Proof Results for Project "path"

Theory "path.Path": fully verified

Obligations																Alt-Ergo 2.5.2	Alt-Ergo 2.5.4	CVC4 1.7
seq_cons																0.04 (obsolete)	0.09	---
equal_hashes_HASHABLE																0.04 (obsolete)	0.08	---
equal_hashes_COMPARABLE																0.04 (obsolete)	0.08	---
VC for gt																---	---	---
exists (empty1: fset t)
	gt'vc.0															---	---	---
	exists (fun(_:t) -> empty1: fset t)
		gt'vc.0.0														0.06 (obsolete)	0.10	---
Check.G.Iter_succ.permitted_empty																0.04 (obsolete)	0.10	---
Check.path_suc																---	---	---
split_vc
	path_suc.0															---	---	---
	unfold has_path
		path_suc.0.0														---	---	---
		unfold has_path in H1
			path_suc.0.0.0													---	---	---
			introduce_exists
				path_suc.0.0.0.0												---	---	---
				exists (snoc p v3)
					path_suc.0.0.0.0.0											0.11 (obsolete)	0.18	---
Check.edge_path																0.06 (obsolete)	0.11	---
Check.self_path																0.10 (obsolete)	0.11	---
VC for intermediate_value_func																result missing (obsolete)	1.65	---
Check.intermediate_value																---	---	---
split_vc
	intermediate_value.0															---	---	---
	instantiate intermediate_value_func'spec p,u,v
		intermediate_value.0.0														---	---	---
		instantiate Hinst (to_list s)
			intermediate_value.0.0.0													---	---	---
			instantiate Hinst g
				intermediate_value.0.0.0.0												---	---	---
				destruct_rec Hinst
					destruct premise											0.04 (obsolete)	0.09	---
					destruct premise											0.05 (obsolete)	0.09	---
					destruct premise											0.25 (obsolete)	0.28	---
					intermediate_value.0.0.0.0.3											0.44 (obsolete)	0.40	---
VC for check_path																---	---	---
split_vc
	postcondition															0.08 (obsolete)	0.15	---
	postcondition															0.08 (obsolete)	0.09	---
	postcondition															0.08 (obsolete)	0.12	---
	postcondition															0.05 (obsolete)	0.09	---
	postcondition															0.05 (obsolete)	0.09	---
	postcondition															0.06 (obsolete)	0.11	---
	postcondition															0.08 (obsolete)	0.09	---
	postcondition															0.06 (obsolete)	0.10	---
	postcondition															0.07 (obsolete)	0.11	---
	postcondition															0.09 (obsolete)	0.14	---
	postcondition															0.08 (obsolete)	0.11	---
	postcondition															0.06 (obsolete)	0.09	---
	postcondition															result missing (obsolete)	0.20	---
	postcondition															result missing (obsolete)	0.37	---
	postcondition															result missing (obsolete)	1.11	---
	postcondition															result missing (obsolete)	0.09	---
	postcondition															result missing (obsolete)	0.10	---
	postcondition															result missing (obsolete)	0.11	---
	postcondition															result missing (obsolete)	0.10	---
	postcondition															---	---	---
	unfold disjoint
		VC for check_path														result missing (obsolete)	2.04	---
	postcondition															result missing (obsolete)	0.12	---
	postcondition															result missing (obsolete)	0.16	---
	postcondition															result missing (obsolete)	0.52	---
	postcondition															result missing (obsolete)	0.10	---
	precondition															result missing (obsolete)	0.44	---
	loop invariant init															---	---	---
	split_vc
		loop invariant init														---	---	---
		inline_goal
			loop invariant init													---	---	---
			split_all_full
				VC for check_path												result missing (obsolete)	0.18	---
				VC for check_path												result missing (obsolete)	0.53	---
				VC for check_path												result missing (obsolete)	0.10	---
				VC for check_path												1.32 (obsolete)	---	---
				split_vc
					VC for check_path											result missing (obsolete)	1.03	---
				VC for check_path												result missing (obsolete)	0.13	---
				VC for check_path												result missing (obsolete)	0.14	---
				VC for check_path												---	---	---
				unfold disjoint
					VC for check_path											---	---	---
					split_vc
						VC for check_path										result missing (obsolete)	1.05	---
						VC for check_path										result missing (obsolete)	1.06	---
				VC for check_path												result missing (obsolete)	0.18	---
				VC for check_path												result missing (obsolete)	0.62	---
				VC for check_path												result missing (obsolete)	0.10	---
				VC for check_path												result missing (obsolete)	0.15	---
				VC for check_path												result missing (obsolete)	0.10	---
				VC for check_path												---	---	---
				inline_goal
					VC for check_path											result missing (obsolete)	0.13	---
	precondition															result missing (obsolete)	0.13	---
	precondition															result missing (obsolete)	0.10	---
	loop variant decrease															result missing (obsolete)	0.56	---
	loop invariant preservation															---	---	---
	split_vc
		loop invariant preservation														---	---	---
		inline_goal
			loop invariant preservation													---	---	---
			split_all_full
			VC for check_path												result missing (obsolete)	0.14	---
			VC for check_path												result missing (obsolete)	1.08	---
			VC for check_path												---	---	---
			split_vc
				VC for check_path											---	---	---
				inline_goal
					VC for check_path										result missing (obsolete)	Timeout (30.00s)	16.93
			VC for check_path												result missing (obsolete)	0.57	---
			VC for check_path												result missing (obsolete)	6.46	---
			VC for check_path												result missing (obsolete)	0.51	---
			VC for check_path												result missing (obsolete)	4.82	---
			VC for check_path												result missing (obsolete)	0.22	---
			VC for check_path												result missing (obsolete)	0.51	---
			VC for check_path												result missing (obsolete)	0.14	---
			VC for check_path												result missing (obsolete)	0.15	---
			VC for check_path												result missing (obsolete)	0.22	---
			VC for check_path												result missing (obsolete)	0.94	---
loop variant decrease															result missing (obsolete)	0.52	---
loop invariant preservation															result missing (obsolete)	1.05	---
variant decrease															result missing (obsolete)	0.42	---
precondition															---	---	---
case (mem3 v1 q.view2)
	true case (precondition)														result missing (obsolete)	0.14	---
	false case (precondition)														---	---	---
	case (mem3 v2 q.view2)
		false case (true case. precondition)													result missing (obsolete)	0.41	---
		false case (precondition)													---	---	---
		assert (not mem1 v2 visited.dom)
			asserted formula												result missing (obsolete)	0.14	---
			false case (precondition)												---	---	---
			assert (mem1 v1 visited.dom)
				asserted formula											result missing (obsolete)	0.13	---
				false case (precondition)											---	---	---
				instantiate intermediate_value (fun x -> mem1 x visited.dom)
					false case (precondition)										---	---	---
					instantiate Hinst v1,v2
						false case (precondition)									---	---	---
						unfold has_path in H
							false case (precondition)								---	---	---
							introduce_exists
								false case (precondition)							---	---	---
								instantiate Hinst p,graph
									false case (precondition)						---	---	---
									destruct Hinst
										destruct premise					result missing (obsolete)	0.14	---
										false case (precondition)					---	---	---
										destruct Hinst
											destruct premise				result missing (obsolete)	0.14	---
											false case (precondition)				---	---	---
											destruct Hinst
												destruct premise			result missing (obsolete)	0.11	---
												false case (precondition)			---	---	---
												introduce_exists
													false case (precondition)		---	---	---
													exists v'
														check_path'vc.33.1.1.1.1.0.0.0.0.0.1.1.1.0.0	result missing (obsolete)	1.39	---
precondition															result missing (obsolete)	0.14	---
precondition															result missing (obsolete)	0.20	---
precondition															result missing (obsolete)	0.40	---
precondition															---	---	---
assert (forall vt. mem4 vt sucs -> mem1 vt graph.dom1)
	asserted formula														result missing (obsolete)	0.21	---
	precondition														result missing (obsolete)	0.14	---
precondition															result missing (obsolete)	0.20	---
precondition															result missing (obsolete)	0.14	---
precondition															result missing (obsolete)	0.14	---
precondition															result missing (obsolete)	0.21	---
precondition															---	---	---
split_vc
	precondition														result missing (obsolete)	0.47	---
precondition															result missing (obsolete)	0.21	---
precondition															result missing (obsolete)	0.21	---
precondition															result missing (obsolete)	0.14	---
postcondition															result missing (obsolete)	0.11	---
postcondition															result missing (obsolete)	0.10	---
postcondition															result missing (obsolete)	0.15	---
postcondition															result missing (obsolete)	0.10	---
postcondition															result missing (obsolete)	0.11	---
postcondition															result missing (obsolete)	0.14	---
postcondition															result missing (obsolete)	0.11	---
postcondition															result missing (obsolete)	0.11	---
postcondition															result missing (obsolete)	0.14	---
postcondition															result missing (obsolete)	0.22	---
postcondition															result missing (obsolete)	0.14	---
postcondition															result missing (obsolete)	0.11	---
exceptional postcondition															result missing (obsolete)	0.10	---
precondition															result missing (obsolete)	0.15	---
precondition															result missing (obsolete)	0.13	---
precondition															result missing (obsolete)	0.14	---
precondition															result missing (obsolete)	0.21	---
precondition															result missing (obsolete)	0.23	---
precondition															result missing (obsolete)	0.23	---
precondition															result missing (obsolete)	0.26	---
precondition															result missing (obsolete)	0.35	---
precondition															result missing (obsolete)	0.13	---
precondition															result missing (obsolete)	0.26	---
precondition															result missing (obsolete)	0.14	---
precondition															result missing (obsolete)	0.18	---
precondition															result missing (obsolete)	0.12	---
postcondition															result missing (obsolete)	0.09	---

Tree

Why3 Proof Results for Project "tree"

Theory "tree.Tree": fully verified

Obligations		Alt-Ergo 2.5.4	CVC5 1.2.0
Tree.T.Fold.permitted_empty		0.08	---
Tree.T.Fold_level.permitted_empty		0.09	---
Tree.T.Iter.permitted_empty		0.06	---
Tree.T.Filter.permitted_empty		0.09	---
VC for sum_tree		---	---
split_vc
	loop invariant init	0.06	---
	precondition	0.08	---
	precondition	0.07	---
	loop variant decrease	0.10	---
	loop invariant preservation	9.40	---
	postcondition	3.78	---
VC for tree_height		0.09	---
VC for gt_seq		---	---
split_vc
	loop invariant init	0.14	---
	precondition	0.11	---
	precondition	0.09	---
	loop variant decrease	0.13	---
	loop invariant preservation	0.33	---
	loop variant decrease	0.13	---
	loop invariant preservation	0.30	---
	postcondition	---	1.92

Platform used

The benchmarks were conducted on a machine with a processor i5-2520M 2 cores @ 3.2GHz; 12Gb RAM; 64-bit linux kernel 6.9.5.