This project is the companion Rocq development of the paper "TypeDis: A Type System for Disentanglement".

See INSTALL.md.

Rocq files are located in the src/ directory.

The architecture is as follows:

• lang/ contains the syntax and semantics of the language.
• newlang/ contains an alternative definition of the semantics that we use in the proofs. Our final theorems all make use of the original semantics in lang/.
• logic/ contains the DisLog2 logic.
  • The wpg.v file defines the general wpg.
  • The wp.v file defines wp, the specialization of wpg to leaves, and gather lemmas.
  • The wpg_adequacy.v file contains the soundness theorem of wpg which is specialized to wp in wp_adequacy.v.
• types/ contains the TypeDis type system.
  • The typing.v file defines the syntax of types.
  • The syntactical.v file defines the type system.
  • The logrel.v file defines logical relations.
  • The final_theorem.v file proves the fundamental theorem of the logical relation and the soundness theorem.
• examples/ contains various examples.
• utils/ contains some utility files.

Rocq files are located in the src/ directory.

TypeDis' typing judgment Δ | Γ ⊢ e : ρ ⊲ δ, takes in Rocq the form typed δ Δ Ω Γ e ρ, where Ω is the environment associating type variables to their kind (merged with Γ in the paper).

Compared with the paper, soundness theorems require that the initial program e does not contain any location value---such locations are allocated dynamically. This hypothesis is written locs e = ∅.

• Figures 3 and 4: file examples/key_ideas.v
• Figures 5 and 6: file examples/itree.v The code presented in the paper omits technical fold/unfold instructions. In the formalization, type for the leaf and node constructor are polymorphic in the type of the leaves.
• Figure 7: file lang/syntax.v
• Figure 8: file lang/head_semantics.v
• Figure 9: file lang/semantics_cycle.v (which is re-exported from lang/semantics.v)
• Figure 10: file lang/disentangled.v Compared to the paper, the function leaves is named frontier.
• Section 3.3, paragraph "Difference with Previous Semantics for Disentanglement": file lang/old_semantics/semantics_equiv_more.v, lemmas rtc_step_old_to_new and rtc_step_new_to_old.
• Figure 11: file types/typing.v
  • Timestamp variables are of type stimestamp.
  • Logical graphs are set edges, represented as pair of stimestamps.
  • Kinds are integers.
  • Unboxed types are of type tbase.
  • Boxed types are of type typat.
  • Types are of type typ.
  • Environments are maps from type variables to types.
  • As explained above, the environment of kinds Ω is separated from the environment Γ in the formalization.
• Figure 12: file types/syntactical.v, inductive typed
• Figure 13: file types/syntactical.v, inductive subtime_typ
• Figure 14:
  • The predicate AllRedOrOOB is called reducible and appears in file lang/reducible.v. It is parameterized by a boolean indicating if an OOB is allowed to occur. This parameter is instantiated to true during the soundness proof of TypeDis, but can be left to false to have a stronger statement.
  • The predicate Safe appears in logic/wpg_adequacy.v.
• Theorem 5.1: file types/final_theorem.v, lemma soundness
• Figure 15:
  • D-Load: file logic/wp.v, lemma wp_load
  • D-LoadOOB: file logic/wpg_load.v, lemma wpg_load_escape
  • D-Par: file logic/wp.v, lemma wp_par
  • D-ClockMono: file logic/interp.v, lemma clock_mon
• Theorem 5.2: file logic/wp_adequacy.v, lemma wp_adequacy
• Figure 16: file types/fundamental.v, definition log_typed. Please unfold definitions when needed, the figure in the paper inlines a lot of intermediate names.
• Theorem 5.3: file types/final_theorem.v, lemma fundamental
• Figure 17: file examples/stdlib.v, definitions parfor and parfor_typed.
• Figure 18: file examples/dedup.v, definitions hs_add and dedup as well as hs_add_typed and dedup_typed

Appendix:

• Figure 19: file types/typing.v, definition wk_typ
• Figure 20: file types/syntactical.v, definition very_pure
• Figure 21: file utils/graph.v, definition reachable
• Figure 22: file types/syntactical.v, definition valid_variable_typ
• Figure 23: file types/troot.v, definition troot
• Figure 24: file types/logrel.v, definition interp_typ

Users can check that all files compile and that no Admitted or Axiom remains. It suffices to open the file src/noaxioms.v and play with it interactively. If the Rocq command Print Assumptions xxx prints "Closed under the global context", it indicates that xxx has no dependencies (reference).

Users can also open some selected .v files inside CoqIDE or Proof General and evaluate the whole file to check that no errors occur and to verify that the objects and statements mentioned in the claims are what they are supposed to be.

NB: There is a hack to work with ProofGeneral. We have a dumb src/_CoqProject which makes visible the files produced by dune.

See issue: ProofGeneral/PG#477