Infinitary Relational Logic

The paper introduces infinitary relational logic (IRL) and demonstrates its advantages through examples and case studies. This artifact accompanies the paper with a mechanized proof development in Lean 4. It formalizes IRL's metatheory and provides machine-checked soundness proofs, together with proofs of all the examples and case studies presented in the paper.

This is a mechanized proof artifact. Claims are reproduced by proof checking: a successful lake build confirms that every claimed lemma and example has a complete proof. StatsTab1.lean and StatsTab2.lean provide scripts to reproduce numbers of Table 1 and Table 2 in the paper.

• Lean 4 v4.20.0 (pinned in lean-toolchain)
• Internet access on first build (Lake fetches Mathlib and other dependencies)

Supported platforms are those of elan / Lean 4 (Linux, macOS, and Windows, where WSL is recommended).

1. Install Lean via the official installer: https://lean-lang.org/install/
2. (Skip during artifact evaluation) Clone this repository with submodules:

git clone --recurse-submodules https://github.com/verse-lab/lean-lgtm.git
cd lean-lgtm
git submodule update --init --recursive

The WeirdLogic submodule must be present; it supplies the WM development and several IRL lemmas referenced below.

Do not modify lakefile.lean or lean-toolchain.

3. (For artifact evaluation) Download the code from the Zenodo link:

cd lean-lgtm

Run the following command:

lake build

This will take a while (~20 minutes on a MacBook Pro with an M3 Pro chip and 32 GB of RAM).

This builds Lgtm (IRL and the case studies in Secs. 2 and 3) and WeirdLogic (the WM rules and the WMR case study in Sec. 5).

Expected: Build completed successfully with no errors.

A successful lake build without "sorry" in warning messages already establishes the reproducibility of the IRL metatheory and of every lemma, rule, example, and case study claimed in the paper.

Detailed guidelines from the paper to the artifact are shown below:

The semantics of the IRL language can be found in Lgtm/Unary/Lang.lean and Lgtm/Unary/SepLog.lean. The AllocExec rule in Section 4.1 of the paper corresponds to alloc_exec in Lgtm/Unary/SepLog.lean.

The definition of the IRL triple is htriple in Lgtm/Hyper/SepLog.lean. Another variant is triple in Lgtm/Hyper/WP.lean. Each IRL rule is phrased as a Lean Prop about triples and is sound once it is proved.

The case studies presented in Table 1 of Section 2.4 are in Lgtm/Experiments/, organized as shown below.

The example introduced in Secs. 2.1 to 2.3 is the second one in the table, $\iint_{\mathbb{R}} Grid(x,y)\ dx\ dy $.

StatsTab1.lean produces numbers for Table 1 (Section 2.4) in the paper. Run it from the repository root:

lake build  # required if any modifications to the code
lake env lean StatsTab1.lean

Note: do not modify any code when running this command, since edits to the sources may change the LOC values.

Output: 1) the numbers for Table 1; 2) the original numbers from the paper; and 3) a breakdown per program and per lemma.

Expected output table:

| #  | Operation                 | Spec | C_O | C_A | Pf  | Pf/C_O | Pf/C_A |
|----|---------------------------|------|-----|-----|-----|--------|--------|
| 1  | ∫ Grid(x) dx              | 11   | 9   | 14  | 43  | 4.8    | 3.1    |
| 2  | ∬ Grid(x,y) dx dy         | 11   | 11  | 24  | 64  | 5.8    | 2.7    |
| 3  | ∫₀¹ Grid(p+x) dx          | 12   | 22  | 34  | 102 | 4.6    | 3.0    |
| 4  | ∬₀¹ Grid(p+x,q+y) dx dy   | 13   | 27  | 42  | 128 | 4.7    | 3.0    |
| 5  | |Ps(i,x) ∩ Interval(x)|   | 11   | 16  | 22  | 89  | 5.6    | 4.0    |
| 6  | |Ps(i,x,y) ∩ Box(x,y)|    | 12   | 20  | 35  | 117 | 5.9    | 3.3    |
| 7  | |Ps(i,x,y) ∩ Circle(x,y)| | 10   | 46  | 66  | 250 | 5.4    | 3.8    |

