Spy game

Contents

• orders_ext.v: Theory of complete lattices.

• optimal_least_fixed_point.v: Theory of optimal least fixed points. The file features the definition and the proof of existence of the optimal least fixed point.

• type_repr.v: Link between Coq terms and HeapLang values plus definition of the 'implements' predicate. Intimately related to section 3.2.

• proph_lib.v: Reasoning rules for prophecy variables, namely the disposal rule and the extension to typed prophecy variables explained in section 3.3.

• conjunction.v: Proof of the restricted infinitary conjunction rule and definition of the conjApply combinator.

• lists.v: Verified library for HeapLang code manipulating lists.

• maps.v: Verified library for HeapLang code manipulating a parametric implementation of maps.

• modulus.v: Proof and specification of modulus. The file proposes two specifications: the first one corresponds to the rule used in proof of lfp, while the second one (proved as a corollary of the first) corresponds to the specification shown on section 7.

• fix.v: Proof and specification of lfp.