Test ci

.github/copilot-instructions.md

@@ -0,0 +1,43 @@
+# Copilot Instructions for the Diff Repository
+
+Before starting a task, check if you have ghc 9.14.1 available in the PATH.
+If no, install it.
+
+## Build & Test Commands
+
+```bash
+# Build the library (no LiquidHaskell)
+
+cabal build
+
+# Build the library with LiquidHaskell to run the static checks
+# (requires ghc 9.14.1)
+cd Diff-liquidhaskell && cabal build
+
+# Run the QuickCheck test suite
+cabal test
+
+# Run benchmarks
+cabal bench
+```
+
+## Repository Architecture
+
+### Two-package structure
+
+| Package | Cabal file | Purpose |
+|---------|-----------|---------|
+| `Diff` | `Diff.cabal` | The library itself — no LH dependency. |
+| `Diff-liquidhaskell` | `Diff-liquidhaskell/Diff-liquidhaskell.cabal` | Shares `Diff`'s source tree (`src/`) to compile its modules with the LH GHC plugin enabled.|
+
+The `Diff-liquidhaskell` package exists to break the cyclic dependency
+`Diff → liquidhaskell → liquidhaskell-boot → Diff`.
+Source changes live in `src/`; the `Diff-liquidhaskell/` directory only has cabal metadata.
+
+### Source modules
+
+- `Data.Algorithm.Diff` — core Myers O(ND) diff algorithm and public API.
+- `Data.Algorithm.DiffOutput` — pretty-printing utilities for regular `diff` output.
+- `Data.Algorithm.DiffContext` — pretty-printing utilities for `diff -u` like output.
+- `Internal.LiftedFunctions` — not always present depending on current git checkout:
+   utility functions used exclusively in LH logic (lifted using `reflect` or `measure` LH directives).

.github/skills/haskell-toolchain/SKILL.md

@@ -0,0 +1,114 @@
+---
+name: haskell-toolchain
+description: >
+  Install a specific version of GHC, cabal-install, and stack using ghcup,
+  plus a recent z3 binary from GitHub. Use this skill
+  whenever the user needs to set up or reproduce a Haskell build environment
+  in a container: version-pinned toolchains, CI images, LiquidHaskell setups,
+  or any task that starts with "install GHC".
+compatibility:
+  os: Ubuntu 22.04 / 24.04 (Debian-based), x86_64
+  network: downloads.haskell.org, hackage.haskell.org, github.com must be reachable
+---
+
+# Haskell Toolchain
+
+## 1. System prerequisites
+
+```bash
+apt-get update -qq
+apt-get install -y --no-install-recommends \
+  curl ca-certificates \
+  build-essential \
+  libgmp-dev libffi-dev zlib1g-dev \
+  libnuma-dev \
+  pkg-config
+```
+
+`libnuma-dev` is required by some GHC bindists; omitting it causes a silent
+link failure.
+
+## 2. Install ghcup (non-interactive)
+
+```bash
+export BOOTSTRAP_HASKELL_NONINTERACTIVE=1
+export BOOTSTRAP_HASKELL_NO_UPGRADE=1
+# Do not install any default GHC/cabal yet — we pin versions below
+export BOOTSTRAP_HASKELL_INSTALL_NO_STACK=1
+export GHCUP_INSTALL_BASE_PREFIX=/usr/local
+
+curl -sSf https://get-ghcup.haskell.org | sh
+
+# Make ghcup and installed tools available in the current shell
+source /usr/local/.ghcup/env
+# For subsequent RUN layers in a Dockerfile, persist it:
+echo 'source /usr/local/.ghcup/env' >> /etc/profile.d/ghcup.sh
+```
+
+`BOOTSTRAP_HASKELL_NONINTERACTIVE=1` suppresses all prompts.
+`GHCUP_INSTALL_BASE_PREFIX=/usr/local` installs system-wide rather than into
+`~/.ghcup`.
+
+## 3. Install specific tool versions
+
+Replace the version strings with whatever the project requires.
+
+```bash
+# Discover available versions if needed:
+#   ghcup list --tool ghc
+#   ghcup list --tool cabal
+#   ghcup list --tool stack
+
+GHC_VERSION=9.6.6
+CABAL_VERSION=3.10.3.0
+STACK_VERSION=2.15.7
+
+ghcup install ghc   $GHC_VERSION   && ghcup set ghc   $GHC_VERSION
+ghcup install cabal $CABAL_VERSION && ghcup set cabal $CABAL_VERSION
+ghcup install stack $STACK_VERSION && ghcup set stack $STACK_VERSION
+```
+
+`ghcup set` updates the unversioned symlinks (`ghc`, `cabal`, `stack`) so
+nothing downstream needs to know the exact version.
+
+Verify:
+
+```bash
+ghc   --version   # The Glorious Glasgow Haskell Compilation System, version <GHC_VERSION>
+cabal --version   # cabal-install version <CABAL_VERSION>
+stack --version   # Version <STACK_VERSION>, ...
+```
+
+## 4. Prime the Hackage index
+
+```bash
+cabal update
+```
+
+This is a network call to `hackage.haskell.org`. Run it once before the fist
+`cabal build` invocations.
+
+## 5. Install a recent z3 binary
+
+The Ubuntu 24.04 apt package for z3 is 4.8.12 (2021). LiquidHaskell and
+other SMT-backed tools benefit from a much newer release. Install from the
+GitHub release binary instead.
+
+```bash
+Z3_VERSION=4.16.0  # update to latest tag from github.com/Z3Prover/z3/releases
+GLIBC_VERSION=2.39
+
+curl -sSfL \
+  "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-glibc-${GLIBC_VERSION}.zip" \
+  -o /tmp/z3.zip
+
+apt-get install -y --no-install-recommends unzip
+unzip -q /tmp/z3.zip -d /tmp/z3-bin
+install -m 755 /tmp/z3-bin/z3-${Z3_VERSION}-x64-glibc-2.35/bin/z3 /usr/local/bin/z3
+rm -rf /tmp/z3.zip /tmp/z3-bin
+
+z3 --version  # Z3 version 4.16.0 - 64 bit
+```
+
+The glibc-2.35 build runs on Ubuntu 22.04 and 24.04. Check the releases page
+for the exact asset filename if the version changes.