Each column is obtained as follows:

A lemma's region is the declaration plus the set_option ... in, attribute, omit ... in and @[yapp] lines attached directly above it.

C_A is not counted from the source, since the ANF transformation happens during elaboration. StatsTab1.lean pretty-prints the term Lean stores, which is what the proofs run against.

For example, for a single program in Lgtm/Experiments/Comparison/Code.lean:

lang_def' Lang.linearInterp :=
  fun ⸨xleft:Loc⸩ ⸨xright:Loc⸩ ⸨xval:Loc⸩ ⸨z:Val⸩ ⸨n:Val⸩ =>
    ref ans := ⟨0 : ℝ⟩ in
    for i in [z:n] {
      ans += xval[i] * (xright[i] - xleft[i])
    }; !ans

#print Lang.linearInterp

-- shown in Lean InfoView
def Lang.linearInterp : trm :=
[lang|
  fun xleft xright xval z n =>
    ref ans := 0 in
    for i in [z : n] {
        let temp0 := xval[i] in
        let temp1 := xright[i] in
        let temp2 := xleft[i] in
        let temp3 := temp1 - temp2 in
        let temp4 := temp0 * temp3 in
        ans += temp4 };
    !ans]

#print shows the five let-bindings that ANF introduces for ans += xval[i] * (xright[i] - xleft[i]), giving C_A = 10 against C_O = 5.

StatsTab2.lean produces numbers for Table 2 (Section 3.4) in the paper. Run it from the repository root:

lake build            # required if any modifications to the code
lake env lean StatsTab2.lean

Output: 1) the numbers for Table 1; 2) the original numbers from the paper; and 3) a breakdown per category and per lemma.

The three proof styles are measured over disjoint files, all under Lgtm/Experiments/Comparison/:

Each category is a group of lemmas within those files:

Expected Output:

| Category  | Unary | UvR | Relational |
|-----------|-------|-----|------------|
| Layer     | 0     | 0   | 110        |
| Format    | 180   | 120 | 26         |
| Operation | 200   | 0   | 0          |
| Other     | 120   | 45  | 164        |
| Total     | 500   | 165 + 300 | 300       |

Lgtm/Experiments/ and WeirdLogic/Examples/ show how to write programs, state Hoare-style specifications, and prove them in IRL. A typical workflow:

1. Define programs with lang_def / lang_def' (see Lgtm/Experiments/Comparison/Code.lean). The syntax is Imp-like; binders use ⸨x:Loc⸩ / ⸨x:Val⸩.
2. State a specification as an IRL triple.

WP form:

WP [ℓ | i in s => prog(...)] { v, Q }

Triple form:

{ H }
[ℓ₁ | i in s₁ => prog₁(...)]
[ℓ₂ | i in s₂ => prog₂(...)]
{ v, Q }

Here H / Q are hyper-heaps (separating conjunction ∗, pure facts ⌜_⌝, arrays arr⟨s⟩(...)). The underlying proposition is htriple / hwp from Lgtm/Hyper/SepLog.lean and Lgtm/Hyper/WP.lean.

3. Prove the triple in the IRL proof mode (import Lgtm.Hyper.ProofMode). Common tactics:

   Tactic	Role
   ywp / ytriple	enter weakest-precondition / triple mode
   yapp / ystep	apply a registered spec or take one step
   yfocus / yunfocus	restrict or restore a component's index set (Focus)
   ylet / yseq / yif / yref	structural rules for let, sequencing, if, ref
   yfor / ywhile	loop rules (For, While)
   ysimp / ypull	simplify / pull pure facts from the precondition
   yin ℓ: ...	apply tactics under a selected label

   Register reusable specs with @[yapp] or #hint_yapp so yapp can apply them automatically.

4. Start from an existing case study. For a concrete end-to-end proof, see linearInterp_spec in Lgtm/Experiments/Comparison/Hyper/BilinInterp.lean. For WM-style reasoning, see WeirdLogic/Examples/VulnWM.lean.