Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: verse-lab/coq-lgtm
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: pldi24
Choose a base ref
...
head repository: verse-lab/coq-lgtm
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
  • 3 commits
  • 18 files changed
  • 2 contributors

Commits on Mar 25, 2024

  1. fix vcfloat version

    volodeyka committed Mar 25, 2024
    Copy the full SHA
    e5f4d85 View commit details
  2. fix coq-interval version

    zqy1018 authored Mar 25, 2024
    Copy the full SHA
    479cc89 View commit details

Commits on Apr 9, 2024

  1. split LibWP, update README

    volodeyka committed Apr 9, 2024
    Copy the full SHA
    fa7e775 View commit details
Showing with 3,949 additions and 2,879 deletions.
  1. +1 −1 Makefile
  2. +20 −3 README.md
  3. +1 −1 experiments/COO.v
  4. +1 −1 experiments/CSR.v
  5. +1 −1 experiments/CSR_float.v
  6. +1 −1 experiments/Prelude.v
  7. +1 −1 experiments/RL.v
  8. +1 −1 experiments/SV.v
  9. +1 −1 experiments/UnaryCommon.v
  10. +1 −1 experiments/uCSR.v
  11. +1 −1 lib/seplog/LibArray.v
  12. +315 −0 lib/seplog/LibHypHeap.v
  13. +1 −1 lib/seplog/LibLoops.v
  14. +1 −1 lib/seplog/LibLoops_float.v
  15. +5 −2,862 lib/seplog/LibWP.v
  16. +3,595 −0 lib/seplog/LibXWP.v
  17. +1 −1 lib/seplog/NTriple.v
  18. +1 −1 lib/seplog/Subst.v
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -4,7 +4,7 @@ TLC_FILES := LibAxioms.v LibTactics.v LibEqual.v LibLogic.v LibOperation.v LibBo

THEORY_FILES := LibSummation.v LibListExt.v LibDotprod_float.v LibFunExt.v LibLabType.v

SEPLOG_FILES := LibSepFmap.v LibSepVar.v LibSepSimpl.v LibWP.v LibSepReference.v LibArray.v LibLoops.v NTriple.v Subst.v LibLoops_float.v
SEPLOG_FILES := LibSepFmap.v LibSepVar.v LibSepSimpl.v LibHypHeap.v LibWP.v LibXWP.v LibSepReference.v LibArray.v LibLoops.v NTriple.v Subst.v LibLoops_float.v

EXPERIMENTS_FILES := COO.v RL.v SV.v CSR.v UnaryCommon.v uCSR.v CSR_float.v Prelude.v

