TLAi linter: Check consistency of natural language comments and TLA+ formulas.

[Build]

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

.github/scripts/TLAi-linter.genai.js

@@ -0,0 +1,25 @@
+// learn more at https://aka.ms/genaiscript
+script({ title: "TLAi-linter", description: "Check if the prose comments and their TLA+ declarations and definitions are syntactically and semantically consistent" })
+
+// use def to emit LLM variables
+def("TLA+", env.files.filter(f => f.filename.endsWith(".tla")), {lineNumbers: true})
+
+// use $ to output formatted text to the prompt
+$`You are an expert at TLA+/TLAPLUS. Your task is to check if the prose comments and their TLA+ declarations and definitions are syntactically and semantically consistent!!!
+Explain any consistencies and inconsistencies you may find.  Report inconsistent and consistent pairs in a single ANNOTATION section.
+
+## TLA+ Syntax Hints
+- A formula [A]_v is called a temporal formula, and is shorthand for the formula A \/ v' = v.  In other words, the formula is true if A is true or if the value of v remains unchanged.  Usually, v is a tuple of the spec's variables.
+- The symbol \`#\` is alternative syntax used for inequality in TLA+; the other symbol is \`/=\".
+
+## TLA+ Semantics Hints
+- Do NOT add any invariants or properties to the behavior specification Spec or any of its subformulas.  This would change THEOREM Spec => Inv into THEOREM Spec /\ Inv => Inv, which is vacuously true.
+- TLA+ specs are always stuttering insensitive, i.e., the next-state relation is always [A]_v.  In other words, one cannot write a stuttering sensitive specification.
+
+## TLA+ Convention Hints
+- The type correctness invariant is typically called TypeOK.
+- Users can employ TLA labels as a means to conceptually associate a comment with a sub-formula like a specific disjunct or conjunct of a TLA formula. Even though these labels have no other function, they facilitate referencing particular parts of the formula from a comment.
+
+## Formal and informal math Hints
+- Take into account that humans may write informal math that is syntactically different from the formal math, yet semantically equivalent.  For example, humans may write \`N > 3T\` instead of \`N > 3 * T\`.
+`

.github/workflows/PR.yml

@@ -0,0 +1,46 @@
+name: TLAi linter
+
+on: [pull_request]
+
+jobs:
+  linting:
+    name: TLAi linter
+
+    runs-on: ubuntu-latest
+
+    env:
+      ## https://microsoft.github.io/genaiscript/reference/token/
+      OPENAI_API_KEY: ${{ secrets.OPENAI_API_KEY }}
+      OPENAI_API_BASE: ${{ secrets.OPENAI_API_BASE }}
+      OPENAI_API_TYPE: ${{ secrets.OPENAI_API_TYPE }}
+
+    defaults:
+      run:
+        shell: bash
+
+    steps:
+      - name: Clone repo
+        uses: actions/checkout@v4
+        with:
+            ## All history for git diff below to succeed.
+            fetch-depth: 0
+
+      - name: Setup NodeJS
+        ## https://github.com/actions/setup-node
+        uses: actions/setup-node@v4
+        with:
+            node-version: "20"
+
+      - name: Run GenAIscript on the TLA+ specs that are added in this pull request.
+        ## Identify git diff: $(git diff --name-only HEAD^ | grep '.tla')
+        ## Install genaiscript runtime: https://microsoft.github.io/genaiscript/reference/cli/
+        ## Output LLM response in SARIF format: https://microsoft.github.io/genaiscript/reference/scripts/annotations/ (redirect other output to /dev/null for GH not to also show the annotations)
+        run: npx --yes genaiscript-cli run .github/scripts/TLAi-Linter.genai.js $(git diff --name-only HEAD^ | grep '.tla') --max-tokens 2000 --out-annotations results.sarif > /dev/null
+
+      - name: Upload SARIF file
+        ## https://sarifweb.azurewebsites.net
+        ## https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/uploading-a-sarif-file-to-github
+        if: success() || failure()
+        uses: github/codeql-action/upload-sarif@v3
+        with:
+            sarif_file: results.sarif