The Logical Essence of Well-Bracketed Control Flow

A Program logic on top of Iris for reasoning about well-bracketed control flow.

---

Links & Downloads:

• Github repository
• artifact [.tar.gz]
• accompanying technical appendix [.pdf]
• Artifact on Zenodo

---

The structure of the Coq development:

The links below open the browsable html version of the corresponding Coq file (produced by the coqdoc tool and enhanced by coqdocjs). The Coq development is organized as follows.

• F_mu_ref: Unary and binary logical relations models for F_mu_ref.
  • base.v: Some basic definitions and tactics.
  • binary: The binary logical relations model.
    • context_refinement.v: The definition of contextual refinement and some lemmas.
    • examples: Examples of using our binary logical relations model.
      • fact.v: Equivalence of two factorial implementations.
      • very_awkward.v: The contextual equivalence of VAE.
    • fundamental.v: The fundamental theorem of binary logical relations.
    • logrel.v: The definition of binary logical relations.
    • rules.v: Rules for resources for tracking the specification-side program.
    • soundness.v: Soundness theorem of binary logical relations.
  • lang.v: The definition (syntax & op sem) of F_mu_ref.
  • typing.v: The typing rules of F_mu_ref.
  • unary: The unary logical relations model.
    • examples: Examples of using our unary logical relations model.
      • very_awkward.v: The VAE example using the unary logical relations.
    • fundamental.v: The fundamental theorem of the unary logical relations model.
    • logrel.v: The definition of the unary logical relations.
    • soundness.v: Soundness of the unary logical relations model.
  • wp_rules.v: The (well-bracketed) weakest precondition rules for F_mu_ref.
• heap_lang: A copy of the necessary parts of heap lang from the Iris development.
  • adequacy.v: The adequacy theorem.
  • derived_laws.v: Derived rules for well-bracketed weakest preconditions.
  • primitive_laws.v: Primitive rules for weakest preconditions.
  • proofmode.v: Lemmas and tactics for proofmode support for heap_lang programs.
• heap_lang_examples: Examples on top of heap lang.
  • awkward.v: The awkward example.
  • sts: Examples using the STS encoding.
    • very_awkward.v: The STS version of VAE.
  • very_awkward.v: VAE proven well-bracketed in heap lang.
• heap_lang_trace: The version of heap lang with intensional traces.
  • adequacy.v: The adequacy theorem.
  • class_instances.v: Type classes for Iris's proof mode.
  • derived_laws.v: Derived rules for well-bracketed weakest preconditions.
  • lang.v: Definition of the language heaplang with added trace primitives.
  • notation.v: Useful notations for writing programs.
  • primitive_laws.v: Primitive rules for weakest preconditions.
  • proofmode.v: Lemmas and tactics for proofmode support for heap_lang programs.
  • tactics.v: Supporting tactics for defining proofmode tactics.
  • trace_resources.v: Iris resources for reasoning about program traces.
• heap_lang_trace_examples: Examples using intensional trace properties in heap lang.
  • sequential_trace_alt.v: The definition of well-bracketed trace of calls and returns.
  • very_awkward.v: The VAE example proven to produce well-bracketed traces.
• oneshot.v: The definition of the one-shot resource algebra
• persistent_pred.v: Definition of persistent predicates used in logical relations.
• program_logic: The well-bracketed program logic.
  • adequacy.v: The adequacy theorem of the well-bracketed program logic.
  • ghost_stacks.v: The theory of ghost stacks including resource algebras.
  • lib: Developments on top of the well-bracketed program logic.
    • sts.v: The encoding of STSs using ghost stacks.
  • lifting.v: A couple of useful lemmas.
  • weakestpre.v: Definition of well-bracketed weakest preconditions.