.github/skills/spec-writing/SKILL.md

@@ -0,0 +1,92 @@
+---
+name: spec-writing 
+description: Liquid Haskell specification writing guidelines. Use this when asked to write or fix a Liquid Haskell specification/annotation or statically check invariants to a package/module/source-file/function.
+---
+
+# LiquidHaskell Specification Writing Guidelines
+
+## General approach
+
+1. Make sure the build succeeds with LiquidHaskell enabled by using
+  `ignore` or `lazy` annotations in error trowing functions depending
+   on the cause of the error:
+   - `{-@ lazy f @-}` disables termination checking only.
+   - `{-@ ignore f @-}` suppresses checking a function entirely.
+   This allows to approach incrementally.
+2. Analyze the source, references and documentation comments to find function invariants in the form of pre-conditions or post-conditions.
+3. When writing a new specification for an existing function, begin by marking it `{-@ assume f :: T @-}`:
+   - `{-@ assume f :: T @-}` skips body checking, trusting the spec.
+   This lets you design the postconditions top-down — verify that callers type-check under the assumed spec before investing effort in proving the function body. Once the interface is stable, remove `assume` and prove.
+4. Proving the body of a function obeys its specification, and making callers type-check with it, might require some of the following techniques:
+   - Write new predicates in the form of lifted Haskell functions
+   - Define refinement (predicate or type) aliases to make specs more concise.
+   - Lemmas providing additional constraints in unused bindings.
+   - Refactoring of the function.
+   When attempting a refactoring, aim for changes that preserve existing semantics and improve code readability. Refactoring should always be the last resort.
+5. Keeping check disabling annotations (like `ignore`, `lazy` and `assume`) in a codebase is a valid trade-off when the proof machinery required to remove them would disproportionately clutter the source.
+6. Test your changes are correct by building the package successfully with LH enabled.
+
+## Other guidelines
+
+Before introducing a new specification, pick the one with the least code impact (i.e. the amount of new definitions plus the size and semantic effects of refactorings)
+among two different approaches to prove it.
+
+**Prefer lifted helper functions over source refactoring.** When a
+specification requires auxiliary reasoning (e.g. an intermediate invariant),
+first try to express it with a new reflected predicate rather than restructuring
+the source code.  Refactoring is preferable when it simplifies spec writing
+without altering semantics.
+
+### Choosing `inline`, `measure`, or `reflect` to lift a function into the LH logic
+
+| Annotation | What it does | When to use |
+|------------|-------------|-------------|
+| `inline` | Expands the definition as an SMT term (`ite`/arithmetic). Not visible inside `reflect`ed bodies. | Pure arithmetic or boolean helpers used in refinement types. Must be total and simple enough for SMT to reason about directly: they cannot be recursive and they can call other (non-recursive) inlined functions. |
+| `measure` | Eagerly evaluated on constructor-applied data, attached to the type's constructors. | Single-argument functions defined by pattern matching on one ADT. |
+| `reflect` | Lifts the definition into logic; PLE can unfold it at constructor-applied arguments. | The general-purpose choice for predicates and helpers used in specifications. Safe for any type, including `[SomeSpecificType]`. |
+
+**Rule of thumb:** start with `reflect`. Switch to `measure` only when you need
+eager evaluation on constructors *and* the function's domain is a standalone ADT
+(not a parameterised container with mixed element types). Switch to `inline`
+only for small arithmetic/boolean combinators that SMT should reason about
+equationally.
+
+## PLE and opaque terms
+
+PLE (Proof by Logical Evaluation) unfolds reflected functions **only** at
+syntactically constructor-applied arguments.  A variable — even one known to
+equal a constructor via a measure — is opaque to PLE.
+
+Key consequences:
+
+- **Recursive call results are opaque.** In `f (x:xs) = … f xs …`, PLE can unfold `g (x:xs)` (the input) but NOT `g (f xs)` (the recursive result). Use postconditions on `f` to carry facts about `f xs` into the SMT context.
+
+- **Opaque function parameters don't flow into SMT.** For a guard `eq x y`, where`eq` is a binary operator that evaluates to a `Bool` at runtime, LH records **no** connection between the Boolean and `eq(x,y)` in SMT. Only built-in operations like `(==)` (mapped to SMT equality) produce usable facts.
+
+- **Measures on opaque terms stay as uninterpreted SMT terms.** `isFirst x` where `x` is constructor-applied evaluates eagerly; where `x` is a variable it becomes an uninterpreted function.  Thread the needed fact via a postcondition on the function that produces `x`.
+
+- **Per-constructor function variants enable PLE.** When a function receives a value whose constructor is known only via a measure or a precondition, PLE cannot match the reflected definition's patterns.  Split the function into per-constructor variants (e.g. `grabGroupF`, `grabGroupS`, `grabGroupB`) that pattern-match on the constructor explicitly so PLE can unfold.
+
+### Proving properties through recursive structures
+
+- **Carry invariants through postconditions, not PLE unfolding.** For
+  recursive functions, state the desired property of the recursive result in
+  the postcondition rather than expecting PLE to derive it.  The SMT solver
+  can then combine the postcondition with locally unfolded facts.
+
+- **Biconditional head-constructor specs.** When a function transforms a list
+  and the proof depends on the head element's constructor, add `<=>` (not just
+  `=>`) postconditions: `headIsFirst xs <=> headIsFirst vs`.  The forward
+  direction lets you prove positive properties; the backward direction
+  (contrapositive) lets you prove negative ones.
+
+- **Intermediate invariants for multi-stage pipelines.** When a pipeline involves stages that weaken and re-establish an invariant define an explicit intermediate predicate and type the stages accordingly.
+
+### Termination
+
+- Termination metrics are declared with `/ [expr]`.  LH adds an implicit `expr >= 0` constraint at all call sites and requires strict decrease at recursive sites.
+- **Mutually recursive functions need explicit `/ [len xs]` metrics.** Without them, LH may report "decreasing parameters should be of same type" even when types match.
+
+### Common pitfalls
+
+- GHC may infer a polymorphic type for a local binding (e.g. a numeric literal `0`).  If the LH annotation specifies `Int`, add an explicit Haskell type signature to avoid "specified type does not refine Haskell type" errors.

