Replace Python qualification and release scripts with F#

.github/workflows/automata-providers.yml

@@ -6,6 +6,7 @@ on:
   pull_request:
     paths:
       - 'examples/AutomataProviders/**'
+      - 'eng/Qualification/**'
       - '.github/workflows/automata-providers.yml'
       - 'global.json'
       - 'Directory.Build.props'
@@ -23,12 +24,12 @@ jobs:
       - name: Install compiler prerequisites
         run: sudo apt-get update && sudo apt-get install -y build-essential bison flex perl pkg-config
       - name: Build pinned private PostgreSQL and extensions
-        run: python3 examples/AutomataProviders/provision.py "$RUNNER_TEMP/providers"
+        run: dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- providers-provision "$RUNNER_TEMP/providers"
       - name: Run all provider contracts and process-kill recovery checks
         run: >-
-          python3 examples/AutomataProviders/check.py
-          --automata-source "$RUNNER_TEMP/providers/automata"
-          --postgres-bin "$RUNNER_TEMP/providers/tools/bin"
+          dotnet run --project eng/Qualification/Qualification.fsproj -c Release --
+          providers-check "$RUNNER_TEMP/providers/automata"
+          "$RUNNER_TEMP/providers/tools/bin"
       - uses: actions/upload-artifact@v7
         if: always()
         with:

.github/workflows/release.yml

@@ -32,6 +32,8 @@ jobs:
       - uses: actions/setup-dotnet@v6
         with:
           global-json-file: global.json
+      - name: Check F# readback guards
+        run: dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- selftest
       - name: Read-only recovery verification
         if: inputs.readback_version != ''
         env:
@@ -41,7 +43,7 @@ jobs:
           set -euo pipefail
           [[ "$READBACK_VERSION" =~ ^[0-9]+\.[0-9]+\.[0-9]+(-[A-Za-z0-9.-]+)?$ ]]
           source_head=$(git rev-parse "refs/tags/v$READBACK_VERSION^{commit}")
-          python3 eng/readback.py "$READBACK_VERSION" "$source_head"
+          dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- readback "$READBACK_VERSION" "$source_head"
           bash eng/public-example.sh "$READBACK_VERSION"
       - name: NuGet trusted publishing identity
         id: nuget
@@ -75,7 +77,7 @@ jobs:
         if: github.event_name == 'push'
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: python3 eng/readback.py "${GITHUB_REF_NAME#v}"
+        run: dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- readback "${GITHUB_REF_NAME#v}"
       - name: Anonymous public package example
         if: github.event_name == 'push'
         run: bash eng/public-example.sh

README.md

@@ -80,7 +80,7 @@ Run the committed-trace consumer from this checkout:
 
 ```sh
 dotnet pack src/FsQuint/FsQuint.fsproj -c Release -o artifacts/packages
-python3 examples/AutomataReplay/check.py
+dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- replay
 ```
 
 This creates an isolated package consumer and verifies dependency provenance before

docs/automata-integration.md

@@ -29,7 +29,7 @@ From the repository root, using SDK 10.0.401:
 
 ```sh
 dotnet pack src/FsQuint/FsQuint.fsproj -c Release -o artifacts/packages
-python3 examples/AutomataReplay/check.py
+dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- replay
 ```
 
 This restores an isolated NuGet consumer and runs package characterization, application
@@ -59,8 +59,8 @@ Use a fresh destination for provisioning. This adds pinned Quint typechecking, w
 fixed-seed simulation, fixture regeneration and required coverage checks. Regeneration
 compares semantic states and preserves raw bytes for unchanged committed fixtures; it
 refuses a changed regression trace rather than silently replacing expected behavior.
