GFQL: Alloy model for F/B/F + WHERE

[lmeyerov]

Why

Provide bounded, mechanized checks (Alloy) for linear GFQL patterns under set semantics so the forward/backward/forward lowering with WHERE remains semantically sound.

Deliverables

• Alloy model covering: graph, linear pattern steps, named bindings, path-semantics spec (set semantics: nodes/edges on some satisfying path, not explicit path results)
• Predicates for algorithmic forward reachability, backward pruning, final collect
• Lowerings:
  • Monotone WHERE via extremum summaries (equivalent to set-theoretic min/max over prefix paths)
  • Equality via exact sets (bitsets modeled as sets; hashing excluded)
• Assertions: Spec == Algo (no WHERE) and Spec_WHERE == Algo_Lowering (inequality + equality-as-sets)
• Scopes: ≤8 nodes, ≤4 steps, ≤4 values

Notes

• Skip NaN/null in Alloy; SQL-style null semantics live in Python/cuDF tests
• Treat any hashing as sound prefilters; final verification must re-check exactness
• Base theory: Yannakakis two-pass semijoin for acyclic CQs

Acceptance

• No counterexamples under stated scopes
• Alloy check wired into CI