.github/workflows/liquidhaskell.yml

@@ -0,0 +1,55 @@
+name: LiquidHaskell
+
+on:
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  liquidhaskell:
+    name: Build / Run Checks
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        cabal: ["3.16.0.0"]
+        ghc:
+          - "9.14.1"
+        z3:
+          - "4.15.1"
+    steps:
+      - uses: actions/checkout@v7
+
+      - name: Setup z3-${{ matrix.z3 }}
+        uses: pavpanchekha/setup-z3@6b2d476d7a9227e0d8d2b94f73cd9fcba91b5e98
+        with:
+          version: ${{ matrix.z3 }}
+          distribution: glibc-2.39
+
+      - name: Setup GHC and cabal-install
+        uses: haskell-actions/setup@v2
+        with:
+          ghc-version: ${{ matrix.ghc }}
+          cabal-version: ${{ matrix.cabal }}
+
+      - name: Configure cabal
+        working-directory: ./Diff-liquidhaskell
+        run: |
+          cabal update
+          # should produce a plan.json file
+          cabal build --dry-run
+
+      - uses: actions/cache@v3
+        with:
+          path: |
+            ~/.cabal/packages
+            ~/.cabal/store
+            ./Diff-liquidhaskell/dist-newstyle
+          key: ${{ runner.os }}-${{ matrix.ghc }}-cabal-${{ hashFiles('./Diff-liquidhaskell/dist-newstyle/cache/plan.json') }}
+
+      - name: Install dependencies
+        working-directory: ./Diff-liquidhaskell
+        run: cabal build --dependencies-only -j Diff-liquidhaskell
+
+      - name: Build (run LiquidHaskell checks)
+        working-directory: ./Diff-liquidhaskell
+        run: cabal build -j Diff-liquidhaskell

