Syng

Syng is concurrent separation logic with propositional ghost state, fully mechanized in Agda.

Syng supports propositional ghost state, which brings powerful expressivity, just like an existing separation logic Iris (Jung et al., 2015).
Notably, Syng supports propositional invariants (a.k.a. impredicative invariants).

But in contrast to Iris's fully semantic approach, Syng models the propositional ghost state simply using the logic's syntax (for propositions and judgments).

As a result, while Iris suffers from step indexing everywhere, Syng is not step-indexed at all.
Thanks to that, Syng has intuitive, easy-to-extend semantics and can flexibly support termination-sensitive program reasoning.

Syng is mechanized in Agda, a modern, dependently typed programming language.
Agda is chosen here rather than Coq, Lean, etc., because Agda has excellent support of coinduction enabled by sized types, and Syng's approach takes great advantage of that.

Getting Started

Just install Agda. Syng is known to work with Agda 2.6.2.2.
Syng has no dependencies on external libraries.

Agda Mode

For viewing and editing Agda code, you can use Agda mode for Emacs or VS Code.

When you open an Agda file, you should first load the file (Ctrl-c Ctrl-l in Emacs and VS Code), which loads and type-checks the contents of the file and its dependencies.

Also, you can quickly jump to the definition (Meta-. in Emacs and F12 in VS Code) of any identifiers, including those that use symbols.

Fonts

Syng's source code uses a lot of Unicode characters.
To render them beautifully, we recommend you use monospace Unicode fonts that support these characters, such as the following:

• JuliaMono ― Has a huge Unicode cover, including all the characters used in Syng's source code.
• Menlo ― Is preinstalled on Mac and pretty beautiful. Doesn't support some characters (e.g., ⊢).

For example, in VS Code, you can use the following setting (in settings.json) to use Menlo as the primary font and fill in some gaps with JuliaMono.

"editor.fontFamily": "Menlo, JuliaMono"

Learning Agda

You can learn Agda's language features from the official document.

Here are notable features used in Syng.

• Sized types ― Enable flexible coinduction and induction, especially in combination with thunks and shrunks.
• With-abstractions ― Allow case analysis on calculated values.
• Copatterns ― Get access to a component of records like a pattern.
• Record modules ― Extend record types with derived notions, effectively used by the type ERA.

Source Code

In the folder src is the Agda source code for Syng.

Base/

In Base/ is a general-purpose library (though newly developed for Syng). Some of them re-export Agda's built-in libraries, possibly with renaming. The library consists of the following parts.

• Basics ― Level for universe levels; Func for functions; Few for two-, one- and zero-element sets; Eq for equality; Dec for decidability; Acc for accessibility; Size for sizes (modeling ordinals), thunks and shrunks.
• Data types ― Bool for Booleans; Zoi for zoi (zero, one, or infinity) numbers; Option for option types; Prod for sigma and product types; Sum for sum types; Nat for natural numbers; Natp for positive natural numbers; List for singly linked lists; Seq for infinite sequences; Str for characters and strings; Ratp for positive rational numbers.
• Misc ― Sety for syntactic sets.

Syng/

In Syng/ is the heart of Syng, which consists of the following parts.

• Lang/ ― The target language of Syng.
  • Expr for addresses, types and expressions; Ktxred for evaluation contexts and redexes; Reduce for reduction of expressions.
  • Example for examples.
• Logic/ ― The syntax of the separation logic Syng.
  • Prop for propositions; Judg for judgments.
  • Core for core proof rules; Names for the name set token; Fupd for the fancy update; Hor for the Hoare triple; Heap for the heap; Ind for the indirection modality and the precursors; Inv for the propositional invariant; Lft for the lifetime; Bor for the borrow; Ub for the upper bound.
  • Paradox for paradoxes on plausible proof rules.
  • Example for examples.
• Model/ ― The semantic model and soundness proof of Syng.
  • ERA/ ― Environmental resource algebras (ERAs), for modeling the ghost state of Syng.
    • Base for the basics of the ERA; All for the dependent-map ERA; Bnd for the bounded-map ERA; Fin for the finite-map ERA.
    • Basic ERAs ― Zoi for the zoi ERA; Exc for the exclusive ERA; Ag for the agreement ERA; FracAg for the fractional agreement ERA.
    • Tailored ERAs ― Heap for the heap ERA; Names for the name set ERA; Ind for the indirection ERAs; Inv for the invariant ERA; Lft for the lifetime ERA; Bor for the borrow ERA; Ub for the upper bound ERA.
    • Global ERA ― Glob for the global ERA.
  • Prop/ ― The semantic model of the propositions and the semantic soundness of the pure sequent.
    • Base for the core semantic logic connectives; Smry for the map summary; Names for the name set token; Heap for the heap-related tokens; Lft for the lifetime-related tokens; Ub for the upper bound-related tokens.
    • Basic for basic propositions; Ind for the indirection modality and precursors; Inv for the invariant-related tokens; Bor for the borrow-related tokens.
    • Interp for the semantics of all the propositions; Sound for the semantic soundness and adequacy of the logic's pure sequent.
  • Fupd/ ― The semantic model and soundness proof of the fancy update.
    • Base for the general fancy update; Ind for the fancy update on the indirection modality and precursors; Inv for the fancy update on the propositional invariant; Bor for the fancy update on the borrow.
    • Interp for interpreting the fancy update; Sound for the semantic soundness and adequacy