Infinitary Relational Logic

1. Overview

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.

2. Getting Started

Requirements

• 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).

Download and installation

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

3. Evaluation Instructions / Functionality

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.

4. Paper-to-Artifact / Reproducibility Guidelines

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:

IRL Rules

Name	Paper	Location	Lemma
SeqU1	Page 7, Figure 3	WeirdLogic/LgtmMisc.lean	LGTM.triple_sequ1
SeqU2	Page 7, Figure 3	WeirdLogic/LgtmMisc.lean	LGTM.triple_sequ2
Focus	Page 7, Figure 3	Lgtm/Hyper/ProofMode.lean	yfocus_set_lemma
For	Page 9, Figure 5	Lgtm/Hyper/Loops/YLemmas.lean	yfor_lemma
InfInfProd	Page 8, Figure 4	WeirdLogic/InfInfProd.lean	htriple_htriple_partition
InfProd	Page 8, Figure 4	Lgtm/Hyper/SepLog.lean	htriple_prod
LetU	Page 10, Figure 6	Lgtm/Hyper/ProofMode.lean	ylet_lemma
Merge	Page 10, Figure 6	Lgtm/Hyper/Merge.lean	ymerge_lemma
While	Page 17, Figure 8	Lgtm/Hyper/Loops/YLemmas.lean	ywhile_lemma
Expand	Converse of Merge rule	WeirdLogic/LgtmMisc.lean	hsubst_htriple_gen

WM Rules

Name	Paper	Location	Lemma
Weaken	Page 20, Figure 10	WeirdLogic/WLogic.lean	weird_weaken_lemma
GrmDisj	Page 20, Figure 10	WeirdLogic/GramDisjStandard.lean	weird_grmdisj_lemma_standard
Payload	Page 20, Figure 10	WeirdLogic/WLogic.lean	weird_payload_index_lemmaweird_payload_index_lemma2
GrmSeq	Page 20, Figure 10	WeirdLogic/GramSeq.lean	weird_gram_seq_full_prod

Semantic Rules

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.

Soundness Statements

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.

5. Case Studies

Geometric Case Studies in Section 2

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

#	Name	Location	Lemma
1	$\int_{\mathbb{R}} Grid(x)\ dx $	Lgtm/Experiments/Comparison/Hyper/BilinInterp.lean	linearInterp_spec
2	$\iint_{\mathbb{R}} Grid(x,y)\ dx\ dy $	Lgtm/Experiments/Comparison/Hyper/BilinInterp.lean	bilinearInterp_spec_entire
3	$\int_{0}^{1} Grid(p+x)\ dx $	Lgtm/Experiments/BilinearInterp.lean	linearInterp'_spec
4	$\iint_{0}^{1} Grid(p+x,q+y)\ dx\ dy$	Lgtm/Experiments/BilinearInterp.lean	bilinearInterp_spec
5	$\mid \mathit{Ps(i,x)} \cap \mathit{Interval(x)}\mid$	Lgtm/Experiments/BoxCount.lean	intervalCountQuery'_spec
6	$\mid \mathit{Ps(i,x,y)} \cap \mathit{Box(x,y)}\mid$	Lgtm/Experiments/BoxCount.lean	boxCountQuery'_spec
7	$\mid \mathit{Ps(i,x,y)} \cap \mathit{Circle(x,y)}\mid$	Lgtm/Experiments/CircleCount.lean	circleCountQuery'_spec

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 $.

Case Studies in Section 3

#	Name	Location	Lemma
1	Unary	Lgtm/Experiments/Comparison/Unary/BilinInterp.lean	unary_biunary_linearInterp_spec
2	UvR	Lgtm/Experiments/Comparison/HyperToUnary.lean	bilinearInterp_spec
3	Relational	Lgtm/Experiments/Comparison/Hyper/BilinInterp.lean	bilinearInterp_spec_entire

Case Studies in Section 5

Name	Paper	Location	Lemma
Overall Example	triple (25)	WeirdLogic/Examples/VulnWM.lean	vulnwm_spec
Part 1	triple (29)	WeirdLogic/Examples/ForWM.lean	forwm_spec
Part 2	triple (30)	WeirdLogic/Examples/IfWM.lean	ifwm_spec

6. Reproducibility of Tables

6.1. Table 1

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:

Column	How it is measured
Spec	lines of the specification lemma, up to and including its := by, ignoring blank and commented-out lines
C_O	lines of the program's lang_def/lang_def' block, as written in the source
C_A	lines of the same program after ANF transformation, read back from the elaborated term
Pf	non-blank lines of the whole region a lemma occupies, together with the regions of the auxiliary lemmas the case study establishes
Pf/C_O	ratio of Pf to C_O
Pf/C_A	ratio of Pf to C_A

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 InfoViewdefLang.linearInterp : trm :=
[lang|
fun xleft xright xval z n =>
ref ans := 0in
for i in [z : n] {
let temp0 := xval[i] inlet temp1 := xright[i] inlet temp2 := xleft[i] inlet temp3 := temp1 - temp2 inlet 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.

6.2. Table 2

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/:

Style	Files
Unary	Unary/PureTheory.lean, Unary/BilinInterp.lean
UvR	GetterSpec.lean and HyperToUnary.lean, on top of the relational proof
Relational	Hyper/SearchSRLE.lean, Hyper/BilinInterp.lean

Each category is a group of lemmas within those files:

Category	What it counts
Layer	the payload-agnostic search and its relational lifting, searchSparseRLE_spec through searchSRLE_hspec
Format	the lemmas about the sparse RLE grid that any operation on it reuses
Operation	the unary lemmas deriving the (double) integral from the representation invariant
Other	the proof of bilinInterp itself: the theorem the style states together with every lemma that proof uses, minus what the three rows above already count

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 |

7. Using IRL / Reusability

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.