.gitignore

@@ -1 +1,2 @@
-/dist-newstyle/
+dist-newstyle/
+cabal.project.local

Diff-liquidhaskell/Diff-liquidhaskell.cabal

@@ -0,0 +1,38 @@
+cabal-version: 2.4
+name:          Diff-liquidhaskell
+version:       0.1.0.0
+synopsis:      Liquid Haskell static checks for the Diff package
+description:
+  Provides a test suite whose build executes Diff's Liquid Haskell refinement type
+  annotation checks.
+  Exists as a separate package to break the cyclic dependency:
+  Diff -> liquidhaskell -> liquidhaskell-boot -> Diff.
+license:       BSD-3-Clause
+build-type:    Simple
+
+tested-with:   GHC == 9.14.1
+
+library
+  default-language: Haskell2010
+  -- Re-use the main Diff source tree so Liquid Haskell checks the real code.
+  hs-source-dirs:   ../src
+  -- No modules are exposed because this package is intended
+  -- for checking the build only.
+  other-modules:
+    Data.Algorithm.Diff
+    Data.Algorithm.DiffOutput
+    Data.Algorithm.DiffContext
+    Internal.LiftedFunctions
+  build-depends:
+      base          >= 4.22.0.0 && < 5
+    , array
+    , pretty        >= 1.1
+      -- LH version scheme: 0.<GHC_VERSION>.<LH_REVISION>
+      -- Update the corresponding versions in .github/workflows/liquidhaskell.yml
+      -- after upgrading GHC and LH to keep CI in sync.
+    , liquidhaskell ^>= 0.9.14.1.1
+  -- Recompilation check is disabled to make sure changes to specification
+  -- annotations are checked by the LH plugin (otherwise they are silently ignored
+  -- if no source change is introduced).
+  -- All warnings are disabled to focus on LH output.
+  ghc-options: -fplugin=LiquidHaskell -O0 -fforce-recomp -w

Diff.cabal

@@ -13,6 +13,7 @@ license-file:        LICENSE
 author:              Sterling Clover
 maintainer:          David Fox <dsf@seereason.com>
 Build-Type:          Simple
+extra-doc-files:     README.md
 
 tested-with:
   GHC == 9.14.1
@@ -41,6 +42,7 @@ library
                    Data.Algorithm.Diff
                    Data.Algorithm.DiffOutput
                    Data.Algorithm.DiffContext
+  other-modules:   Internal.LiftedFunctions
   ghc-options:     -Wall -funbox-strict-fields
 
 source-repository head