-The [generation script](../examples/AutomataReplay/regenerate.py) exposes explicit
-`--write` for deliberately adding reviewed new fixtures.
+The [F# generator](../eng/Qualification/Generation.fs) exposes `generate --write`
+for deliberately adding reviewed new fixtures.
 
 The resolver's [bounded-check evidence](../examples/AutomataReplay/fixtures/resolver/bounded-check.json)
 records a separate completed Apalache check through two transitions. Ordinary CI does not

docs/roadmaps/2026-09-27-090245-quint-automata-integration.md

@@ -432,7 +432,7 @@ Stages are intentionally evidence-based. Estimates are planning ranges for one e
   dependency is justified by the current local-only consumer demand.
 - [x] **FQA-4 — scenario generation and evidence:** merged in [PR #34](https://github.com/FS-GG/FsQuint/pull/34),
   commit `439bfe473e5f6c96e7624584f8a2d6c08b8caf20`; merge readback confirmed.
-  [Regeneration](../../examples/AutomataReplay/regenerate.py) pins Quint/evaluator bytes,
+  [Regeneration](../../eng/Qualification/Generation.fs) pins Quint/evaluator bytes,
   reproduces fixed witnesses and eight 30-step samples, and compares semantic artifacts
   while preserving original raw bytes. Sampled manifests bind the dedicated input channel,
   seed, bounds, model digest and source location. [Coverage](../../examples/AutomataReplay/fixtures/coverage.json)

eng/NuspecIdentity.fsx

@@ -1,72 +1,2 @@
 #load "archive-fingerprint.fsx"
-
-open System
-open System.IO
-open System.IO.Compression
-open System.Text.RegularExpressions
-open System.Xml
-open System.Xml.Linq
-open ArchiveFingerprint
-
-type Identity = {
-    Id: string
-    Version: string
-    RepositoryCommit: string
-    NuspecSha256: string
-}
-
-let private invalid message = raise (InvalidDataException message)
-let private sha = Regex(@"\A[0-9a-f]{40}\z", RegexOptions.CultureInvariant)
-
-let private one name (elements: seq<XElement>) =
-    match elements |> Seq.toList with
-    | [ value ] -> value
-    | _ -> invalid $"nuspec must contain one {name}"
-
-/// Read-only identity check for a caller-supplied expected release commit.
-/// The caller must qualify the expected commit and archive provenance separately.
-let verify (path: string) (expectedId: string) (expectedVersion: string)
-           (expectedCommit: string) : Identity =
-    if String.IsNullOrWhiteSpace expectedId || expectedId.Contains('/')
-       || expectedId.Contains('\\') || String.IsNullOrWhiteSpace expectedVersion
-       || String.IsNullOrWhiteSpace expectedCommit || not (sha.IsMatch expectedCommit) then
-        invalid "expected nuspec identity is invalid"
-
-    let members = ArchiveFingerprint.inspect path
-    let expectedName = expectedId + ".nuspec"
-    let manifests =
-        members
-        |> List.filter (fun member' -> member'.Name.EndsWith(".nuspec", StringComparison.OrdinalIgnoreCase))
-    let manifest =
-        match manifests with
-        | [ only ] when only.Name = expectedName -> only
-        | _ -> invalid "archive must contain one exact root nuspec"
-
-    use archive = ZipFile.OpenRead path
-    let entry = archive.GetEntry expectedName
-    if isNull entry then invalid "nuspec archive entry is missing"
-    use stream = entry.Open()
-    let settings = XmlReaderSettings(
-        DtdProcessing = DtdProcessing.Prohibit,
-        XmlResolver = null,
-        MaxCharactersInDocument = 1_048_576L
-    )
-    use reader = XmlReader.Create(stream, settings)
-    let document =
-        try XDocument.Load reader
-        with :? XmlException -> invalid "nuspec XML is invalid"
-    let root = document.Root
-    if isNull root || root.Name.LocalName <> "package" then invalid "nuspec package root is invalid"
-    let metadata = one "metadata" (root.Elements() |> Seq.filter (fun item -> item.Name.LocalName = "metadata"))
-    let value name =
-        one name (metadata.Elements() |> Seq.filter (fun item -> item.Name.LocalName = name))
-        |> fun item -> item.Value
-    let id = value "id"
-    let version = value "version"
-    let repository =
-        one "repository" (metadata.Elements() |> Seq.filter (fun item -> item.Name.LocalName = "repository"))
-    let commit = repository.Attribute(XName.Get "commit")
-    let observedCommit = if isNull commit then "" else commit.Value
-    if id <> expectedId || version <> expectedVersion || observedCommit <> expectedCommit then
-        invalid "nuspec identity differs from expected package or release commit"
-    { Id = id; Version = version; RepositoryCommit = observedCommit; NuspecSha256 = manifest.Sha256 }
+#load "Qualification/NuspecIdentity.fs"

eng/Qualification/ArchiveFingerprint.fs

@@ -0,0 +1,84 @@
+// Cross-feed equality uses the original readback member-name and payload-digest
+// contract. Mode is recorded for audit and symlink refusal.
+module ArchiveFingerprint
+
+open System
+open System.IO
+open System.IO.Compression
+open System.Security.Cryptography
+
+type Member = {
+    Name: string
+    Sha256: string
+    UnixMode: int
+}
+
+let private signature = ".signature.p7s"
+let private invalidData message = raise (InvalidDataException message)
+
+let private safeMemberName (name: string) =
+    let path = if name.EndsWith("/", StringComparison.Ordinal) then name.Substring(0, name.Length - 1) else name
+    not (String.IsNullOrWhiteSpace path)
+    && not (name.StartsWith("/", StringComparison.Ordinal))
+    && not (name.Contains('\\') || name.Contains(':') || name.Contains(char 0))
+    && (path.Split('/') |> Array.forall (fun segment -> segment <> "" && segment <> "." && segment <> ".."))
+
+let private asciiFold (name: string) =
+    let characters = name.ToCharArray()
+    for index in 0 .. characters.Length - 1 do
+        if characters.[index] >= 'A' && characters.[index] <= 'Z' then
+            characters.[index] <- char (int characters.[index] + 32)
+    String(characters)
+
+let inspect (path: string) : Member list =
+    use archive = ZipFile.OpenRead path
+    let names = System.Collections.Generic.HashSet<string>(StringComparer.Ordinal)
+    let aliases = System.Collections.Generic.HashSet<string>(StringComparer.Ordinal)
+
+    [
+        for entry in archive.Entries do
+            if not (names.Add entry.FullName) then
+                invalidData $"{path}: duplicate archive member '{entry.FullName}'"
+
+            if not (safeMemberName entry.FullName) then
+                invalidData $"{path}: unsafe archive member '{entry.FullName}'"
+
+            if not (aliases.Add(asciiFold entry.FullName)) then
+                invalidData $"{path}: case-alias archive member '{entry.FullName}'"
+
+            let mode = (entry.ExternalAttributes >>> 16) &&& 0xffff
+            if mode &&& 0o170000 = 0o120000 then
+                invalidData $"{path}: symlink archive member '{entry.FullName}'"
+
+            if entry.FullName <> signature then
+                use stream = entry.Open()
+                let digest = SHA256.HashData stream |> Convert.ToHexString |> fun value -> value.ToLowerInvariant()
+
+                {
+                    Name = entry.FullName
+                    Sha256 = digest
+                    UnixMode = mode
+                }
+    ]
+    |> List.sortBy _.Name
+    |> fun members ->
+        if members |> List.exists (fun member' -> not (member'.Name.EndsWith("/", StringComparison.Ordinal))) then members
+        else invalidData $"{path}: archive has no payload members"
+
+let compare (qualified: string) (served: string) : unit =
+    let expected = inspect qualified |> List.map (fun member' -> member'.Name, member') |> Map.ofList
+    let actual = inspect served |> List.map (fun member' -> member'.Name, member') |> Map.ofList
+    let expectedNames = expected |> Map.keys |> Set.ofSeq
+    let actualNames = actual |> Map.keys |> Set.ofSeq
+    let missing = Set.difference expectedNames actualNames
+    let unexpected = Set.difference actualNames expectedNames
+
+    if not missing.IsEmpty || not unexpected.IsEmpty then
+        invalidData $"archive members differ: missing={Set.toList missing}; unexpected={Set.toList unexpected}"
+
+    for name in expectedNames do
+        let before = expected.[name]
+        let after = actual.[name]
+
+        if before.Sha256 <> after.Sha256 then
+            invalidData $"archive member '{name}' digest differs"

eng/Qualification/Common.fs

@@ -0,0 +1,58 @@
+namespace FsQuint.Qualification
+
+open System
+open System.Diagnostics
+open System.IO
+open System.Security.Cryptography
+open System.Text.Json
+open System.Text.Json.Nodes
+
+module Common =
+    let root = Path.GetFullPath(Path.Combine(__SOURCE_DIRECTORY__, "..", ".."))
+    let replay = Path.Combine(root, "examples", "AutomataReplay")
+    let providers = Path.Combine(root, "examples", "AutomataProviders")
+    let path (parts: string list) = Path.Combine(Array.ofList parts)
+    let shaBytes (bytes: byte[]) = SHA256.HashData bytes |> Convert.ToHexString |> fun s -> s.ToLowerInvariant()
+    let shaFile file = File.ReadAllBytes file |> shaBytes
+    let shaText (value: string) = System.Text.Encoding.UTF8.GetBytes value |> shaBytes
+    let read file = JsonNode.Parse(File.ReadAllText file)
+    let prop (node: JsonNode) (key: string) = node.[key]
+    let str (node: JsonNode) = node.GetValue<string>()
+    let num (node: JsonNode) = node.GetValue<int>()
+    let arr (node: JsonNode) = node.AsArray() |> Seq.toList
+    let obj (pairs: (string * JsonNode) list) =
+        let value = JsonObject()
+        for key, item in pairs do value.Add(key, if isNull item then null else item.DeepClone())
+        value :> JsonNode
+    let jstr (s: string) = JsonValue.Create(s) :> JsonNode
+    let jint (n: int) = JsonValue.Create(n) :> JsonNode
+    let jarray (items: JsonNode seq) = JsonArray(items |> Seq.map (fun n -> if isNull n then null else n.DeepClone()) |> Seq.toArray) :> JsonNode
+    let jsonOptions = JsonSerializerOptions(WriteIndented = true)
+    let writeJson (file: string) (value: JsonNode) =
+        Directory.CreateDirectory(Path.GetDirectoryName file) |> ignore
+        File.WriteAllText(file, value.ToJsonString(jsonOptions) + "\n")
+    let ensure condition message = if not condition then failwith message
+    let runCommand (exe: string) (args: string list) (cwd: string) (environment: (string * string option) list) (timeoutSeconds: int) =
+        use p = new Process()
+        p.StartInfo.FileName <- exe
+        p.StartInfo.WorkingDirectory <- cwd
+        p.StartInfo.UseShellExecute <- false
+        p.StartInfo.RedirectStandardOutput <- true
+        p.StartInfo.RedirectStandardError <- true
+        for item in args do p.StartInfo.ArgumentList.Add item
+        for key, value in environment do
+            match value with Some text -> p.StartInfo.Environment.[key] <- text | None -> p.StartInfo.Environment.Remove(key) |> ignore
+        ensure (p.Start()) ("could not start " + exe)
+        let output = p.StandardOutput.ReadToEndAsync()
+        let errors = p.StandardError.ReadToEndAsync()
+        if not (p.WaitForExit(timeoutSeconds * 1000)) then
+            p.Kill(true)
+            failwithf "%s timed out after %ds" exe timeoutSeconds
+        let result = output.Result + errors.Result
+        ensure (p.ExitCode = 0) (sprintf "%s %A failed (%d):\n%s" exe args p.ExitCode result)
+        result
+    type Temporary(prefix: string) =
+        let directory = Path.Combine(Path.GetTempPath(), prefix + Guid.NewGuid().ToString("N"))
+        do Directory.CreateDirectory directory |> ignore
+        member _.Path = directory
+        interface IDisposable with member _.Dispose() = Directory.Delete(directory, true)