ci(alloy): add model checks and caching (stacked)

.github/workflows/ci.yml

@@ -24,6 +24,7 @@ jobs:
       python: ${{ steps.filter.outputs.python }}
       docs: ${{ steps.filter.outputs.docs }}
       infra: ${{ steps.filter.outputs.infra }}
+      alloy: ${{ steps.filter.outputs.alloy }}
     steps:
     - uses: actions/checkout@v3
     - uses: dorny/paths-filter@v3
@@ -58,6 +59,9 @@ jobs:
             - 'demos/**'
             - 'notebooks/**'
 
+          alloy:
+            - 'alloy/**'
+
   python-lint-types:
     needs: changes
     # Run if Python files changed OR infrastructure changed OR manual/scheduled run
@@ -99,6 +103,42 @@ jobs:
         source pygraphistry/bin/activate
         ./bin/typecheck.sh
 
+  alloy-check:
+    needs: changes
+    if: ${{ needs.changes.outputs.alloy == 'true' || needs.changes.outputs.python == 'true' || needs.changes.outputs.infra == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+
+    steps:
+    - name: Checkout repo
+      uses: actions/checkout@v3
+      with:
+        lfs: true
+
+    - name: Login to GitHub Container Registry
+      uses: docker/login-action@v3
+      with:
+        registry: ghcr.io
+        username: ${{ github.actor }}
+        password: ${{ secrets.GITHUB_TOKEN }}
+
+    - name: Pre-pull Alloy image cache
+      run: |
+        docker pull ghcr.io/graphistry/alloy6:6.2.0 || true
+
+    - name: Run Alloy checks (scoped on PR/push, full on schedule/dispatch)
+      env:
+        EVENT_NAME: ${{ github.event_name }}
+      run: |
+        if [[ "$EVENT_NAME" == "schedule" || "$EVENT_NAME" == "workflow_dispatch" ]]; then
+          FULL=1
+          MULTI=1
+        else
+          FULL=0
+          MULTI=0
+        fi
+        ALLOY_PUSH=1 FULL=$FULL MULTI=$MULTI bash alloy/check_fbf_where.sh
+
   test-minimal-python:
     needs: [changes, python-lint-types]
     # Run if Python files changed OR infrastructure changed OR manual/scheduled run

alloy/Dockerfile

@@ -0,0 +1,7 @@
+FROM eclipse-temurin:17-jre
+WORKDIR /work
+
+# Use published Alloy dist jar (6.2.0)
+ADD https://github.com/AlloyTools/org.alloytools.alloy/releases/download/v6.2.0/org.alloytools.alloy.dist.jar /opt/alloy/alloy.jar
+
+ENTRYPOINT ["java", "-jar", "/opt/alloy/alloy.jar"]

alloy/README.md

@@ -0,0 +1,29 @@
+# Alloy Checks for GFQL F/B/F + WHERE
+
+Purpose: bounded, mechanized equivalence checks between the GFQL path-spec and the set-based forward/backward/forward algorithm with WHERE lowerings.
+
+## Model
+- Path semantics: bindings are sequences aligned to `seqSteps`; WHERE is per binding. Mirrors Python hop/chain construction.
+- Set semantics: executor-style F/B/F over per-alias node/edge sets; WHERE lowered via per-alias summaries.
+- Scopes: ≤8 Nodes, ≤8 Edges, ≤4 Steps, ≤4 Values. Null/NaN not modeled; hashing treated as prefilter and omitted.
+- Lowerings: inequalities via min/max summaries; equality via exact sets (bitsets modeled as sets).
+
+## Commands
+- Default small checks (fast): `bash alloy/check_fbf_where.sh`
+- Full scopes (core + scenarios): `FULL=1 bash alloy/check_fbf_where.sh`
+- Add multi-chain full-scope: `FULL=1 MULTI=1 bash alloy/check_fbf_where.sh`
+
+Env vars:
+- `ALLOY_IMAGE` (default `ghcr.io/graphistry/alloy6:6.2.0`)
+- `ALLOY_FALLBACK_IMAGE` (default `local/alloy6:latest`)
+- `ALLOY_PUSH=1` to push built image to ghcr when falling back.
+
+## CI behavior
+- PR/push: small + scenario suite (faster).
+- schedule/workflow_dispatch: full scopes + optional multi-chain (heavier).
+- Job pre-pulls `ghcr.io/graphistry/alloy6:6.2.0`; falls back to local build and pushes when allowed.
+
+## Notes / exclusions
+- Null/NaN semantics excluded; verified in Python/cuDF tests.
+- Hashing omitted; treat any hashing as sound prefilter, exactness rechecked in model.
+- Model uses set semantics for outputs (nodes/edges appearing on some satisfying path).

alloy/check_fbf_where.sh

@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+ALS="/work/gfql_fbf_where.als"
+IMAGE="${ALLOY_IMAGE:-ghcr.io/graphistry/alloy6:6.2.0}"
+LOCAL_FALLBACK_IMAGE="${ALLOY_FALLBACK_IMAGE:-local/alloy6:latest}"
+FULL=${FULL:-0}
+MULTI=${MULTI:-0}
+PUSH=${ALLOY_PUSH:-0}
+
+# Resolve image: pull ghcr if possible, otherwise build local; optionally push built image to ghcr for caching
+resolve_image() {
+  local img="$IMAGE"
+  if docker image inspect "$img" >/dev/null 2>&1; then
+    IMAGE="$img"
+    return
+  fi
+
+  if docker pull "$img" >/dev/null 2>&1; then
+    IMAGE="$img"
+    return
+  fi
+
+  # Fall back to local build
+  if ! docker image inspect "$LOCAL_FALLBACK_IMAGE" >/dev/null 2>&1; then
+    docker build -t "$LOCAL_FALLBACK_IMAGE" "$HERE"
+  fi
+
+  # Optionally publish to ghcr for future pulls
+  if [ "$PUSH" = "1" ]; then
+    docker tag "$LOCAL_FALLBACK_IMAGE" "$img"
+    docker push "$img" || true
+    IMAGE="$img"
+  else
+    IMAGE="$LOCAL_FALLBACK_IMAGE"
+  fi
+}
+
+resolve_image
+
+if [ "$FULL" = "1" ]; then
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c SpecNoWhereEqAlgoNoWhere -o - "$ALS"
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c SpecWhereEqAlgoLowered -o - "$ALS"
+else
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c SpecNoWhereEqAlgoNoWhereSmall -o - "$ALS"
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c SpecWhereEqAlgoLoweredSmall -o - "$ALS"
+fi
+
+# Scenario coverage + additional scopes (fixed small scopes inside .als)
+for ASSERT in SpecNoWhereEqAlgoNoWhereMultiChain SpecWhereEqAlgoLoweredMultiChain SpecWhereEqAlgoLoweredFan SpecWhereEqAlgoLoweredCycle SpecWhereEqAlgoLoweredParallel SpecWhereEqAlgoLoweredDisconnected SpecWhereEqAlgoLoweredAliasWhere SpecWhereEqAlgoLoweredMixedWhere SpecWhereEqAlgoLoweredFilterMix; do
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c "$ASSERT" -o - "$ALS"
+done
+
+if [ "$MULTI" = "1" ]; then
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c SpecNoWhereEqAlgoNoWhereMultiChainFull -o - "$ALS"
+  docker run --rm -v "$HERE":/work "$IMAGE" exec -c SpecWhereEqAlgoLoweredMultiChainFull -o - "$ALS"
+fi