IFM 2025

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/ifm branch on both forks.

git clone git@github.com:ionchirica/cameleer.git
git clone git@github.com:ionchirica/gospel.git

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

opam switch create ifm 4.14.0
eval $(opam env --switch=ifm)

It may be possible that your version of GCC does no longer compile OCaml version 4.14.0. This issue has been filed here, and the fix can be found here.

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

git checkout ifm
opam pin add . 
eval $(opam env)

If everything was successful, you can now launch cameleer with the provided list of examples, found here, for instance, cameleer seq.ml. A 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, which is included in the zip.

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.