23 changes: 20 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -11,7 +11,8 @@ opam install coq-mathcomp-ssreflect=2.1.0
opam install coq-mathcomp-zify coq-mathcomp-algebra=2.1.0 coq-mathcomp-fingroup=2.1.0 coq-mathcomp-finmap=2.1.0
opam install coq-flocq
opam install coq-bignums=9.0.0+coq8.18
opam install coq-vcfloat --ignore-constraints-on=coq
opam install coq-interval=4.9.0
opam install coq-vcfloat=2.1.1 --ignore-constraints-on=coq
```

The flag `--ignore-constraints-on` is necessary for working around some version constraints.
@@ -28,6 +29,22 @@ Please note that warnings (in yellow colour) may appear during the compilation,

## Navigation Guide

This project consists of two major folders: `lib/` with LGTM metatheory formalisation and `experiments/` with LGTM case study evaluation. First we present a brief description of `lib/` folder contents:

- `theory/`: various extensions of Coq Standard Library
- `seplog/`: LGTM metatheoty mechanisation
- `LibSepFmap`: mechanisation of finite mappings
- `LibSepVar`: auxilary file to deal with variables
- `LibSepSimpl`: tactic for heap asserions simplification and automation
- `LibHypHeap`: lemmas about hyper heap assertions
- `LibWP`: lemmas about weakest precondition calculus
- `LibXWP`: setting up a Coq framework (automation and notations) to reason about LGTM hyper-triples in weakest precondition style
- `LibArrays`: lemmas to reason about arrays in LGTM
- `LibLoops`: lemmas to reason about `for`/`while` loops in LGTM
- `LibLoops_float`: lemmas to reason about `for`/`while` loops operating with floats in LGTM
- `NTriple`: lemmas for structural LGTM hyper-triples transformations
- `Subst`: machanisation and a tactic for `Subst` rule from the paper

### Important Proof Rules

Structural rules:
@@ -54,10 +71,10 @@ Domain substitution rule:
- Subst: `htriple_hsub` in `lib/seplog/LibWP.v`

Rule for for-loops:
- For: `wp_for` in `lib/seplog/LibWP.v`
- For: `wp_for` in `lib/seplog/LibXWP.v`

Rule for while-loops:
- While: `wp_while` in `lib/seplog/LibWP.v`
- While: `wp_while` in `lib/seplog/LibXWP.v`

### Important Results

2 changes: 1 addition & 1 deletion experiments/COO.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibSummation LibListExt LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops NTriple.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops NTriple.
From LGTM.experiments Require Import Prelude UnaryCommon.
From mathcomp Require Import ssreflect ssrfun zify.
Hint Rewrite conseq_cons' : rew_listx.
2 changes: 1 addition & 1 deletion experiments/CSR.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibSummation LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops Subst NTriple.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops Subst NTriple.
From LGTM.lib.theory Require Import LibListExt.
From LGTM.experiments Require Import Prelude UnaryCommon SV.
From mathcomp Require Import ssreflect ssrfun zify.
2 changes: 1 addition & 1 deletion experiments/CSR_float.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibSummation LibDotprod_float LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops LibLoops_float Subst NTriple.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops LibLoops_float Subst NTriple.
From LGTM.lib.theory Require Import LibListExt.
From LGTM.experiments Require Import Prelude UnaryCommon.
From mathcomp Require Import ssreflect ssrfun zify.
2 changes: 1 addition & 1 deletion experiments/Prelude.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibReflect.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray.
From mathcomp Require Import ssreflect ssrfun zify.

Ltac bool_rew :=
2 changes: 1 addition & 1 deletion experiments/RL.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibSummation LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops NTriple.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops NTriple.
From LGTM.lib.theory Require Import LibListExt.
From LGTM.experiments Require Import Prelude UnaryCommon.
From mathcomp Require Import ssreflect ssrfun zify.
2 changes: 1 addition & 1 deletion experiments/SV.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibSummation LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops NTriple.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops NTriple.
From LGTM.lib.theory Require Import LibListExt.
From LGTM.experiments Require Import Prelude UnaryCommon.
From mathcomp Require Import ssreflect ssrfun zify.
2 changes: 1 addition & 1 deletion experiments/UnaryCommon.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibListExt LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops.
From LGTM.experiments Require Import Prelude.
From mathcomp Require Import ssreflect ssrfun zify.
Hint Rewrite conseq_cons' : rew_listx.
2 changes: 1 addition & 1 deletion experiments/uCSR.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Implicit Arguments.
From LGTM.lib.theory Require Import LibFunExt LibLabType LibSummation LibSepTLCbuffer.
From LGTM.lib.seplog Require Import LibSepReference LibWP LibSepSimpl LibArray LibLoops Subst NTriple.
From LGTM.lib.seplog Require Import LibSepReference LibHypHeap LibWP LibXWP LibSepSimpl LibArray LibLoops Subst NTriple.
From LGTM.lib.theory Require Import LibListExt.
From LGTM.experiments Require Import Prelude UnaryCommon SV.
From mathcomp Require Import ssreflect ssrfun zify.
2 changes: 1 addition & 1 deletion lib/seplog/LibArray.v
Original file line number Diff line number Diff line change
@@ -2,7 +2,7 @@

Set Implicit Arguments.
From LGTM.lib.theory Require Import LibSepTLCbuffer LibFunExt LibLabType.
From LGTM.lib.seplog Require Import LibSepSimpl LibSepReference LibWP.
From LGTM.lib.seplog Require Import LibSepSimpl LibSepReference LibHypHeap LibWP.
From LGTM.lib.theory Require LibListExt.
From mathcomp Require Import ssreflect ssrfun zify.
Hint Rewrite conseq_cons' : rew_listx.
Loading