Adopt Grackle in gokv tutorial

.envrc

@@ -0,0 +1 @@
+use flake

.gitattributes

@@ -0,0 +1 @@
+external/Goose/** linguist-generated

.github/workflows/ci.yml

@@ -112,6 +112,32 @@ jobs:
       - name: check that Goosed files are clean
         run: etc/ci-goose-check.py
 
+  check-grackle:
+    strategy: 
+      fail-fast: false 
+    runs-on: ubuntu-latest 
+    steps:
+      - name: Checkout 
+        uses: actions/checkout@v4
+        with:
+          submodules: true 
+      - name: Install protoc
+        run: sudo apt-get install protobuf-compiler -y
+      - name: Install Go
+        uses: actions/setup-go@v5
+        with: 
+          go-version: "1.22"
+          cache: false
+      - name: Install Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+          cache: "pip"
+      - name: Check Grackle 
+        run: |
+          ./etc/ci-grackle-check.py
+          git diff --exit-code
+
   python:
     runs-on: ubuntu-latest
     steps:

.gitignore

@@ -35,3 +35,6 @@ __pycache__
 
 # Compiled code supplement
 /peony-code.zip
+
+# direnv 
+.direnv

etc/ci-grackle-check.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+
+import shutil
+import subprocess as sp
+from dataclasses import dataclass
+
+
+@dataclass
+class Proj:
+    name: str
+    repo: str
+    commit: str
+
+    def path(self) -> str:
+        return f"/tmp/{self.name}"
+
+
+projs = {
+    "gokv": Proj("gokv", "https://github.com/mit-pdos/gokv", "main"),
+}
+
+
+def checkout(proj: Proj):
+    print(f"Checking out {proj.name}")
+    path = proj.path()
+    shared_args = {"check": True, "cwd": path}
+
+    try:
+        p = sp.run(
+            ["git", "remote", "get-url", "origin"],
+            text=True,
+            capture_output=True,
+            **shared_args,
+        )
+        assert p.stdout.strip() == proj.repo
+        sp.run(["git", "reset", "--hard"], **shared_args)
+        sp.run(["git", "pull"], **shared_args)
+    except (FileNotFoundError, sp.CalledProcessError, AssertionError):
+        shutil.rmtree(path, ignore_errors=True)
+        sp.run(["git", "clone", proj.repo, path], check=True)
+
+    sp.run(["git", "checkout", proj.commit], **shared_args)
+
+
+for proj in projs.values():
+    checkout(proj)
+
+print("\nRunning Grackle")
+sp.run(
+    [
+        "etc/update-grackle.sh",
+        "--gokv",
+        projs["gokv"].path(),
+    ],
+    check=True,
+)

etc/update-goose.py

@@ -1,8 +1,8 @@
 #!/usr/bin/env python3
 
 import os
-from os import path
 import subprocess
+from os import path
 
 
 def run_command(args, dry_run=False, verbose=False):
@@ -281,10 +281,18 @@ def run_goose(src_path, *pkgs):
             "./vrsm/apps/closed",
             "./tutorial",  # atomic commit
             "./tutorial/objectstore/dir",
+            "./tutorial/objectstore/dir/chunkhandle_gk",
+            "./tutorial/objectstore/dir/finishwrite_gk",
+            "./tutorial/objectstore/dir/recordchunk_gk",
             "./tutorial/objectstore/chunk",
+            "./tutorial/objectstore/chunk/writechunk_gk",
             "./tutorial/objectstore/client",
             "./tutorial/lockservice",
+            "./tutorial/lockservice/lockrequest_gk",
             "./tutorial/kvservice",
+            "./tutorial/kvservice/conditionalput_gk",
+            "./tutorial/kvservice/get_gk",
+            "./tutorial/kvservice/put_gk",
             "./tutorial/basics",
             "./tutorial/queue",
             "./map_marshal",

etc/update-grackle.sh

@@ -0,0 +1,95 @@
+#!/usr/bin/env bash
+
+if [[ -z "$IN_NIX_SHELL" ]]; then 
+    # Not in nix shell, use the default go installs
+    GRACKLE="go run github.com/mjschwenne/grackle/cmd/grackle@latest"
+else 
+    # In a nix shell, expect grackle to be on the PATH and use that
+    GRACKLE="grackle"
+fi
+
+compile_grackle() {
+    CWD=$(pwd)
+    cd "$1" || return
+    go install ./cmd/grackle
+    cd "$CWD" || exit
+}
+
+# Computes the coq logical name by
+#
+# - Replacing "." with "-"
+# - Replacing "-" with "_"
+# - Replacing "/" with "."
+#
+# This mirrors grackle/internal/util/util.go :: CleanCoqName function
+coq_logical_name() {
+    echo "$1" | sed -E -e "s/\./-/g" -e "s/-/_/g" -e "s/\//\./g"
+}
+
+# Run grackle on the input go package.
+#
+# We will assume that:
+# 1. The proto file is in the directory $2/$1
+# 2. We only want to output coq code
+# 3. The coq code should be output into "src/program_proof/$1"
+# 4. The desired coq package matches the directory structure
+#
+# Parameters
+# - $1 : Name of the go package inside its repo
+# - $2 : Path to the root of the go repo. Go package to translate should be at "$2/$1"
+# - $3 : Prefix to compute the go package name, "$3/$1"
+run_grackle() {
+    $GRACKLE --coq-logical-path "Perennial.program_proof.$(coq_logical_name $1)" --coq-physical-path "src/program_proof/$1" --go-package "$3/$1" "$(realpath "$2/$1")"
+}
+
+# Generate Coq files from gokv repo.
+#
+# Parameters
+# - $1 : Path to the gokv repo.
+grackle_gokv() {
+    gokv_packages=(
+        "tutorial/kvservice"
+        "tutorial/lockservice"
+        "tutorial/objectstore/chunk"
+        "tutorial/objectstore/dir"
+    )
+
+    for gopkg in "${gokv_packages[@]}"; do
+        run_grackle "$gopkg" "$1" "github.com/mit-pdos/gokv"
+    done
+}
+
+ARGS=$(getopt -o "c:g:h" --long "compile-grackle:,gokv:,help" -- "$@")
+
+eval set -- "$ARGS"
+while [ $# -ge 1 ]; do
+    case "$1" in
+    -c | --compile-grackle)
+        compile_grackle "$2"
+        shift
+        ;;
+    -g | --gokv)
+        grackle_gokv "$2"
+        shift
+        ;;
+    -h | --help)
+        cat <<EOF
+usage: update-grackle.sh [--compile-grackle <grackle repo> | -c <grackle repo>]
+                         [--gokv | -g] [--help | -h]
+
+Calls grackle on all gokv go modules known to have proto files for grackle usage, generating coq proofs.
+
+--compile-grackle [-c] : Takes the path to the grackle repository, recompiles and installs grackle
+
+--gokv [-g] : Regenerate Coq proofs for the gokv project, takes path to gokv as argument
+EOF
+        shift
+        exit 0
+        ;;
+    --)
+        shift
+        break
+        ;;
+    esac
+    shift
+done