From f2f901eb4e6fb30b381c3b5e312da75cb8d29622 Mon Sep 17 00:00:00 2001 From: EHotwagner Date: Sun, 27 Sep 2026 13:48:04 +0200 Subject: [PATCH] Replace Python qualification and release harnesses with F# --- .github/workflows/automata-providers.yml | 9 +- .github/workflows/release.yml | 6 +- README.md | 2 +- docs/automata-integration.md | 6 +- ...09-27-090245-quint-automata-integration.md | 2 +- eng/NuspecIdentity.fsx | 72 +------ eng/Qualification/ArchiveFingerprint.fs | 84 ++++++++ eng/Qualification/Common.fs | 58 +++++ eng/Qualification/Generation.fs | 156 ++++++++++++++ eng/Qualification/NuspecIdentity.fs | 72 +++++++ eng/Qualification/Program.fs | 28 +++ eng/Qualification/Providers.fs | 178 ++++++++++++++++ eng/Qualification/Qualification.fsproj | 18 ++ eng/Qualification/README.md | 29 +++ eng/Qualification/Readback.fs | 98 +++++++++ eng/Qualification/Replay.fs | 82 +++++++ eng/Qualification/SelfTest.fs | 119 +++++++++++ eng/Qualification/packages.lock.json | 13 ++ eng/archive-fingerprint.fsx | 86 +------- eng/archive-fingerprint.md | 2 + eng/check.sh | 3 +- eng/nuspec-identity.md | 2 + eng/packed-archive-characterization.md | 10 +- eng/public-example.sh | 12 +- eng/readback-case-alias.md | 2 + eng/readback-commit-source.md | 2 + eng/readback-member-guards.md | 2 + eng/readback-mode-policy.md | 2 + eng/readback-nonempty-payload.md | 2 + eng/readback-nuspec-root.md | 2 + eng/readback-nuspec-xml.md | 2 + eng/readback-tag-stability.md | 2 + eng/readback.py | 159 -------------- eng/test-packed-archive-fingerprint.py | 128 ----------- eng/test-readback-case-alias.py | 81 ------- eng/test-readback-commit-source.py | 148 ------------- eng/test-readback-member-guards.py | 95 --------- eng/test-readback-mode-policy.py | 72 ------- eng/test-readback-nonempty-payload.py | 82 ------- eng/test-readback-nuspec-root.py | 103 --------- eng/test-readback-nuspec-xml.py | 105 --------- eng/test-readback-tag-stability.py | 134 ------------ examples/AutomataProviders/README.md | 13 +- examples/AutomataProviders/check.py | 200 ------------------ examples/AutomataProviders/evidence.json | 28 +-- examples/AutomataProviders/provision.py | 55 ----- examples/AutomataReplay/README.md | 10 +- examples/AutomataReplay/check.py | 108 ---------- examples/AutomataReplay/regenerate.py | 185 ---------------- 49 files changed, 1004 insertions(+), 1865 deletions(-) create mode 100644 eng/Qualification/ArchiveFingerprint.fs create mode 100644 eng/Qualification/Common.fs create mode 100644 eng/Qualification/Generation.fs create mode 100644 eng/Qualification/NuspecIdentity.fs create mode 100644 eng/Qualification/Program.fs create mode 100644 eng/Qualification/Providers.fs create mode 100644 eng/Qualification/Qualification.fsproj create mode 100644 eng/Qualification/README.md create mode 100644 eng/Qualification/Readback.fs create mode 100644 eng/Qualification/Replay.fs create mode 100644 eng/Qualification/SelfTest.fs create mode 100644 eng/Qualification/packages.lock.json delete mode 100644 eng/readback.py delete mode 100644 eng/test-packed-archive-fingerprint.py delete mode 100644 eng/test-readback-case-alias.py delete mode 100644 eng/test-readback-commit-source.py delete mode 100644 eng/test-readback-member-guards.py delete mode 100644 eng/test-readback-mode-policy.py delete mode 100644 eng/test-readback-nonempty-payload.py delete mode 100644 eng/test-readback-nuspec-root.py delete mode 100644 eng/test-readback-nuspec-xml.py delete mode 100644 eng/test-readback-tag-stability.py delete mode 100644 examples/AutomataProviders/check.py delete mode 100644 examples/AutomataProviders/provision.py delete mode 100644 examples/AutomataReplay/check.py delete mode 100644 examples/AutomataReplay/regenerate.py diff --git a/.github/workflows/automata-providers.yml b/.github/workflows/automata-providers.yml index 9dd2d1e..f6e4687 100644 --- a/.github/workflows/automata-providers.yml +++ b/.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: diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 7308f10..2a02336 100644 --- a/.github/workflows/release.yml +++ b/.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 diff --git a/README.md b/README.md index 17233b3..01fe537 100644 --- a/README.md +++ b/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 diff --git a/docs/automata-integration.md b/docs/automata-integration.md index 9359460..2a322cd 100644 --- a/docs/automata-integration.md +++ b/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 diff --git a/docs/roadmaps/2026-09-27-090245-quint-automata-integration.md b/docs/roadmaps/2026-09-27-090245-quint-automata-integration.md index 7408972..06f8934 100644 --- a/docs/roadmaps/2026-09-27-090245-quint-automata-integration.md +++ b/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) diff --git a/eng/NuspecIdentity.fsx b/eng/NuspecIdentity.fsx index fb55940..130a58f 100644 --- a/eng/NuspecIdentity.fsx +++ b/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) = - 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" diff --git a/eng/Qualification/ArchiveFingerprint.fs b/eng/Qualification/ArchiveFingerprint.fs new file mode 100644 index 0000000..8ec9bf1 --- /dev/null +++ b/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(StringComparer.Ordinal) + let aliases = System.Collections.Generic.HashSet(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" diff --git a/eng/Qualification/Common.fs b/eng/Qualification/Common.fs new file mode 100644 index 0000000..3d4a787 --- /dev/null +++ b/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() + let num (node: JsonNode) = node.GetValue() + 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) diff --git a/eng/Qualification/Generation.fs b/eng/Qualification/Generation.fs new file mode 100644 index 0000000..d3ed538 --- /dev/null +++ b/eng/Qualification/Generation.fs @@ -0,0 +1,156 @@ +namespace FsQuint.Qualification + +open System +open System.Collections.Generic +open System.IO +open System.Text.RegularExpressions +open System.Text.Json.Nodes +open FsQuint.Qualification.Common + +module Generation = + let private semantic (raw: byte[]) = + let document = JsonNode.Parse raw + ensure (str (prop (prop document "#meta") "status") = "ok") "Quint did not report positive trace evidence" + let states = arr (prop document "states") |> List.map (fun state -> + let copy = state.DeepClone() + copy.AsObject().Remove("#meta") |> ignore + copy) + obj ["vars", prop document "vars"; "states", jarray states] + + let run write = + let baseline = read (Path.Combine(replay, "baseline.json")) + let quint = Environment.GetEnvironmentVariable "QUINT_BIN" + let evaluator = Path.Combine(Environment.GetEnvironmentVariable "QUINT_HOME", "rust-evaluator-v0.6.0", "quint_evaluator") + ensure (shaFile quint = str (prop baseline "quintSha256") && shaFile evaluator = str (prop baseline "evaluatorSha256")) "Generator/evaluator identity differs from baseline" + let sources = Directory.GetFiles(replay, "*.qnt") |> Array.sort |> Array.map (fun file -> Path.GetFileName file, shaFile file) |> Map.ofArray + let commands = ResizeArray() + let inputs = HashSet() + let phases, outcomes, orders = HashSet(), HashSet(), HashSet() + let paths, handlers, markers = HashSet(), HashSet(), HashSet() + let invoke args = + commands.Add(jarray (args |> List.map jstr)) + runCommand quint args replay [] 120 |> ignore + let checkJson file value = + if write then writeJson file value + else ensure (JsonNode.DeepEquals(read file, value)) ("Manifest/coverage differs: " + file) + let accept candidate relative = + let target = Path.Combine(replay, "fixtures", relative) + let parsed = semantic (File.ReadAllBytes candidate) + if write then + Directory.CreateDirectory(Path.GetDirectoryName target) |> ignore + if File.Exists target then + ensure (JsonNode.DeepEquals(parsed, semantic (File.ReadAllBytes target))) ("Existing regression changed: " + relative) + else File.Copy(candidate, target) + else + ensure (JsonNode.DeepEquals(parsed, semantic (File.ReadAllBytes target))) ("Regeneration differs semantically: " + relative) + target, arr (prop parsed "states") + let matchOne folder pattern = + match Directory.GetFiles(folder, pattern) with + | [| file |] -> file + | _ -> failwith ("Missing or ambiguous witness output: " + pattern) + let allowed = Set.ofList ["submit","author"; "approve","author"; "approve","reviewer"; "publish","author"; "cancel","author"; "remind","author"] + let binding target states entries source seed sampled = + ensure (List.length entries = List.length states - 1) "Input count differs" + for entry, state in List.zip entries (List.tail states) do + let input = prop state "input" + let actual = str (prop input "op"), str (prop input "actor") + ensure (input.AsObject().Count = 2 && allowed.Contains actual) "Unknown generated input" + ensure (fst actual = str (prop entry "op") && snd actual = str (prop entry "actor")) "Authored input differs from instrumented input" + inputs.Add actual |> ignore + for item in states do + let state = prop item "state" + phases.Add(str (prop state "phase")) |> ignore + outcomes.Add(str (prop state "outcome")) |> ignore + let order = arr (prop state "actions") |> List.map (fun action -> str (prop action "kind") + ":" + str (prop action "name")) |> String.concat "|" + orders.Add order |> ignore + let properties = + ["schema", jstr (if sampled then "fsquint.approval-binding/2" else "fsquint.approval-binding/1") + "profile", jstr "fsquint.automata-approval/1" + "traceSha256", jstr (shaFile target) + "modelSha256", jstr sources.["approval.qnt"] + "scenarioSha256", jstr sources.[source] + "steps", jarray entries] + @ if sampled then ["sourceFile", jstr source; "seed", jstr (string seed); "maxSteps", jint 30] else [] + let bindingFile = Path.ChangeExtension(Path.ChangeExtension(target, null), ".binding.json") + checkJson bindingFile (obj properties) + use scratch = new Temporary("fsquint-generation-") + for moduleName in ["approval"; "resolver"; "turnstile"; "correction"; "protocol"] do + invoke ["typecheck"; moduleName + ".qnt"] + invoke ["test"; moduleName + "_test.qnt"; "--seed"; "42"; "--max-samples"; "1"; "--out-itf"; Path.Combine(scratch.Path, moduleName + "_{test}_{seq}.itf.json")] + let authored = Dictionary>() + let mutable current = "" + File.ReadAllLines(Path.Combine(replay, "approval_test.qnt")) |> Array.iteri (fun index line -> + let action = Regex.Match(line, @"run (\w+)") + if action.Success then + current <- action.Groups.[1].Value + authored.[current] <- ResizeArray() + let operation = Regex.Match(line, "op: \"(\\w+)\", actor: \"(\\w+)\"") + if operation.Success then + let entries = authored.[current] + entries.Add(obj ["index", jint (entries.Count + 1); "op", jstr operation.Groups.[1].Value; "actor", jstr operation.Groups.[2].Value; "line", jint (index + 1)])) + for KeyValue(name, entries) in authored do + let target, states = accept (matchOne scratch.Path (sprintf "approval_%s_*.itf.json" name)) (name + ".itf.json") + binding target states (List.ofSeq entries) "approval_test.qnt" 42 false + for index in 0..12 do + let _, states = accept (matchOne scratch.Path (sprintf "resolver_case%dTest_*.itf.json" index)) (sprintf "resolver/case%d.itf.json" index) + let result = prop (List.last states) "result" + let exits = arr (prop result "exited") |> List.map str + let entered = arr (prop result "entered") |> List.map str + paths.Add(String.concat "/" exits + "|" + String.concat "/" entered) |> ignore + handlers.Add(str (prop result "handler")) |> ignore + for action in arr (prop result "actions") do + if str (prop action "kind") = "rule" then markers.Add(str (prop action "node")) |> ignore + accept (matchOne scratch.Path "turnstile_passageTest_*.itf.json") "turnstile.itf.json" |> ignore + for moduleName, count in ["correction", 10; "protocol", 7] do + for index in 0..count-1 do + accept (matchOne scratch.Path (sprintf "%s_case%dTest_*.itf.json" moduleName index)) (sprintf "%s/case%d.itf.json" moduleName index) |> ignore + let line = File.ReadAllLines(Path.Combine(replay, "approval.qnt")) |> Array.findIndex (fun line -> line.Contains("action step")) |> (+) 1 + for seed in [1;7;42;99;123;1000;2000;3000] do + let candidate = Path.Combine(scratch.Path, sprintf "sample-%d.itf.json" seed) + invoke ["run"; "approval.qnt"; "--invariant"; "safety"; "--seed"; string seed; "--max-samples"; "1"; "--max-steps"; "30"; "--out-itf"; candidate] + let target, states = accept candidate (sprintf "sampled/seed-%d.itf.json" seed) + let entries = List.tail states |> List.mapi (fun index state -> + let input = prop state "input" + obj ["index", jint (index + 1); "op", prop input "op"; "actor", prop input "actor"; "line", jint line]) + binding target states entries "approval.qnt" seed true + let manifest file names = + let pairs = names |> List.map (fun name -> name, jstr (shaFile (Path.Combine(replay, name)))) + checkJson (Path.Combine(replay, "fixtures", file)) (obj pairs) + manifest "resolver/manifest.json" (["resolver.qnt"; "resolver_test.qnt"] @ [for i in 0..12 -> sprintf "fixtures/resolver/case%d.itf.json" i]) + manifest "turnstile.manifest.json" ["fixtures/turnstile.itf.json"; "turnstile.qnt"; "turnstile_test.qnt"] + manifest "correction/manifest.json" (["correction.qnt"; "correction_test.qnt"] @ [for i in 0..9 -> sprintf "fixtures/correction/case%d.itf.json" i]) + manifest "protocol/manifest.json" (["protocol.qnt"; "protocol_test.qnt"] @ [for i in 0..6 -> sprintf "fixtures/protocol/case%d.itf.json" i]) + ensure (Set.ofSeq inputs = allowed && Set.ofSeq phases = Set.ofList ["Draft";"Pending";"Approved";"Published";"Cancelled"]) "Required input/phase coverage missing" + ensure (Set.ofList ["Initial";"Applied";"NotAuthorized";"Unhandled";"Terminated"] |> Set.isSubset (Set.ofSeq outcomes)) "Required outcome coverage missing" + for order in ["audit:submitted|notify:review"; "audit:published|notify:published"] do ensure (orders.Contains order) "Required ordered action coverage missing" + let stringArray (values: seq) = values |> Seq.sort |> Seq.map jstr |> jarray + let splitOrder (value: string) = value.Split('|', StringSplitOptions.RemoveEmptyEntries) |> Seq.map (fun (item: string) -> item.Split(':') |> Seq.map jstr |> jarray) |> jarray + let coverage = obj [ + "schema", jstr "fsquint.coverage/1" + "inputs", (inputs |> Seq.sort |> Seq.map (fun (a,b) -> jarray [jstr a; jstr b]) |> jarray) + "phases", stringArray phases + "outcomes", stringArray outcomes + "resolverCases", (seq {0..12} |> Seq.map jint |> jarray) + "correctionCases", (seq {0..9} |> Seq.map jint |> jarray) + "protocolSchedules", (seq {0..6} |> Seq.map jint |> jarray) + "actionOrders", (orders |> Seq.sort |> Seq.map splitOrder |> jarray) + "resolverPaths", (paths |> Seq.sortWith (fun a b -> + let parts (value: string) = + let sides = value.Split('|') + sides.[0].Split('/', StringSplitOptions.RemoveEmptyEntries) |> Array.toList, + sides.[1].Split('/', StringSplitOptions.RemoveEmptyEntries) |> Array.toList + compare (parts a) (parts b)) |> Seq.map (fun text -> + let sides = text.Split('|') + let elements side = sides.[side].Split('/', StringSplitOptions.RemoveEmptyEntries) |> Seq.map jstr |> jarray + jarray [elements 0; elements 1]) |> jarray) + "resolverHandlers", stringArray handlers + "ruleMarkers", stringArray markers + "sampleSeeds", ([1;7;42;99;123;1000;2000;3000] |> Seq.map jint |> jarray) + "sampleStepBound", jint 30 + "claim", jstr "required bins exercised; no exhaustive application/runtime claim"] + checkJson (Path.Combine(replay, "fixtures/coverage.json")) coverage + let files = Directory.GetFiles(Path.Combine(replay, "fixtures"), "*.json", SearchOption.AllDirectories) |> Array.sort + let digests = files |> Array.map (fun file -> Path.GetRelativePath(replay, file).Replace('\\','/'), jstr (shaFile file)) |> Array.toList + let evidence = obj ["schema", jstr "fsquint.generation-evidence/1"; "outcome", jstr "passed"; "quintSha256", jstr (shaFile quint); "evaluatorSha256", jstr (shaFile evaluator); "sourceDigests", obj (sources |> Map.toList |> List.map (fun (k,v) -> k,jstr v)); "coverage", coverage; "commands", jarray commands; "rawAndBindingDigests", obj digests] + writeJson (Path.Combine(root, "artifacts/automata-generation.json")) evidence + printfn "PASS: pinned witness/sample regeneration, explicit input bindings and all required coverage bins." diff --git a/eng/Qualification/NuspecIdentity.fs b/eng/Qualification/NuspecIdentity.fs new file mode 100644 index 0000000..a6853f5 --- /dev/null +++ b/eng/Qualification/NuspecIdentity.fs @@ -0,0 +1,72 @@ +module NuspecIdentity + +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) = + 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 } diff --git a/eng/Qualification/Program.fs b/eng/Qualification/Program.fs new file mode 100644 index 0000000..f5bb298 --- /dev/null +++ b/eng/Qualification/Program.fs @@ -0,0 +1,28 @@ +namespace FsQuint.Qualification + +open System +open System.Xml.Linq + +module Program = + [] + let main argv = + try + match argv with + | [| "replay" |] -> Replay.run() + | [| "generate" |] -> Generation.run false + | [| "generate"; "--write" |] -> Generation.run true + | [| "providers-provision"; destination |] -> Providers.provision destination + | [| "providers-check"; source; binaries |] -> Providers.check source binaries + | [| "readback"; version |] -> Readback.run version None + | [| "readback"; version; commit |] -> Readback.run version (Some commit) + | [| "selftest" |] -> SelfTest.run() + | [| "set-package-version"; project; version |] -> + let document = XDocument.Load project + let reference = document.Descendants() |> Seq.find (fun e -> e.Name.LocalName = "PackageReference" && e.Attribute(XName.Get "Include").Value = "FsQuint") + reference.SetAttributeValue(XName.Get "Version", version) + document.Save project + | _ -> failwith "usage: Qualification replay|generate [--write]|providers-provision DEST|providers-check SOURCE POSTGRES_BIN|readback VERSION [COMMIT]" + 0 + with error -> + eprintfn "%s" error.Message + 1 diff --git a/eng/Qualification/Providers.fs b/eng/Qualification/Providers.fs new file mode 100644 index 0000000..50b58ad --- /dev/null +++ b/eng/Qualification/Providers.fs @@ -0,0 +1,178 @@ +namespace FsQuint.Qualification + +open System +open System.IO +open System.IO.Compression +open System.Diagnostics +open System.Text.RegularExpressions +open System.Text.Json.Nodes +open System.Xml.Linq +open System.Threading +open FsQuint.Qualification.Common + +module Providers = + let private source = "03c3282f25888a32d36e53fa708f0342c328ccfc" + let private pins = + ["postgres", "https://github.com/postgres/postgres.git", "3638289fb57bdabec00deda98ee9624a35f5d66a" + "pgmq", "https://github.com/pgmq/pgmq.git", "51d7655a097d91bf05ad5ae40dd604aa067ed355" + "pg_cron", "https://github.com/citusdata/pg_cron.git", "5cedfa472ccc83567aa23ec645925ed8489a7797" + "automata", "https://github.com/byzantine-systems/automata.git", source] + let provision destination = + let destination = Path.GetFullPath destination + ensure (not (Directory.Exists destination)) "destination already exists" + Directory.CreateDirectory destination |> ignore + let prefix = Path.Combine(destination, "tools") + let clone name folder = + let _, url, commit = pins |> List.find (fun (key, _, _) -> key = name) + Directory.CreateDirectory folder |> ignore + runCommand "git" ["init"; "-q"] folder [] 900 |> ignore + runCommand "git" ["fetch"; "--depth"; "1"; url; commit] folder [] 900 |> ignore + runCommand "git" ["checkout"; "--detach"; "FETCH_HEAD"] folder [] 900 |> ignore + use temporary = new Temporary("fsquint-provider-build-") + let pg = Path.Combine(temporary.Path, "postgres") + clone "postgres" pg + runCommand (Path.Combine(pg, "configure")) ["--prefix=" + prefix; "--without-readline"; "--without-icu"; "--without-zlib"] pg [] 900 |> ignore + for args in [["-j4"];["install"];["-C";"contrib/btree_gist";"install"]] do runCommand "make" args pg [] 900 |> ignore + for name, subdir in ["pgmq", "pgmq-extension"; "pg_cron", "."] do + let location = Path.Combine(temporary.Path, name) + clone name location + let directory = Path.Combine(location, subdir) + let option = "PG_CONFIG=" + Path.Combine(prefix, "bin/pg_config") + runCommand "make" [option] directory [] 900 |> ignore + runCommand "make" ["install"; option] directory [] 900 |> ignore + clone "automata" (Path.Combine(destination, "automata")) + let pinData = pins |> List.map (fun (name,url,commit) -> name, jarray [jstr url; jstr commit]) + writeJson (Path.Combine(destination, "pins.json")) (obj pinData) + let private suite (sourcePath: string) (output: string) (provider: string) (database: (string * string) option) (selected: string option) = + let label = if selected.IsSome then provider + "-correction" else provider + let start = Stopwatch.StartNew() + let command = ["run"; "--project"; sprintf "tests/ByzantineSystems.Automata.Storage.%s.Tests" provider; "-c"; "Release"; "--"; "--summary"; "--sequenced"] + @ (match selected with Some name -> ["--filter-test-case"; name] | None -> []) + use scratch = new Temporary("fsquint-suite-") + let environment = ["AUTOMATA_TEST_DB", database |> Option.map fst; + "AUTOMATA_TEST_CRON_DB", database |> Option.map snd; + "TMPDIR", Some scratch.Path] + let log = + try runCommand "dotnet" command sourcePath environment 300 + with error -> + File.WriteAllText(Path.Combine(output, label + ".log"), error.Message) + reraise() + File.WriteAllText(Path.Combine(output, label + ".log"), log) + let clean = Regex.Replace(log, "\\x1b\\[[0-9;?]*[A-Za-z]", "") + let counts = Regex.Match(clean, "(\\d+) tests run.*?(\\d+) passed,\\s*(\\d+) ignored,\\s*(\\d+) failed,\\s*(\\d+) errored", RegexOptions.Singleline) + let expected = if selected.IsSome then 1 elif provider = "Sqlite" then 118 else 152 + ensure (counts.Success && int counts.Groups.[1].Value = expected && counts.Groups.[1].Value = counts.Groups.[2].Value && [3..5] |> List.forall (fun index -> int counts.Groups.[index].Value = 0)) (provider + ": missing, ignored or failing provider contracts; inspect log") + obj ["tests", jint expected; "passed", jint expected; "ignored", jint 0; + "elapsedSeconds", JsonValue.Create(Math.Round(start.Elapsed.TotalSeconds, 3)) :> JsonNode; + "command", jarray (["dotnet"] @ command |> List.map jstr); + "logSha256", jstr (shaText log)] + + let private crash (provider: string) (connection: string) (restart: unit -> unit) = + let start = Stopwatch.StartNew() + let dll = Path.Combine(providers, "bin/Release/net10.0/AutomataProviders.dll") + use worker = new Process() + worker.StartInfo.FileName <- "dotnet" + for arg in [dll; provider; "seed"; connection] do worker.StartInfo.ArgumentList.Add arg + worker.StartInfo.UseShellExecute <- false + worker.StartInfo.RedirectStandardOutput <- true + worker.StartInfo.RedirectStandardError <- true + ensure (worker.Start()) "could not start provider seed worker" + let mutable boundary = "" + try + let line = worker.StandardOutput.ReadLineAsync() + ensure (line.Wait(TimeSpan.FromSeconds 30.)) "provider never reached crash boundary" + boundary <- line.Result + ensure (Regex.IsMatch(boundary, "^READY (\\d+) (\\d+)$")) ("bad crash boundary: " + boundary) + finally + if not worker.HasExited then worker.Kill(true) + worker.WaitForExit(10000) |> ignore + let parts = boundary.Split ' ' + restart() + Thread.Sleep 1100 + let result = runCommand "dotnet" [dll; provider; "recover"; connection; parts.[1]; parts.[2]] root [] 30 + ensure (result.Trim() = "RECOVERED state=2 epoch=2 actions=2") ("recovery mismatch: " + result) + obj ["boundary", jstr "commit-first-claim-second"; + "workerExit", jint worker.ExitCode; + "recovered", obj ["state", jint 2; "epoch", jint 2; "actions", jint 2; "newFenceToken", JsonValue.Create(true) :> JsonNode]; + "serverImmediateRestart", (JsonValue.Create((provider = "postgres")) :> JsonNode); + "elapsedSeconds", JsonValue.Create(Math.Round(start.Elapsed.TotalSeconds, 3)) :> JsonNode] + + let check sourcePath binaries = + let sourcePath, binaries = Path.GetFullPath sourcePath, Path.GetFullPath binaries + ensure (runCommand "git" ["rev-parse"; "HEAD"] sourcePath [] 30 |> fun s -> s.Trim() = source) "wrong Automata source" + ensure (runCommand "git" ["status"; "--porcelain"; "--untracked-files=normal"] sourcePath [] 30 |> String.IsNullOrWhiteSpace) "modified source" + let output = Path.Combine(root, "artifacts/automata-providers") + Directory.CreateDirectory output |> ignore + writeJson (Path.Combine(output, "report.json")) (obj ["status", jstr "incomplete"; "sourceCommit", jstr source]) + let pg name = Path.Combine(binaries, name) + let version = runCommand (pg "postgres") ["--version"] root [] 30 |> fun s -> s.Trim() + ensure (version = "postgres (PostgreSQL) 19beta3") "unqualified PostgreSQL version; use provider provisioning" + runCommand "dotnet" ["restore"; providers; "--locked-mode"] root [] 180 |> ignore + runCommand "dotnet" ["build"; providers; "-c"; "Release"; "--no-restore"] root [] 180 |> ignore + let cache = runCommand "dotnet" ["nuget"; "locals"; "global-packages"; "--list"] root [] 30 |> fun s -> s.Trim().Split(": ").[1] + let packages = ["sqlite";"postgres"] |> List.map (fun provider -> + let id = "byzantinesystems.automata.storage." + provider + let archive = Path.Combine(cache, id, "0.5.0", id + ".0.5.0.nupkg") + use zip = ZipFile.OpenRead archive + let entry = zip.Entries |> Seq.find (fun e -> e.FullName.EndsWith(".nuspec")) + use stream = entry.Open() + let xml = XDocument.Load stream + let repository = xml.Descendants() |> Seq.find (fun e -> e.Name.LocalName = "repository") + ensure (repository.Attribute(XName.Get "commit").Value = source) "provider package/source commit mismatch" + obj ["id", jstr id; "version", jstr "0.5.0"; "sourceCommit", jstr source; "sha256", jstr (shaFile archive)]) + let report = obj ["schemaVersion", jint 1; "sourceCommit", jstr source; + "sdk", jstr ((runCommand "dotnet" ["--version"] root [] 30).Trim()); + "postgres", jstr version; "packages", jarray packages; + "timeoutsSeconds", obj ["upstreamSuite", jint 300; "crashBoundary", jint 30; "recovery", jint 30]] + let sqlite = suite sourcePath output "Sqlite" None None + use sqliteDir = new Temporary("fsquint-sqlite-") + sqlite.AsObject().Add("crashRecovery", crash "sqlite" (Path.Combine(sqliteDir.Path, "store.db")) ignore) + report.AsObject().Add("sqlite", sqlite) + use scratch = new Temporary("fsquint-pg-") + let data, socket = Path.Combine(scratch.Path, "db"), Path.Combine(scratch.Path, "socket") + Directory.CreateDirectory socket |> ignore + runCommand (pg "initdb") ["-D"; data; "--auth=trust"; "--no-locale"] root [] 180 |> ignore + File.AppendAllText(Path.Combine(data, "postgresql.conf"), "\nshared_preload_libraries = 'pg_cron'\ncron.database_name = 'postgres'\ncron.use_background_workers = on\n") + let serverLog = Path.Combine(scratch.Path, "server.log") + let serverOptions = sprintf "-k %s -h '' -p 55439" socket + let startServer () = runCommand (pg "pg_ctl") ["-D"; data; "-l"; serverLog; "-o"; serverOptions; "-w"; "start"] root [] 60 |> ignore + let stopServer () = runCommand (pg "pg_ctl") ["-D"; data; "-m"; "immediate"; "-w"; "stop"] root [] 60 |> ignore + try + startServer() + let sql = "CREATE ROLE automata_app LOGIN; GRANT CREATE ON DATABASE postgres TO automata_app; GRANT CREATE ON SCHEMA public TO automata_app; CREATE EXTENSION btree_gist; CREATE EXTENSION pgmq; CREATE EXTENSION pg_cron; GRANT ALL ON SCHEMA pgmq TO automata_app; GRANT ALL ON ALL TABLES IN SCHEMA pgmq TO automata_app; GRANT ALL ON ALL SEQUENCES IN SCHEMA pgmq TO automata_app;" + runCommand (pg "psql") ["-h"; socket; "-p"; "55439"; "-d"; "postgres"; "-v"; "ON_ERROR_STOP=1"; "-c"; sql] root [] 60 |> ignore + let connection role = sprintf "Host=%s;Port=55439;Database=postgres;Username=%s;Pooling=false" socket role + let database = Some(connection "automata_app", connection Environment.UserName) + let postgres = suite sourcePath output "Postgres" database None + let restart () = stopServer(); startServer() + postgres.AsObject().Add("crashRecovery", crash "postgres" (fst database.Value) restart) + let correction = suite sourcePath output "Postgres" database (Some "a correction rewrites the timeline and keeps what was believed before it") + let beliefs () = + ["instance_state";"instance_state_history";"transition";"command_correction"] + |> List.map (fun table -> + let sql = sprintf "SELECT row_to_json(t)::text FROM fsm.%s t ORDER BY row_to_json(t)::text;" table + let rows = runCommand (pg "psql") ["-h"; socket; "-p"; "55439"; "-d"; "postgres"; "-At"; "-c"; sql] root [] 60 + |> fun output -> output.Split('\n', StringSplitOptions.RemoveEmptyEntries) |> Seq.map JsonNode.Parse |> jarray + ensure (arr rows |> List.isEmpty |> not) ("empty correction evidence: " + table) + table, rows) |> obj + let before = beliefs() + restart() + ensure (JsonNode.DeepEquals(before, beliefs())) "corrected history changed across immediate PostgreSQL restart" + let counts = before.AsObject() |> Seq.map (fun item -> item.Key, jint (arr item.Value |> List.length)) |> Seq.toList |> obj + correction.AsObject().Add("persistedRows", counts) + correction.AsObject().Add("rowsSha256", jstr (shaText (before.ToJsonString()))) + writeJson (Path.Combine(output, "corrected-history.json")) before + postgres.AsObject().Add("correctionRecovery", correction) + report.AsObject().Add("postgresql", postgres) + finally + if File.Exists(Path.Combine(data, "postmaster.pid")) then stopServer() + if File.Exists serverLog then File.Copy(serverLog, Path.Combine(output, "postgres-server.log"), true) + report.AsObject().Add("status", jstr "passed") + let harnessFiles = + ["Program.fs", Path.Combine(providers, "Program.fs") + "packages.lock.json", Path.Combine(providers, "packages.lock.json") + "Providers.fs", Path.Combine(__SOURCE_DIRECTORY__, "Providers.fs") + "Common.fs", Path.Combine(__SOURCE_DIRECTORY__, "Common.fs")] + report.AsObject().Add("harnessSha256", obj (harnessFiles |> List.map (fun (name,file) -> name, jstr (shaFile file)))) + writeJson (Path.Combine(output, "report.json")) report + printfn "%s" (report.ToJsonString(jsonOptions)) diff --git a/eng/Qualification/Qualification.fsproj b/eng/Qualification/Qualification.fsproj new file mode 100644 index 0000000..40deaca --- /dev/null +++ b/eng/Qualification/Qualification.fsproj @@ -0,0 +1,18 @@ + + + Exe + net10.0 + false + + + + + + + + + + + + + diff --git a/eng/Qualification/README.md b/eng/Qualification/README.md new file mode 100644 index 0000000..29cde6b --- /dev/null +++ b/eng/Qualification/README.md @@ -0,0 +1,29 @@ +# F# qualification commands + +Run from the repository root with SDK 10.0.401: + +```sh +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- selftest +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- replay +``` + +`replay` restores a locked external consumer, checks package and source identities, +then runs the Automata conformance examples. With `QUINT_BIN` and `QUINT_HOME` set, it +also runs `generate` and the pinned model checks. `generate --write` adds reviewed new +fixtures; it refuses changed semantics for an existing regression fixture. + +`providers-provision DEST` builds pinned PostgreSQL and extensions in a new private +destination. `providers-check SOURCE POSTGRES_BIN` runs the provider contracts and +crash/restart witnesses. The [provider guide](../../examples/AutomataProviders/README.md) +has the prerequisite and capability details. + +`readback VERSION [COMMIT]` checks published FsQuint packages against the release +source tag and qualified archive payloads. The release workflow supplies credentials +for the GitHub package feed. `selftest` exercises the same F# archive and nuspec +readers against malformed members, identities and source tags without contacting a +package feed. The release workflow runs it before readback. + +The project uses only the repository's .NET SDK and pinned FSharp.Core. Shell scripts +remain for tool download, packing and CI entry points; FsQuint qualification and release +do not need a Python runtime. The separately installed work-roadmap skill retains its +own Python helpers. diff --git a/eng/Qualification/Readback.fs b/eng/Qualification/Readback.fs new file mode 100644 index 0000000..d136bee --- /dev/null +++ b/eng/Qualification/Readback.fs @@ -0,0 +1,98 @@ +namespace FsQuint.Qualification + +open System +open System.IO +open System.IO.Compression +open System.Net +open System.Net.Http +open System.Net.Http.Headers +open System.Text +open System.Text.RegularExpressions +open System.Text.Json.Nodes +open System.Threading +open System.Xml +open System.Xml.Linq +open FsQuint.Qualification.Common + +module Readback = + let tagCommit version repository = + let tag = sprintf "refs/tags/v%s^{commit}" version + let value = runCommand "git" ["rev-parse"; "--verify"; "--end-of-options"; tag] repository [] 30 |> fun s -> s.Trim() + ensure (Regex.IsMatch(value, "^[0-9a-f]{40}$")) "source tag commit is unavailable" + value + + let inspectNuspec path package version commit = + NuspecIdentity.verify path package version commit |> ignore + + let downloaded (client: HttpClient) (url: string) authorization = + let origin = Uri url + let rec get (current: Uri) redirects = + ensure (redirects <= 5) "too many package redirects" + use request = new HttpRequestMessage(HttpMethod.Get, current) + request.Headers.UserAgent.ParseAdd("FsQuint-Qualification/1.0") + if current.Authority = origin.Authority then + match authorization with Some value -> request.Headers.Authorization <- AuthenticationHeaderValue("Basic", value) | None -> () + use response = client.Send(request) + if int response.StatusCode >= 300 && int response.StatusCode < 400 then + let target = response.Headers.Location + ensure (not (isNull target)) "package redirect has no target" + let redirected = Uri(current, target) + ensure (redirected.Scheme = Uri.UriSchemeHttps) "insecure package redirect" + get redirected (redirects + 1) + elif response.StatusCode = HttpStatusCode.NotFound then None + else + response.EnsureSuccessStatusCode() |> ignore + Some(response.Content.ReadAsByteArrayAsync().Result) + get origin 0 + + let run (version: string) (suppliedCommit: string option) = + ensure (Regex.IsMatch(version, "^[0-9]+\\.[0-9]+\\.[0-9]+(?:-[A-Za-z0-9.-]+)?$")) "Invalid package version" + let commit = tagCommit version root + let requested = defaultArg suppliedCommit (Environment.GetEnvironmentVariable "GITHUB_SHA") + if not (String.IsNullOrWhiteSpace requested) then ensure (requested = commit) "supplied commit differs from source tag" + let checkTag () = ensure (tagCommit version root = commit) "source tag moved during readback" + let output = Path.Combine(root, "artifacts/readback") + Directory.CreateDirectory output |> ignore + let receipts = JsonObject() + use handler = new HttpClientHandler(AllowAutoRedirect = false) + use client = new HttpClient(handler, Timeout = TimeSpan.FromSeconds 30.) + for package in ["FsQuint"; "FsQuint.Tooling"] do + let name = package.ToLowerInvariant() + let local = Path.Combine(root, "artifacts/packages", sprintf "%s.%s.nupkg" package version) + let mutable expected = if File.Exists local then Some(ArchiveFingerprint.inspect local) else None + for feed in ["github"; "nuget"] do + checkTag() + let url = + if feed = "github" then sprintf "https://nuget.pkg.github.com/FS-GG/download/%s/%s/%s.%s.nupkg" name version name version + else sprintf "https://api.nuget.org/v3-flatcontainer/%s/%s/%s.%s.nupkg" name version name version + let authorization = + if feed = "github" then + let actor = Environment.GetEnvironmentVariable "GITHUB_ACTOR" + let token = Environment.GetEnvironmentVariable "GH_TOKEN" + ensure (not (String.IsNullOrWhiteSpace actor) && not (String.IsNullOrWhiteSpace token)) "GitHub readback credentials missing" + Some(Convert.ToBase64String(Encoding.UTF8.GetBytes(actor + ":" + token))) + else None + let mutable content = None + let mutable attempt = 0 + while content.IsNone && attempt < 120 do + content <- downloaded client url authorization + attempt <- attempt + 1 + if content.IsNone && attempt < 120 then + if attempt % 6 = 1 then printfn "%s: %s has not exposed the download yet; retrying" package feed + Thread.Sleep 10000 + ensure content.IsSome (sprintf "%s: %s package is unavailable" package feed) + checkTag() + let bytes = content.Value + let target = Path.Combine(output, sprintf "%s.%s.nupkg" name feed) + File.WriteAllBytes(target, bytes) + let actual = ArchiveFingerprint.inspect target + inspectNuspec target package version commit + match expected with + | Some qualified -> + ensure ((qualified |> List.map (fun m -> m.Name,m.Sha256)) = (actual |> List.map (fun m -> m.Name,m.Sha256))) (sprintf "%s: %s differs from qualified payload" package feed) + | None -> expected <- Some actual + let members = actual |> List.map (fun m -> m.Name, jstr m.Sha256) + receipts.Add(package + ":" + feed, obj ["archiveSha256", jstr (shaBytes bytes); "payloads", obj members]) + checkTag() + writeJson (Path.Combine(output, "receipt.json")) receipts + printfn "Both package payloads match both feeds." diff --git a/eng/Qualification/Replay.fs b/eng/Qualification/Replay.fs new file mode 100644 index 0000000..7a22b83 --- /dev/null +++ b/eng/Qualification/Replay.fs @@ -0,0 +1,82 @@ +namespace FsQuint.Qualification + +open System +open System.IO +open System.IO.Compression +open System.Text.Json.Nodes +open System.Xml.Linq +open FsQuint.Qualification.Common + +module Replay = + let private copyFile source destination = File.Copy(source, destination, true) + let private copyTree source destination = + Directory.CreateDirectory destination |> ignore + for file in Directory.GetFiles(source, "*", SearchOption.AllDirectories) do + let target = Path.Combine(destination, Path.GetRelativePath(source, file)) + Directory.CreateDirectory(Path.GetDirectoryName target) |> ignore + copyFile file target + + let run () = + let baseline = read (Path.Combine(replay, "baseline.json")) + use scratch = new Temporary("fsquint-automata-") + let target = scratch.Path + for name in ["AutomataReplay.fsproj"; "baseline.json"; "packages.lock.json"] do + copyFile (Path.Combine(replay, name)) (Path.Combine(target, name)) + for pattern in ["*.fs"; "*.qnt"] do + for file in Directory.GetFiles(replay, pattern) do + copyFile file (Path.Combine(target, Path.GetFileName file)) + copyTree (Path.Combine(replay, "fixtures")) (Path.Combine(target, "fixtures")) + copyFile (Path.Combine(root, "examples/Shared/PureReplay.fs")) (Path.Combine(target, "PureReplay.fs")) + for name in ["global.json"; "NuGet.Config"] do copyFile (Path.Combine(root, name)) (Path.Combine(target, name)) + let environment = ["NUGET_PACKAGES", Some(Path.Combine(target, "packages")); "NUGET_HTTP_CACHE_PATH", Some(Path.Combine(target, "http"))] + let restore = ["restore"; "AutomataReplay.fsproj"; "--source"; Path.Combine(root, "artifacts/packages"); "--source"; "https://api.nuget.org/v3/index.json"] + let oldLock = read (Path.Combine(target, "packages.lock.json")) + runCommand "dotnet" (restore @ ["--force-evaluate"]) target environment 180 |> ignore + let refreshed = read (Path.Combine(target, "packages.lock.json")) + prop (prop (prop oldLock "dependencies") "net10.0") "FsQuint" |> fun p -> p.AsObject().["contentHash"] <- jstr (str (prop (prop (prop (prop refreshed "dependencies") "net10.0") "FsQuint") "contentHash")) + ensure (JsonNode.DeepEquals(oldLock, refreshed)) "Dependency lock changed beyond the candidate FsQuint content hash" + let candidate = Path.Combine(root, "artifacts/packages/FsQuint.0.1.1.nupkg") + let restored = Path.Combine(target, "packages/fsquint/0.1.1/fsquint.0.1.1.nupkg") + ensure (shaFile restored = shaFile candidate) "Consumer did not restore the exact candidate FsQuint package" + runCommand "dotnet" (restore @ ["--locked-mode"]) target environment 180 |> ignore + let checkPin (pin: JsonNode) = + let id = str (prop pin "id") + let version = str (prop pin "version") + let name = id.ToLowerInvariant() + let archive = Path.Combine(target, "packages", name, version, sprintf "%s.%s.nupkg" name version) + ensure (shaFile archive = str (prop pin "sha256")) ("Package provenance mismatch: " + id) + archive + let core = obj ["id", prop baseline "packageId"; "version", prop baseline "packageVersion"; "sha256", prop baseline "packageSha256"] + let archive = checkPin core + for pin in arr (prop baseline "additionalPackages") do checkPin pin |> ignore + use zip = ZipFile.OpenRead archive + let nuspec = zip.Entries |> Seq.find (fun e -> e.FullName.EndsWith(".nuspec", StringComparison.Ordinal)) + use stream = nuspec.Open() + let xml = XDocument.Load stream + let metadata = xml.Root.Elements() |> Seq.find (fun e -> e.Name.LocalName = "metadata") + let element name = metadata.Elements() |> Seq.find (fun e -> e.Name.LocalName = name) + for name, expected in ["id", str (prop baseline "packageId"); "version", str (prop baseline "packageVersion"); "license", str (prop baseline "licenseExpression")] do + ensure ((element name).Value = expected) ("Unexpected package " + name) + let repository = element "repository" + ensure (repository.Attribute(XName.Get "url").Value = str (prop baseline "repository") && repository.Attribute(XName.Get "commit").Value = str (prop baseline "repositoryCommit")) "Unexpected package source provenance" + let execution = runCommand "dotnet" ["run"; "--project"; "AutomataReplay.fsproj"; "-c"; "Release"; "--no-restore"] target environment 120 + Console.Write execution + let failures = execution.Split('\n') |> Array.choose (fun line -> if line.StartsWith("DIVERGENCE ") then Some(JsonNode.Parse(line.Substring(11))) else None) + ensure (failures.Length = 4) "Missing approval mutation diagnostics" + writeJson (Path.Combine(root, "artifacts/automata-replay.json")) (obj ["schema", jstr "fsquint.replay-evidence/1"; "outcome", jstr "passed"; "mutationDiagnostics", JsonArray(failures) :> JsonNode]) + printfn "PASS: isolated locked restore and package archive/source/license provenance." + match Environment.GetEnvironmentVariable "QUINT_BIN" with + | null | "" -> printfn "Model execution not requested; offline fixture replay qualified above." + | quint -> + ensure (shaFile quint = str (prop baseline "quintSha256")) "Quint executable differs from the qualified pin" + Generation.run false + let cases = + [ ["typecheck"; "approval.qnt"]; ["typecheck"; "turnstile.qnt"] + ["run"; "correction.qnt"; "--invariant"; "safety"; "--seed"; "42"; "--max-samples"; "1000"; "--max-steps"; "10"; "--verbosity"; "1"] + ["run"; "protocol.qnt"; "--invariant"; "safety"; "--seed"; "42"; "--max-samples"; "1000"; "--max-steps"; "10"; "--verbosity"; "1"] + ["test"; "turnstile_test.qnt"; "--seed"; "42"]; ["typecheck"; "resolver.qnt"]; ["test"; "resolver_test.qnt"; "--seed"; "42"] + ["run"; "resolver.qnt"; "--invariant"; "safety"; "--seed"; "42"; "--max-samples"; "1000"; "--max-steps"; "10"; "--verbosity"; "1"] + ["test"; "approval_test.qnt"; "--seed"; "42"] + ["run"; "approval.qnt"; "--invariant"; "safety"; "--seed"; "42"; "--max-samples"; "1000"; "--max-steps"; "30"; "--verbosity"; "1"] + ["run"; "approval.qnt"; "--invariant"; "transitionSafety"; "--seed"; "42"; "--max-samples"; "1000"; "--max-steps"; "30"; "--verbosity"; "1"] ] + for args in cases do runCommand quint args replay [] 120 |> ignore diff --git a/eng/Qualification/SelfTest.fs b/eng/Qualification/SelfTest.fs new file mode 100644 index 0000000..b3d8e70 --- /dev/null +++ b/eng/Qualification/SelfTest.fs @@ -0,0 +1,119 @@ +namespace FsQuint.Qualification + +open System +open System.IO +open System.IO.Compression +open System.Net +open System.Net.Http +open System.Threading +open System.Threading.Tasks +open FsQuint.Qualification.Common + +module SelfTest = + type private MockHandler(answer: HttpRequestMessage -> HttpResponseMessage) = + inherit HttpMessageHandler() + override _.Send(request, _) = answer request + override _.SendAsync(request, _) = Task.FromResult(answer request) + let private archive file entries = + use zip = ZipFile.Open(file, ZipArchiveMode.Create) + for name, bytes, mode in entries do + let item = zip.CreateEntry(name) + item.ExternalAttributes <- mode <<< 16 + use stream = item.Open() + stream.Write(bytes, 0, bytes.Length) + file + let private member' (name: string) = name, System.Text.Encoding.UTF8.GetBytes name, 0o100644 + let private rejected label thunk = + let mutable refused = false + try thunk() with _ -> refused <- true + ensure refused ("accepted invalid " + label) + let private goodXml commit = sprintf "FsQuint0.1.0" commit + let run () = + use temporary = new Temporary("fsquint-readback-selftest-") + let file name entries = archive (Path.Combine(temporary.Path, name + ".nupkg")) entries + let valid = file "valid" [member' "README.md"; member' "LICENSE.txt"] + ensure (ArchiveFingerprint.inspect valid |> List.length = 2) "valid package rejected" + let duplicate = file "duplicate" [member' "README.md"; member' "README.md"] + rejected "duplicate ZIP member" (fun () -> ArchiveFingerprint.inspect duplicate |> ignore) + let badMembers = + ["root-case", ["README.md"; "readme.md"] + "nested-case", ["README.md"; "Docs/Guide.md"; "docs/guide.md"] + "directory-case", ["README.md"; "Folder/"; "folder/"] + "signature-case", ["README.md"; ".signature.p7s"; ".SIGNATURE.P7S"] + "parent", ["README.md"; "../outside"] + "absolute", ["README.md"; "/outside"] + "dot", ["README.md"; "docs/./file"] + "backslash", ["README.md"; "docs\\file"] + "colon", ["README.md"; "C:drive"] + "empty-segment", ["README.md"; "docs//file"] + "blank", ["README.md"; " "]] + for label, names in badMembers do + let path = file label (names |> List.map member') + rejected label (fun () -> ArchiveFingerprint.inspect path |> ignore) + for label, entries in + ["empty", [] + "signature-only", [member' ".signature.p7s"] + "directory-only", ["docs/", [||], 0o040755] + "symlink-payload", ["README.md", [|1uy|], 0o120777] + "symlink-signature", [member' "README.md"; ".signature.p7s", [|1uy|], 0o120777]] do + rejected label (fun () -> ArchiveFingerprint.inspect (file label entries) |> ignore) + let signed = file "signed" [member' "README.md"; member' ".signature.p7s"] + ensure ((ArchiveFingerprint.inspect signed |> List.map _.Name) = ["README.md"]) "signature altered payload set" + let executable = file "executable" ["README.md", System.Text.Encoding.UTF8.GetBytes "README.md", 0o100755; member' "LICENSE.txt"] + ArchiveFingerprint.compare valid executable + let nestedSignature = file "nested-signature" [member' "README.md"; member' "LICENSE.txt"; member' "nested/.signature.p7s"] + rejected "nested signature" (fun () -> ArchiveFingerprint.compare valid nestedSignature) + let changed = file "changed" ["README.md", [|1uy|], 0o100644; member' "LICENSE.txt"] + rejected "changed payload" (fun () -> ArchiveFingerprint.compare valid changed) + let commit = String.replicate 40 "a" + let xmlBytes (value: string) = System.Text.Encoding.UTF8.GetBytes value + let makeSpec label xml names = file label (("FsQuint.nuspec", xmlBytes xml, 0o100644) :: (names |> List.map member')) + let spec = makeSpec "spec-valid" (goodXml commit) ["lib/a.dll"] + Readback.inspectNuspec spec "FsQuint" "0.1.0" commit + let namespaceXml = (goodXml commit).Replace("", "") + Readback.inspectNuspec (makeSpec "spec-namespace" namespaceXml ["lib/a.dll"]) "FsQuint" "0.1.0" commit + for label, xml in + ["wrong-id", (goodXml commit).Replace("FsQuint", "Foreign") + "wrong-version", (goodXml commit).Replace("0.1.0", "0.2.0") + "wrong-commit", (goodXml commit).Replace(commit, String.replicate 40 "b") + "wrong-root", (goodXml commit).Replace("", "").Replace("", "") + "two-id", (goodXml commit).Replace("FsQuint", "FsQuintFsQuint") + "two-metadata", (goodXml commit).Replace("", "FsQuint") + "two-repository", (goodXml commit).Replace("", "") + "dtd", "]>" + (goodXml commit).Replace("FsQuint", "&x;") + "malformed", ""] do + rejected label (fun () -> Readback.inspectNuspec (makeSpec label xml ["lib/a.dll"]) "FsQuint" "0.1.0" commit) + let extraSpec = file "two-specs" ["FsQuint.nuspec", xmlBytes (goodXml commit), 0o100644; member' "foreign.nuspec"; member' "lib/a.dll"] + rejected "two nuspecs" (fun () -> Readback.inspectNuspec extraSpec "FsQuint" "0.1.0" commit) + let nestedSpec = file "nested-spec" ["metadata/FsQuint.nuspec", xmlBytes (goodXml commit), 0o100644; member' "lib/a.dll"] + rejected "nested nuspec" (fun () -> Readback.inspectNuspec nestedSpec "FsQuint" "0.1.0" commit) + let repo = Path.Combine(temporary.Path, "source") + Directory.CreateDirectory repo |> ignore + let git args = runCommand "git" args repo [] 30 |> ignore + git ["init"; "-q"; "-b"; "main"] + git ["config"; "user.name"; "Fixture"] + git ["config"; "user.email"; "fixture@example.invalid"] + File.WriteAllText(Path.Combine(repo, "marker"), "source") + git ["add"; "marker"] + git ["commit"; "-qm"; "source"] + let tagged = (runCommand "git" ["rev-parse"; "HEAD"] repo [] 30).Trim() + git ["tag"; "v0.1.0"] + File.WriteAllText(Path.Combine(repo, "marker"), "foreign") + git ["commit"; "-qam"; "foreign"] + ensure (Readback.tagCommit "0.1.0" repo = tagged) "release readback selected caller head over tag" + git ["tag"; "-d"; "v0.1.0"] + rejected "missing tag" (fun () -> Readback.tagCommit "0.1.0" repo |> ignore) + let mutable firstAuthenticated, secondAuthenticated = false, true + use handler = new MockHandler(fun request -> + if request.RequestUri.Host = "origin.example" then + firstAuthenticated <- not (isNull request.Headers.Authorization) + let redirect = new HttpResponseMessage(HttpStatusCode.Redirect) + redirect.Headers.Location <- Uri("https://other.example/archive.nupkg") + redirect + else + secondAuthenticated <- not (isNull request.Headers.Authorization) + new HttpResponseMessage(HttpStatusCode.OK, Content = new ByteArrayContent([|1uy; 2uy|]))) + use client = new HttpClient(handler) + let bytes = Readback.downloaded client "https://origin.example/archive.nupkg" (Some "fixture-token") + ensure (firstAuthenticated && not secondAuthenticated && bytes.Value = [|1uy; 2uy|]) "redirect leaked package credentials" + printfn "PASS: F# readback archive, nuspec and release-tag controls." diff --git a/eng/Qualification/packages.lock.json b/eng/Qualification/packages.lock.json new file mode 100644 index 0000000..7f9bfc1 --- /dev/null +++ b/eng/Qualification/packages.lock.json @@ -0,0 +1,13 @@ +{ + "version": 1, + "dependencies": { + "net10.0": { + "FSharp.Core": { + "type": "Direct", + "requested": "[10.1.401, )", + "resolved": "10.1.401", + "contentHash": "IGqjL9U8pQl7CaCpFP3f5slZMduE8c7ZBx7HycAQ9dc1tawyniNyw7Fh6L2cShIoQDcaDL+S8/kokhWs8WwnBQ==" + } + } + } +} \ No newline at end of file diff --git a/eng/archive-fingerprint.fsx b/eng/archive-fingerprint.fsx index 3b8a9ca..f74f6b4 100644 --- a/eng/archive-fingerprint.fsx +++ b/eng/archive-fingerprint.fsx @@ -1,85 +1 @@ -// FSC-08 source primitive. This is not wired into release/readback.py. -// Cross-feed equality follows the live Python readback's 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(StringComparer.Ordinal) - let aliases = System.Collections.Generic.HashSet(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" +#load "Qualification/ArchiveFingerprint.fs" diff --git a/eng/archive-fingerprint.md b/eng/archive-fingerprint.md index 59f171f..d08215f 100644 --- a/eng/archive-fingerprint.md +++ b/eng/archive-fingerprint.md @@ -1,5 +1,7 @@ # FSC-08 archive fingerprint source pilot +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + `archive-fingerprint.fsx` is a read-only F# source primitive. It records each archive member's exact name, SHA-256 digest, and ZIP Unix mode bits. It refuses duplicate, ASCII case-alias, unsafe, or symlink member names and archives diff --git a/eng/check.sh b/eng/check.sh index 261a0a0..33ccd99 100755 --- a/eng/check.sh +++ b/eng/check.sh @@ -2,9 +2,10 @@ set -euo pipefail cd "$(dirname "$0")/.." dotnet run --project tests/FsQuint.Tests -c Release +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- selftest dotnet pack src/FsQuint/FsQuint.fsproj -c Release -o artifacts/packages dotnet pack src/FsQuint.Tooling/FsQuint.Tooling.fsproj -c Release -o artifacts/packages -python3 examples/AutomataReplay/check.py +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- replay scratch=$(mktemp -d) trap 'rm -rf "$scratch"' EXIT cp examples/BoundedQueue/{BoundedQueue.fsproj,Program.fs,queue.itf.json} "$scratch/" diff --git a/eng/nuspec-identity.md b/eng/nuspec-identity.md index a86c487..4efd623 100644 --- a/eng/nuspec-identity.md +++ b/eng/nuspec-identity.md @@ -1,5 +1,7 @@ # Provisional `.nuspec` identity source seam +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + `NuspecIdentity.fsx` checks one exact root `.nuspec` member, package ID, version, and repository commit in a local archive. It uses the archive member guard from draft #15 and stacks on packed characterization draft #16. The diff --git a/eng/packed-archive-characterization.md b/eng/packed-archive-characterization.md index d4ae490..61eb59d 100644 --- a/eng/packed-archive-characterization.md +++ b/eng/packed-archive-characterization.md @@ -1,5 +1,7 @@ # FSC-08 packed archive characterization +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + This source-only fixture is stacked on the F# archive fingerprint draft #15. It compares locally packed `.nupkg` member names, SHA-256 payload digests, and ZIP Unix mode bits against an independent Python `zipfile` enumeration. It mirrors @@ -10,14 +12,10 @@ nested signature members; a mode-only difference retains payload equality. A feed-added root `.signature.p7s` stays excluded. Repacking the same payload with different ZIP container bytes passes. -Run after locked restore, using only local files: +The live offline readback controls use the F# qualification project: ```sh -dotnet restore src/FsQuint/FsQuint.fsproj --locked-mode -dotnet restore src/FsQuint.Tooling/FsQuint.Tooling.fsproj --locked-mode -dotnet pack src/FsQuint/FsQuint.fsproj -c Release --no-restore -o /tmp/fsquint-fsc08-local-packs -dotnet pack src/FsQuint.Tooling/FsQuint.Tooling.fsproj -c Release --no-restore -o /tmp/fsquint-fsc08-local-packs -python3 eng/test-packed-archive-fingerprint.py /tmp/fsquint-fsc08-local-packs/FsQuint.0.1.0.nupkg /tmp/fsquint-fsc08-local-packs/FsQuint.Tooling.0.1.0.nupkg +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- selftest ``` The local archives carry 13 and 10 payload members respectively at this diff --git a/eng/public-example.sh b/eng/public-example.sh index 16b848a..708c36e 100755 --- a/eng/public-example.sh +++ b/eng/public-example.sh @@ -4,18 +4,10 @@ cd "$(dirname "$0")/.." scratch=$(mktemp -d) trap 'rm -rf "$scratch"' EXIT cp examples/BoundedQueue/{BoundedQueue.fsproj,Program.fs,queue.itf.json} "$scratch/" +cp examples/Shared/PureReplay.fs "$scratch/" cp global.json NuGet.Config "$scratch/" if [[ -n "${1:-}" ]]; then - python3 - "$scratch/BoundedQueue.fsproj" "$1" <<'PYTHON' -import sys -import xml.etree.ElementTree as ET -path, version = sys.argv[1:] -tree = ET.parse(path) -for package in tree.iter('PackageReference'): - if package.attrib['Include'] == 'FsQuint': - package.set('Version', version) -tree.write(path) -PYTHON + dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- set-package-version "$scratch/BoundedQueue.fsproj" "$1" fi export NUGET_PACKAGES="$scratch/packages" export NUGET_HTTP_CACHE_PATH="$scratch/http" diff --git a/eng/readback-case-alias.md b/eng/readback-case-alias.md index 43f7458..0df7f45 100644 --- a/eng/readback-case-alias.md +++ b/eng/readback-case-alias.md @@ -1,5 +1,7 @@ # FSC-08 ASCII case-alias archive guard +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + This draft rejects an archive containing two ZIP member names that differ only by ASCII letter case. Such names can refer to the same extracted path on a case-insensitive filesystem, even though both source readers previously saw diff --git a/eng/readback-commit-source.md b/eng/readback-commit-source.md index ead44ba..4ac54d6 100644 --- a/eng/readback-commit-source.md +++ b/eng/readback-commit-source.md @@ -1,5 +1,7 @@ # FSC-08 source-only expected commit selection +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + The Python readback previously trusted its optional command-line expected commit, or `GITHUB_SHA` when no argument was supplied. A caller could provide the commit recorded by the wrong served package, and two feeds with matching diff --git a/eng/readback-member-guards.md b/eng/readback-member-guards.md index b5ed7fe..17d9ff2 100644 --- a/eng/readback-member-guards.md +++ b/eng/readback-member-guards.md @@ -1,5 +1,7 @@ # FSC-08 source-only Python archive member guards +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + The live Python `eng/readback.py` computes a name-to-SHA-256 payload map for each qualified and served archive. Before this draft, its `payloads()` function accepted ZIP symlink members and unsafe names. A symlinked root diff --git a/eng/readback-mode-policy.md b/eng/readback-mode-policy.md index 9daf8f1..4d4d8aa 100644 --- a/eng/readback-mode-policy.md +++ b/eng/readback-mode-policy.md @@ -1,5 +1,7 @@ # FSC-08 source-only archive mode policy +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + Select exact archive member names and SHA-256 payload digests as the cross-feed equality contract. This is the contract documented in `docs/releases.md` and implemented by the current Python `eng/readback.py` receiver. ZIP Unix mode is diff --git a/eng/readback-nonempty-payload.md b/eng/readback-nonempty-payload.md index 5cad0b9..7394a0d 100644 --- a/eng/readback-nonempty-payload.md +++ b/eng/readback-nonempty-payload.md @@ -1,5 +1,7 @@ # FSC-08 nonempty archive payload guard +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + The Python `payloads()` projection previously returned an empty or directory-only map for archives without a regular payload member. The F# archive inspector refused those archives. An independent offline fixture diff --git a/eng/readback-nuspec-root.md b/eng/readback-nuspec-root.md index c545bae..925199c 100644 --- a/eng/readback-nuspec-root.md +++ b/eng/readback-nuspec-root.md @@ -1,5 +1,7 @@ # FSC-08 source-only `.nuspec` root selection +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + The Python release readback previously chose the first ZIP member whose name ended in `.nuspec`. A nested manifest, a foreign root manifest, or the first of two root manifests could supply the repository commit and pass readback diff --git a/eng/readback-nuspec-xml.md b/eng/readback-nuspec-xml.md index a1647d8..202d28f 100644 --- a/eng/readback-nuspec-xml.md +++ b/eng/readback-nuspec-xml.md @@ -1,5 +1,7 @@ # FSC-08 source-only `.nuspec` XML identity guard +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + The Python release readback previously parsed the served root `.nuspec` XML, selected the first descendant `repository` element, and checked only its `commit` when a caller supplied one. It could accept a wrong package ID or diff --git a/eng/readback-tag-stability.md b/eng/readback-tag-stability.md index 9d8ec5c..20fc4cf 100644 --- a/eng/readback-tag-stability.md +++ b/eng/readback-tag-stability.md @@ -1,5 +1,7 @@ # FSC-08 source-only tag stability checks +> Historical note: the Python readback experiments described here have been superseded by the F# qualification tool in [Qualification](Qualification/README.md). This document preserves the original findings. + The expected commit is selected once from `refs/tags/v^{commit}` in the preceding source draft. Before this draft, a tag could move after that selection while the readback continued to validate archives against the stale diff --git a/eng/readback.py b/eng/readback.py deleted file mode 100644 index 874a449..0000000 --- a/eng/readback.py +++ /dev/null @@ -1,159 +0,0 @@ -"""Compare served package payloads (NuGet may add a repository signature).""" -import base64 -import hashlib -import json -import re -import xml.etree.ElementTree as ET -import xml.parsers.expat as expat -import os -from pathlib import Path -import subprocess -import sys -import time -import urllib.error -import urllib.request -import zipfile -from urllib.parse import urlsplit - -class SafeRedirect(urllib.request.HTTPRedirectHandler): - def redirect_request(self, req, fp, code, msg, headers, newurl): - redirected = super().redirect_request(req, fp, code, msg, headers, newurl) - if redirected is not None and urlsplit(req.full_url).netloc != urlsplit(newurl).netloc: - redirected.remove_header("Authorization") - return redirected - -reader = urllib.request.build_opener(SafeRedirect()) - -version = sys.argv[1] -if not re.fullmatch(r"[0-9]+\.[0-9]+\.[0-9]+(?:-[A-Za-z0-9.-]+)?", version): - raise ValueError("Invalid package version") - -def select_expected_commit(version, supplied_commit, repository=None): - if not re.fullmatch(r"[0-9]+\.[0-9]+\.[0-9]+(?:-[A-Za-z0-9.-]+)?", version): - raise ValueError('Invalid package version') - tag = f'refs/tags/v{version}^{{commit}}' - result = subprocess.run( - ['git', 'rev-parse', '--verify', '--end-of-options', tag], - cwd=repository, text=True, capture_output=True, check=False, - ) - source_commit = result.stdout.strip() - if result.returncode != 0 or not re.fullmatch(r'[0-9a-f]{40}', source_commit): - raise ValueError(f'{version}: source tag commit is unavailable') - if supplied_commit is not None and supplied_commit != source_commit: - raise ValueError(f'{version}: supplied commit differs from source tag') - return source_commit - -def verify_source_tag_stable(version, selected_commit, repository=None): - current = select_expected_commit(version, None, repository) - if current != selected_commit: - raise ValueError(f'{version}: source tag moved during readback') - -expected_commit = select_expected_commit( - version, sys.argv[2] if len(sys.argv) > 2 else os.environ.get('GITHUB_SHA')) -root = Path('artifacts/readback') -root.mkdir(parents=True, exist_ok=True) - -def payloads(path): - with zipfile.ZipFile(path) as archive: - entries = archive.infolist() - names = [entry.filename for entry in entries] - if len(names) != len(set(names)): - raise ValueError('Duplicate ZIP entry') - ascii_fold = str.maketrans('ABCDEFGHIJKLMNOPQRSTUVWXYZ', 'abcdefghijklmnopqrstuvwxyz') - aliases = set() - for entry in entries: - name = entry.filename - path_part = name[:-1] if name.endswith('/') else name - if (not path_part.strip() or name.startswith('/') - or any(char in name for char in ('\\', ':', '\x00')) - or any(segment in ('', '.', '..') for segment in path_part.split('/'))): - raise ValueError(f'Unsafe ZIP entry: {name!r}') - folded = name.translate(ascii_fold) - if folded in aliases: - raise ValueError(f'Case-alias ZIP entry: {name!r}') - aliases.add(folded) - mode = (entry.external_attr >> 16) & 0xffff - if mode & 0o170000 == 0o120000: - raise ValueError(f'Symlink ZIP entry: {name!r}') - if not any(entry.filename != '.signature.p7s' and not entry.is_dir() - for entry in entries): - raise ValueError('Archive has no payload members') - return {entry.filename: hashlib.sha256(archive.read(entry)).hexdigest() - for entry in entries if entry.filename != '.signature.p7s'} - -def select_nuspec(archive, package): - expected = f'{package}.nuspec' - specs = [name for name in archive.namelist() if name.lower().endswith('.nuspec')] - if specs != [expected]: - raise ValueError(f'{package}: archive must contain one exact root nuspec') - return expected - -def verify_nuspec_xml(archive, spec, package, version, expected_commit): - body = archive.read(spec) - parser = expat.ParserCreate() - def refuse_doctype(*_): - raise ValueError(f'{package}: nuspec DTD is prohibited') - parser.StartDoctypeDeclHandler = refuse_doctype - try: - parser.Parse(body, True) - except expat.ExpatError as error: - raise ValueError(f'{package}: nuspec XML is invalid') from error - root = ET.fromstring(body) - def local_name(node): - return node.tag.rsplit('}', 1)[-1] if isinstance(node.tag, str) else None - def one(parent, name): - matches = [node for node in parent if local_name(node) == name] - if len(matches) != 1: - raise ValueError(f'{package}: nuspec must contain one {name}') - return matches[0] - if local_name(root) != 'package': - raise ValueError(f'{package}: nuspec package root is invalid') - metadata = one(root, 'metadata') - actual_id = ''.join(one(metadata, 'id').itertext()) - actual_version = ''.join(one(metadata, 'version').itertext()) - repository = one(metadata, 'repository') - if actual_id != package or actual_version != version: - raise ValueError(f'{package}: nuspec package identity differs') - if expected_commit and repository.attrib.get('commit') != expected_commit: - raise ValueError(f'{package}: source commit differs from release tag') - -receipts = {} -for package in ['FsQuint', 'FsQuint.Tooling']: - name = package.lower() - local = Path(f'artifacts/packages/{package}.{version}.nupkg') - expected = payloads(local) if local.exists() else None - for feed in ['github', 'nuget']: - verify_source_tag_stable(version, expected_commit) - url = (f'https://nuget.pkg.github.com/FS-GG/download/{name}/{version}/{name}.{version}.nupkg' - if feed == 'github' else - f'https://api.nuget.org/v3-flatcontainer/{name}/{version}/{name}.{version}.nupkg') - headers = {} - if feed == 'github': - credential = (os.environ['GITHUB_ACTOR'] + ':' + os.environ['GH_TOKEN']).encode() - headers['Authorization'] = 'Basic ' + base64.b64encode(credential).decode() - for attempt in range(120): - try: - with reader.open(urllib.request.Request(url, headers=headers), timeout=30) as response: - content = response.read() - break - except urllib.error.HTTPError as error: - if error.code != 404 or attempt == 119: - raise - if attempt % 6 == 0: - print(f"{package}: {feed} has not exposed the download yet; retrying", flush=True) - time.sleep(10) - verify_source_tag_stable(version, expected_commit) - target = root / f'{name}.{feed}.nupkg' - target.write_bytes(content) - actual = payloads(target) - with zipfile.ZipFile(target) as archive: - spec = select_nuspec(archive, package) - verify_nuspec_xml(archive, spec, package, version, expected_commit) - if expected is None: - expected = actual - if expected != actual: - raise ValueError(f'{package}: {feed} differs from qualified payload') - receipts[f'{package}:{feed}'] = {'archiveSha256': hashlib.sha256(content).hexdigest(), 'payloads': actual} -verify_source_tag_stable(version, expected_commit) -(root / 'receipt.json').write_text(json.dumps(receipts, indent=2) + '\n') -print('Both package payloads match both feeds.') diff --git a/eng/test-packed-archive-fingerprint.py b/eng/test-packed-archive-fingerprint.py deleted file mode 100644 index 8776043..0000000 --- a/eng/test-packed-archive-fingerprint.py +++ /dev/null @@ -1,128 +0,0 @@ -#!/usr/bin/env python3 -"""Offline, independent characterization over locally packed FsQuint .nupkg bytes.""" - -import copy -import hashlib -import json -from pathlib import Path -import subprocess -import sys -import tempfile -import xml.etree.ElementTree as ET -import zipfile - -ROOT = Path(__file__).resolve().parents[1] -FSX = ROOT / "eng/packed-archive-fingerprint.fsx" -passed = 0 - - -def fsharp(*args): - return subprocess.run( - ["dotnet", "fsi", str(FSX), "--", *map(str, args)], - cwd=ROOT, - text=True, - capture_output=True, - check=False, - ) - - -def python_payloads(path): - # The exact payload projection in eng/readback.py; that script's top level - # performs feed requests, so it cannot be imported into an offline fixture. - with zipfile.ZipFile(path) as archive: - names = archive.namelist() - if len(names) != len(set(names)): - raise ValueError("Duplicate ZIP entry") - return { - name: hashlib.sha256(archive.read(name)).hexdigest() - for name in names - if name != ".signature.p7s" - } - - -def rewrite(source, target, *, rename=None, change=None, mode=None, add=None): - with zipfile.ZipFile(source) as original, zipfile.ZipFile(target, "w") as output: - for info in original.infolist(): - item = copy.copy(info) - if info.filename == rename: - item.filename = "renamed/" + info.filename - if info.filename == mode: - item.external_attr = 0o100755 << 16 - body = original.read(info) - if info.filename == change: - body += b"changed" - output.writestr(item, body) - if add: - output.writestr(add, b"feed-added-signature") - - -def check(package): - global passed - with zipfile.ZipFile(package) as archive: - records = [ - { - "Name": info.filename, - "Sha256": hashlib.sha256(archive.read(info)).hexdigest(), - "UnixMode": (info.external_attr >> 16) & 0xFFFF, - } - for info in archive.infolist() - if info.filename != ".signature.p7s" - ] - records.sort(key=lambda item: item["Name"]) - specs = [info for info in archive.infolist() if info.filename.endswith(".nuspec")] - assert len(specs) == 1, (package, "expected one package identity manifest") - assert package.name.startswith(specs[0].filename.removesuffix(".nuspec") + "."), ( - package, - specs[0].filename, - ) - ET.fromstring(archive.read(specs[0])) - target_member = next(info.filename for info in archive.infolist() if info.filename == "README.md") - spec_member = specs[0].filename - - result = fsharp("inspect", package) - assert result.returncode == 0, (package, result.stderr) - assert json.loads(result.stdout) == records, (package, result.stdout) - passed += 1 - - with tempfile.TemporaryDirectory(prefix="fsquint-packed-characterization-") as folder: - temporary = Path(folder) - - def expect(label, expected, **changes): - global passed - served = temporary / (label + ".nupkg") - rewrite(package, served, **changes) - actual = fsharp("compare", package, served) - if expected is None: - assert actual.returncode == 0 and actual.stdout.strip() == "match", (label, actual.stderr) - assert python_payloads(package) == python_payloads(served), label - else: - assert actual.returncode == 2 and expected in actual.stderr, (label, actual.stderr) - passed += 1 - return served - - expect("repacked-copy", None) - expect("root-signature", None, add=".signature.p7s") - expect("nested-signature", "archive members differ", add="nested/.signature.p7s") - expect("wrong-member", "archive members differ", rename=target_member) - expect("wrong-digest", "digest differs", change=target_member) - expect("wrong-nuspec", "digest differs", change=spec_member) - changed_mode = expect("wrong-mode", None, mode=target_member) - # The receiver contract compares names and payload digests. Mode is - # retained in inspection evidence, but not cross-feed equality. - assert python_payloads(package) == python_payloads(changed_mode) - passed += 1 - - print(f"{package.name}: {len(records)} exact payload members characterized") - - -def main(): - packages = [Path(value).resolve() for value in sys.argv[1:]] - if len(packages) != 2 or any(not path.is_file() or path.suffix != ".nupkg" for path in packages): - raise SystemExit("usage: test-packed-archive-fingerprint.py FsQuint.nupkg FsQuint.Tooling.nupkg") - for package in packages: - check(package) - print(f"packed archive fingerprint: {passed} offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-case-alias.py b/eng/test-readback-case-alias.py deleted file mode 100644 index c015838..0000000 --- a/eng/test-readback-case-alias.py +++ /dev/null @@ -1,81 +0,0 @@ -#!/usr/bin/env python3 -"""Offline ASCII case-alias controls for both archive readers.""" - -import ast -import hashlib -from pathlib import Path -import subprocess -import tempfile -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/packed-archive-fingerprint.fsx" - - -def python_payloads(path): - # Run the real function without the module's feed and receipt side effects. - tree = ast.parse(READBACK.read_text()) - definition = next(node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name == "payloads") - scope = {"hashlib": hashlib, "zipfile": zipfile} - exec(compile(ast.Module(body=[definition], type_ignores=[]), str(READBACK), "exec"), scope) - return scope["payloads"](path) - - -def make_archive(path, names): - with zipfile.ZipFile(path, "w") as archive: - for name in names: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = (0o040755 if name.endswith("/") else 0o100644) << 16 - archive.writestr(info, b"" if name.endswith("/") else name.encode()) - return path - - -def fsharp(path): - return subprocess.run( - ["dotnet", "fsi", str(FSX), "--", "inspect", str(path)], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - - -def expect_alias_refusal(path): - errors = [] - try: - python_payloads(path) - except ValueError as error: - if "Case-alias ZIP entry" not in str(error): - errors.append(f"Python wrong refusal: {error}") - else: - errors.append(f"Python accepted {path.name}") - result = fsharp(path) - if result.returncode != 2 or "case-alias archive member" not in result.stderr: - errors.append(f"F# accepted or misclassified {path.name}: {result.stderr}") - return errors - - -def main(): - with tempfile.TemporaryDirectory(prefix="fsquint-case-alias-") as folder: - temp = Path(folder) - valid = make_archive(temp / "valid.nupkg", ["README.md", "LICENSE.txt", "docs/a.md", "docs/b.md"]) - assert len(python_payloads(valid)) == 4 - assert fsharp(valid).returncode == 0 - - cases = [ - ("root", ["README.md", "readme.md"]), - ("nested", ["README.md", "Docs/Guide.md", "docs/guide.md"]), - ("directory", ["README.md", "Folder/", "folder/"]), - ("signature", ["README.md", ".signature.p7s", ".SIGNATURE.P7S"]), - ] - missed = [] - for label, names in cases: - archive = make_archive(temp / f"{label}.nupkg", names) - missed.extend(expect_alias_refusal(archive)) - assert not missed, "\n".join(missed) - - print("readback case aliases: 5 offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-commit-source.py b/eng/test-readback-commit-source.py deleted file mode 100644 index e8b1a1a..0000000 --- a/eng/test-readback-commit-source.py +++ /dev/null @@ -1,148 +0,0 @@ -#!/usr/bin/env python3 -"""Offline expected-commit authority controls over readback source selection.""" - -import ast -import hashlib -import os -from pathlib import Path -import re -import subprocess -import sys -import tempfile -from types import SimpleNamespace -import xml.etree.ElementTree as ET -import xml.parsers.expat as expat -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/nuspec-root-inspect.fsx" -PACKAGE = "FsQuint" -VERSION = "0.1.0" - - -def readback_source(): - # Extract only pure helpers and the actual expected_commit assignment. - # Importing the module would fetch feeds and write a receipt. - tree = ast.parse(READBACK.read_text()) - helpers = [node for node in tree.body if isinstance(node, ast.FunctionDef) - and node.name in ("payloads", "select_nuspec", "verify_nuspec_xml", "select_expected_commit")] - assignments = [node for node in tree.body if isinstance(node, ast.Assign) - and any(isinstance(target, ast.Name) and target.id == "expected_commit" for target in node.targets)] - assert len(assignments) == 1, "readback must select one expected commit" - scope = {"hashlib": hashlib, "zipfile": zipfile, "ET": ET, "expat": expat, - "subprocess": subprocess, "re": re} - exec(compile(ast.Module(body=helpers, type_ignores=[]), str(READBACK), "exec"), scope) - expression = compile(ast.Expression(assignments[0].value), str(READBACK), "eval") - - def select(version, supplied, github_sha, repository): - args = [str(READBACK), version] + ([supplied] if supplied is not None else []) - context = dict(scope, version=version, sys=SimpleNamespace(argv=args), - os=SimpleNamespace(environ={"GITHUB_SHA": github_sha} if github_sha is not None else {})) - original = Path.cwd() - try: - os.chdir(repository) - return eval(expression, context) - finally: - os.chdir(original) - - return scope, select - - -def git(repository, *args): - result = subprocess.run(["git", *args], cwd=repository, text=True, - capture_output=True, check=True) - return result.stdout.strip() - - -def archive(path, commit): - xml = (f'{PACKAGE}{VERSION}' - f'').encode() - with zipfile.ZipFile(path, "w") as packed: - for name, body in [("FsQuint.nuspec", xml), ("lib/a.dll", b"payload")]: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = 0o100644 << 16 - packed.writestr(info, body) - return path - - -def fsharp_refuses(path, expected): - result = subprocess.run( - ["dotnet", "fsi", str(FSX), "--", str(path), PACKAGE, VERSION, expected], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - assert result.returncode == 2 and "nuspec" in result.stderr, result.stderr - - -def main(): - helpers, select = readback_source() - with tempfile.TemporaryDirectory(prefix="fsquint-commit-source-") as folder: - temp = Path(folder) - repo = temp / "source" - repo.mkdir() - git(repo, "init", "-q", "-b", "main") - git(repo, "config", "user.name", "Fixture") - git(repo, "config", "user.email", "fixture@example.invalid") - marker = repo / "marker.txt" - marker.write_text("release source\n") - git(repo, "add", "marker.txt") - git(repo, "commit", "-qm", "release source") - source_commit = git(repo, "rev-parse", "HEAD") - git(repo, "tag", "v0.1.0") - marker.write_text("foreign source\n") - git(repo, "commit", "-qam", "foreign source") - foreign_commit = git(repo, "rev-parse", "HEAD") - assert source_commit != foreign_commit - - wrong_one = archive(temp / "github.nupkg", foreign_commit) - wrong_two = archive(temp / "nuget.nupkg", foreign_commit) - assert helpers["payloads"](wrong_one) == helpers["payloads"](wrong_two) - with zipfile.ZipFile(wrong_one) as packed: - spec = helpers["select_nuspec"](packed, PACKAGE) - helpers["verify_nuspec_xml"](packed, spec, PACKAGE, VERSION, foreign_commit) - fsharp_refuses(wrong_one, source_commit) - - missed = [] - try: - chosen = select(VERSION, foreign_commit, foreign_commit, repo) - except ValueError as error: - assert "source tag" in str(error), str(error) - else: - missed.append(f"caller-selected foreign commit {chosen}") - - chosen = select(VERSION, source_commit, foreign_commit, repo) - assert chosen == source_commit, "recovery CLI commit must match source tag" - chosen = select(VERSION, None, source_commit, repo) - assert chosen == source_commit, "tag-push event commit must match source tag" - chosen = select(VERSION, None, None, repo) - if chosen != source_commit: - missed.append("missing caller commit disabled source identity check") - with zipfile.ZipFile(wrong_one) as packed: - spec = helpers["select_nuspec"](packed, PACKAGE) - try: - helpers["verify_nuspec_xml"](packed, spec, PACKAGE, VERSION, chosen) - except ValueError as error: - assert "source commit differs" in str(error), str(error) - else: - missed.append("foreign archive passed tag-selected commit") - correct = archive(temp / "correct.nupkg", source_commit) - with zipfile.ZipFile(correct) as packed: - spec = helpers["select_nuspec"](packed, PACKAGE) - helpers["verify_nuspec_xml"](packed, spec, PACKAGE, VERSION, chosen) - - git(repo, "tag", "-d", "v0.1.0") - try: - chosen = select(VERSION, source_commit, None, repo) - except ValueError as error: - assert "source tag" in str(error), str(error) - else: - missed.append(f"missing source tag accepted {chosen}") - assert not missed, "\n".join(missed) - - print("readback commit source: 7 offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-member-guards.py b/eng/test-readback-member-guards.py deleted file mode 100644 index 2dba4ab..0000000 --- a/eng/test-readback-member-guards.py +++ /dev/null @@ -1,95 +0,0 @@ -#!/usr/bin/env python3 -"""Offline guard controls over the real Python readback payload function.""" - -import ast -import hashlib -from pathlib import Path -import subprocess -import tempfile -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/packed-archive-fingerprint.fsx" - - -def receiver_payloads(path): - # Importing readback.py would fetch feeds and write a receipt. - tree = ast.parse(READBACK.read_text()) - definition = next(node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name == "payloads") - scope = {"hashlib": hashlib, "zipfile": zipfile} - exec(compile(ast.Module(body=[definition], type_ignores=[]), str(READBACK), "exec"), scope) - return scope["payloads"](path) - - -def make_archive(path, members): - with zipfile.ZipFile(path, "w") as archive: - for name, body, mode in members: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = mode << 16 - archive.writestr(info, body) - return path - - -def fsharp_refuses(path, reason): - result = subprocess.run( - ["dotnet", "fsi", str(FSX), "--", "inspect", str(path)], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - assert result.returncode == 2 and reason in result.stderr, result.stderr - - -def receiver_refuses(path, reason): - try: - receiver_payloads(path) - except ValueError as error: - assert reason in str(error), str(error) - else: - raise AssertionError(f"Python receiver accepted {path.name}") - - -def main(): - with tempfile.TemporaryDirectory(prefix="fsquint-member-guards-") as folder: - temp = Path(folder) - regular = make_archive(temp / "regular.nupkg", [("README.md", b"same", 0o100644)]) - executable = make_archive(temp / "executable.nupkg", [("README.md", b"same", 0o100755)]) - assert receiver_payloads(regular) == receiver_payloads(executable) - signature = make_archive(temp / "signature.nupkg", [ - ("README.md", b"same", 0o100644), (".signature.p7s", b"feed", 0o100644) - ]) - assert receiver_payloads(regular) == receiver_payloads(signature) - - cases = [ - ("symlink-payload", "README.md", 0o120777, "Symlink ZIP entry", "symlink archive member"), - ("symlink-signature", ".signature.p7s", 0o120777, "Symlink ZIP entry", "symlink archive member"), - ("parent", "../outside", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ("absolute", "/outside", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ("dot", "docs/./file", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ("backslash", "docs\\file", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ("colon", "C:drive", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ("empty-segment", "docs//file", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ("blank", " ", 0o100644, "Unsafe ZIP entry", "unsafe archive member"), - ] - missed = [] - for label, name, mode, python_reason, fsharp_reason in cases: - members = [("README.md", b"same", 0o100644)] - if label == "symlink-payload": - members = [(name, b"same", mode)] - else: - members.append((name, b"same", mode)) - archive = make_archive(temp / f"{label}.nupkg", members) - fsharp_refuses(archive, fsharp_reason) - try: - receiver_refuses(archive, python_reason) - except AssertionError as error: - missed.append(str(error)) - - assert not missed, "\n".join(missed) - - print("readback member guards: 11 offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-mode-policy.py b/eng/test-readback-mode-policy.py deleted file mode 100644 index d8fb4b8..0000000 --- a/eng/test-readback-mode-policy.py +++ /dev/null @@ -1,72 +0,0 @@ -#!/usr/bin/env python3 -"""Offline comparison of the Python readback projection and F# candidate.""" - -import ast -import hashlib -from pathlib import Path -import subprocess -import tempfile -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/packed-archive-fingerprint.fsx" - - -def live_payloads(path): - # Extract only the real receiver function; importing readback.py runs feed IO. - tree = ast.parse(READBACK.read_text()) - definition = next(node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name == "payloads") - scope = {"hashlib": hashlib, "zipfile": zipfile} - exec(compile(ast.Module(body=[definition], type_ignores=[]), str(READBACK), "exec"), scope) - return scope["payloads"](path) - - -def make_archive(path, members): - with zipfile.ZipFile(path, "w") as archive: - for name, body, mode in members: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = mode << 16 - archive.writestr(info, body) - return path - - -def compare(source, served, *, accept, reason=""): - result = subprocess.run( - ["dotnet", "fsi", str(FSX), "--", "compare", str(source), str(served)], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - if accept: - assert result.returncode == 0 and result.stdout.strip() == "match", result.stderr - else: - assert result.returncode == 2 and reason in result.stderr, result.stderr - - -def main(): - with tempfile.TemporaryDirectory(prefix="fsquint-mode-policy-") as folder: - temp = Path(folder) - source = make_archive(temp / "source.nupkg", [("README.md", b"same", 0o100644)]) - mode_only = make_archive(temp / "mode.nupkg", [("README.md", b"same", 0o100755)]) - digest = make_archive(temp / "digest.nupkg", [("README.md", b"changed", 0o100644)]) - name = make_archive(temp / "name.nupkg", [("OTHER.md", b"same", 0o100644)]) - signature = make_archive(temp / "signature.nupkg", [ - ("README.md", b"same", 0o100644), (".signature.p7s", b"feed", 0o100644) - ]) - symlink = make_archive(temp / "symlink.nupkg", [("README.md", b"same", 0o120777)]) - - assert live_payloads(source) == live_payloads(mode_only) - compare(source, mode_only, accept=True) - assert live_payloads(source) != live_payloads(digest) - compare(source, digest, accept=False, reason="digest differs") - assert live_payloads(source) != live_payloads(name) - compare(source, name, accept=False, reason="archive members differ") - assert live_payloads(source) == live_payloads(signature) - compare(source, signature, accept=True) - compare(source, symlink, accept=False, reason="symlink archive member") - print("readback mode policy: 5 offline comparisons passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-nonempty-payload.py b/eng/test-readback-nonempty-payload.py deleted file mode 100644 index 4bf1427..0000000 --- a/eng/test-readback-nonempty-payload.py +++ /dev/null @@ -1,82 +0,0 @@ -#!/usr/bin/env python3 -"""Offline no-payload archive controls for Python and F# readers.""" - -import ast -import hashlib -from pathlib import Path -import subprocess -import tempfile -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/packed-archive-fingerprint.fsx" - - -def python_payloads(path): - # Importing readback.py would fetch feeds and write a receipt. - tree = ast.parse(READBACK.read_text()) - definition = next(node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name == "payloads") - scope = {"hashlib": hashlib, "zipfile": zipfile} - exec(compile(ast.Module(body=[definition], type_ignores=[]), str(READBACK), "exec"), scope) - return scope["payloads"](path) - - -def make_archive(path, members): - with zipfile.ZipFile(path, "w") as packed: - for name, body in members: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = (0o040755 if name.endswith("/") else 0o100644) << 16 - packed.writestr(info, body) - return path - - -def fsharp(path, accept): - result = subprocess.run( - ["dotnet", "fsi", str(FSX), "--", "inspect", str(path)], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - if accept: - assert result.returncode == 0 and "README.md" in result.stdout, result.stderr - else: - assert result.returncode == 2 and "no payload members" in result.stderr, result.stderr - - -def main(): - with tempfile.TemporaryDirectory(prefix="fsquint-nonempty-payload-") as folder: - temp = Path(folder) - good = [ - ("file", [("README.md", b"payload")]), - ("file-signature", [("README.md", b"payload"), (".signature.p7s", b"feed")]), - ("directory-file", [("docs/", b""), ("README.md", b"payload")]), - ] - for label, members in good: - path = make_archive(temp / f"{label}.nupkg", members) - assert "README.md" in python_payloads(path) - fsharp(path, True) - - bad = [ - ("empty", []), - ("signature", [(".signature.p7s", b"feed")]), - ("directory", [("docs/", b"")]), - ("directory-signature", [("docs/", b""), (".signature.p7s", b"feed")]), - ] - missed = [] - for label, members in bad: - path = make_archive(temp / f"{label}.nupkg", members) - fsharp(path, False) - try: - python_payloads(path) - except ValueError as error: - assert "no payload members" in str(error), str(error) - else: - missed.append(f"Python accepted {label}.nupkg") - assert not missed, "\n".join(missed) - - print("readback nonempty payload: 7 offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-nuspec-root.py b/eng/test-readback-nuspec-root.py deleted file mode 100644 index 344c8fa..0000000 --- a/eng/test-readback-nuspec-root.py +++ /dev/null @@ -1,103 +0,0 @@ -#!/usr/bin/env python3 -"""Offline root .nuspec selection against the real readback expression.""" - -import ast -import hashlib -from pathlib import Path -import subprocess -import tempfile -import xml.etree.ElementTree as ET -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/nuspec-root-inspect.fsx" -PACKAGE = "FsQuint" -VERSION = "0.1.0" -COMMIT = "a" * 40 -SPEC = ( - f'{PACKAGE}{VERSION}' - f'' -).encode() - - -def readback_functions(): - # Extract only source expressions/functions; the module top level fetches - # feeds and writes archives and receipts. - tree = ast.parse(READBACK.read_text()) - functions = [node for node in tree.body if isinstance(node, ast.FunctionDef) - and node.name in ("payloads", "select_nuspec")] - scope = {"hashlib": hashlib, "zipfile": zipfile} - exec(compile(ast.Module(body=functions, type_ignores=[]), str(READBACK), "exec"), scope) - assignments = [node for node in ast.walk(tree) if isinstance(node, ast.Assign) - and any(isinstance(target, ast.Name) and target.id == "spec" for target in node.targets)] - assert len(assignments) == 1, "readback must select one spec expression" - expression = compile(ast.Expression(assignments[0].value), str(READBACK), "eval") - - def select(archive): - return eval(expression, scope, {"archive": archive, "package": PACKAGE}) - - return scope["payloads"], select - - -def make_archive(path, members): - with zipfile.ZipFile(path, "w") as archive: - for name, body in members: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = 0o100644 << 16 - archive.writestr(info, body) - return path - - -def fsharp(path, expected): - result = subprocess.run( - ["dotnet", "fsi", str(FSX), "--", str(path), PACKAGE, VERSION, COMMIT], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - if expected: - assert result.returncode == 0 and result.stdout.strip() == "match", result.stderr - else: - assert result.returncode == 2 and "nuspec" in result.stderr, result.stderr - - -def main(): - payloads, select = readback_functions() - with tempfile.TemporaryDirectory(prefix="fsquint-nuspec-root-") as folder: - temp = Path(folder) - valid = make_archive(temp / "valid.nupkg", [ - ("FsQuint.nuspec", SPEC), ("lib/a.dll", b"payload"), - (".signature.p7s", b"feed") - ]) - with zipfile.ZipFile(valid) as archive: - assert select(archive) == "FsQuint.nuspec" - assert ET.fromstring(archive.read(select(archive))).find("metadata/repository").attrib["commit"] == COMMIT - assert len(payloads(valid)) == 2 - fsharp(valid, True) - - cases = [ - ("nested", [("nested/FsQuint.nuspec", SPEC), ("lib/a.dll", b"payload")]), - ("wrong-root", [("Foreign.nuspec", SPEC), ("lib/a.dll", b"payload")]), - ("two-roots", [("FsQuint.nuspec", SPEC), ("Foreign.nuspec", SPEC), ("lib/a.dll", b"payload")]), - ("missing", [("lib/a.dll", b"payload")]), - ] - missed = [] - for label, members in cases: - path = make_archive(temp / f"{label}.nupkg", members) - assert payloads(path), label - fsharp(path, False) - with zipfile.ZipFile(path) as archive: - try: - select(archive) - except ValueError as error: - assert "exact root nuspec" in str(error), str(error) - else: - missed.append(f"Python selected {label}.nupkg") - assert not missed, "\n".join(missed) - - print("readback nuspec root: 5 offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-nuspec-xml.py b/eng/test-readback-nuspec-xml.py deleted file mode 100644 index ec87d36..0000000 --- a/eng/test-readback-nuspec-xml.py +++ /dev/null @@ -1,105 +0,0 @@ -#!/usr/bin/env python3 -"""Offline XML identity parity over the actual Python readback block.""" - -import ast -import hashlib -from pathlib import Path -import subprocess -import tempfile -import xml.etree.ElementTree as ET -import xml.parsers.expat as expat -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -FSX = ROOT / "eng/nuspec-root-inspect.fsx" -PACKAGE = "FsQuint" -VERSION = "0.1.0" -COMMIT = "a" * 40 - - -def readback_identity(): - # Compile the served-archive `with ZipFile(target)` block itself, together - # with its pure helpers. Never execute readback.py's feed/receipt top level. - tree = ast.parse(READBACK.read_text()) - helpers = [node for node in tree.body if isinstance(node, ast.FunctionDef) - and node.name in ("payloads", "select_nuspec", "verify_nuspec_xml")] - blocks = [node for node in ast.walk(tree) if isinstance(node, ast.With) - and len(node.items) == 1 - and isinstance(node.items[0].context_expr, ast.Call) - and isinstance(node.items[0].context_expr.func, ast.Attribute) - and node.items[0].context_expr.func.attr == "ZipFile" - and node.items[0].context_expr.args - and isinstance(node.items[0].context_expr.args[0], ast.Name) - and node.items[0].context_expr.args[0].id == "target"] - assert len(blocks) == 1, "readback must have one served-archive identity block" - function = ast.parse("def identity(target, package, version, expected_commit):\n pass\n").body[0] - function.body = [blocks[0], ast.Return(value=ast.Constant(True))] - scope = {"ET": ET, "zipfile": zipfile, "hashlib": hashlib, "expat": expat} - module = ast.fix_missing_locations(ast.Module(body=[*helpers, function], type_ignores=[])) - exec(compile(module, str(READBACK), "exec"), scope) - return scope["payloads"], scope["identity"] - - -def make_archive(path, xml): - with zipfile.ZipFile(path, "w") as archive: - for name, body in [("FsQuint.nuspec", xml.encode()), ("lib/a.dll", b"payload")]: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = 0o100644 << 16 - archive.writestr(info, body) - return path - - -def fsharp(path, accept): - result = subprocess.run( - ["dotnet", "fsi", str(FSX), "--", str(path), PACKAGE, VERSION, COMMIT], - cwd=ROOT, text=True, capture_output=True, check=False, - ) - if accept: - assert result.returncode == 0 and result.stdout.strip() == "match", result.stderr - else: - assert result.returncode == 2 and "nuspec" in result.stderr, result.stderr - - -def main(): - payloads, identity = readback_identity() - metadata = f'{PACKAGE}{VERSION}' - valid = f'{metadata}' - namespace = f'{metadata}' - cases = [ - ("valid", valid, True), - ("namespace", namespace, True), - ("wrong-id", valid.replace(f'{PACKAGE}', 'Foreign'), False), - ("wrong-version", valid.replace(f'{VERSION}', '0.2.0'), False), - ("two-metadata", f'{metadata}{metadata}', False), - ("two-id", valid.replace(f'{PACKAGE}', f'{PACKAGE}{PACKAGE}'), False), - ("two-repository", valid.replace('', f''), False), - ("wrong-root", f'{metadata}', False), - ("dtd-entity", f']>{metadata.replace(PACKAGE, "&id;", 1)}', False), - ("malformed", '', False), - ("wrong-commit", valid.replace(COMMIT, "b" * 40), False), - ] - missed = [] - with tempfile.TemporaryDirectory(prefix="fsquint-nuspec-xml-") as folder: - for label, xml, accept in cases: - path = make_archive(Path(folder) / f"{label}.nupkg", xml) - assert len(payloads(path)) == 2 - fsharp(path, accept) - try: - result = identity(path, PACKAGE, VERSION, COMMIT) - except (ValueError, ET.ParseError): - if accept: - raise AssertionError(f"Python refused valid {label}") - else: - if not accept: - missed.append(f"Python accepted {label}.nupkg") - else: - assert result is True - assert not missed, "\n".join(missed) - print(f"readback nuspec XML: {len(cases)} offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/eng/test-readback-tag-stability.py b/eng/test-readback-tag-stability.py deleted file mode 100644 index 542a755..0000000 --- a/eng/test-readback-tag-stability.py +++ /dev/null @@ -1,134 +0,0 @@ -#!/usr/bin/env python3 -"""Offline version-tag movement controls without running feed readback.""" - -import ast -import hashlib -from pathlib import Path -import re -import subprocess -import tempfile -import xml.etree.ElementTree as ET -import xml.parsers.expat as expat -import zipfile - - -ROOT = Path(__file__).resolve().parents[1] -READBACK = ROOT / "eng/readback.py" -VERSION = "0.1.0" -PACKAGE = "FsQuint" - - -def source_functions(): - tree = ast.parse(READBACK.read_text()) - names = {"payloads", "select_nuspec", "verify_nuspec_xml", - "select_expected_commit", "verify_source_tag_stable"} - functions = [node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name in names] - scope = {"hashlib": hashlib, "zipfile": zipfile, "ET": ET, "expat": expat, - "re": re, "subprocess": subprocess} - exec(compile(ast.Module(body=functions, type_ignores=[]), str(READBACK), "exec"), scope) - return tree, scope - - -def git(repository, *args): - return subprocess.run(["git", *args], cwd=repository, text=True, - capture_output=True, check=True).stdout.strip() - - -def archive(path, commit): - xml = (f'{PACKAGE}{VERSION}' - f'').encode() - with zipfile.ZipFile(path, "w") as packed: - for name, body in [("FsQuint.nuspec", xml), ("lib/a.dll", b"payload")]: - info = zipfile.ZipInfo(name) - info.create_system = 3 - info.external_attr = 0o100644 << 16 - packed.writestr(info, body) - return path - - -def guard_call(node): - return (isinstance(node, ast.Expr) and isinstance(node.value, ast.Call) - and isinstance(node.value.func, ast.Name) - and node.value.func.id == "verify_source_tag_stable") - - -def wired_checkpoints(tree): - loops = [node for node in ast.walk(tree) if isinstance(node, ast.For) - and isinstance(node.target, ast.Name) and node.target.id == "feed"] - if len(loops) != 1: - return False - body = loops[0].body - if not body or not guard_call(body[0]): - return False - retries = [index for index, node in enumerate(body) if isinstance(node, ast.For) - and isinstance(node.target, ast.Name) and node.target.id == "attempt"] - if len(retries) != 1 or retries[0] + 1 >= len(body) or not guard_call(body[retries[0] + 1]): - return False - writes = [index for index, node in enumerate(tree.body) if isinstance(node, ast.Expr) - and isinstance(node.value, ast.Call) - and isinstance(node.value.func, ast.Attribute) - and node.value.func.attr == "write_text"] - return len(writes) == 1 and writes[0] > 0 and guard_call(tree.body[writes[0] - 1]) - - -def main(): - tree, source = source_functions() - with tempfile.TemporaryDirectory(prefix="fsquint-tag-stability-") as folder: - temp = Path(folder) - repo = temp / "source" - repo.mkdir() - git(repo, "init", "-q", "-b", "main") - git(repo, "config", "user.name", "Fixture") - git(repo, "config", "user.email", "fixture@example.invalid") - marker = repo / "marker.txt" - marker.write_text("source A\n") - git(repo, "add", "marker.txt") - git(repo, "commit", "-qm", "source A") - commit_a = git(repo, "rev-parse", "HEAD") - git(repo, "tag", "v0.1.0") - marker.write_text("source B\n") - git(repo, "commit", "-qam", "source B") - commit_b = git(repo, "rev-parse", "HEAD") - assert commit_a != commit_b - - selected = source["select_expected_commit"](VERSION, commit_a, repo) - package = archive(temp / "served-a.nupkg", commit_a) - with zipfile.ZipFile(package) as packed: - spec = source["select_nuspec"](packed, PACKAGE) - source["verify_nuspec_xml"](packed, spec, PACKAGE, VERSION, selected) - - git(repo, "tag", "-f", "v0.1.0", commit_b) - # The old flow still accepts A's archive using the stale selected A. - with zipfile.ZipFile(package) as packed: - source["verify_nuspec_xml"](packed, spec, PACKAGE, VERSION, selected) - - missed = [] - guard = source.get("verify_source_tag_stable") - if guard is None: - missed.append("tag moved from A to B but readback has no tag-stability guard") - else: - try: - guard(VERSION, selected, repo) - except ValueError as error: - assert "source tag" in str(error), str(error) - else: - missed.append("moved source tag accepted stale A") - git(repo, "tag", "-d", "v0.1.0") - try: - guard(VERSION, selected, repo) - except ValueError as error: - assert "source tag" in str(error), str(error) - else: - missed.append("missing source tag accepted stale A") - git(repo, "tag", "v0.1.0", commit_a) - guard(VERSION, selected, repo) - - if not wired_checkpoints(tree): - missed.append("tag guard is not wired at feed entry, after download, and before receipt") - assert not missed, "\n".join(missed) - - print("readback tag stability: 5 offline controls passed") - - -if __name__ == "__main__": - main() diff --git a/examples/AutomataProviders/README.md b/examples/AutomataProviders/README.md index 5ca47fa..bc36071 100644 --- a/examples/AutomataProviders/README.md +++ b/examples/AutomataProviders/README.md @@ -7,18 +7,17 @@ upstream implementation's own tests is an independent formal proof. ## Reproduce -Linux prerequisites: the repository's .NET SDK, Python 3, Git, a C compiler, GNU Make, +Linux prerequisites: the repository's .NET SDK, Git, a C compiler, GNU Make, Bison, Flex, Perl and pkg-config. Run as a non-root user. The destination must not exist: ```sh -python3 examples/AutomataProviders/provision.py /tmp/fsquint-providers -python3 examples/AutomataProviders/check.py \ - --automata-source /tmp/fsquint-providers/automata \ - --postgres-bin /tmp/fsquint-providers/tools/bin +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- providers-provision /tmp/fsquint-providers +dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- \ + providers-check /tmp/fsquint-providers/automata /tmp/fsquint-providers/tools/bin ``` Provisioning builds PostgreSQL 19beta3, btree_gist, PGMQ 1.10.0 and pg_cron 1.6.8 from -immutable commits recorded in `provision.py`. PostgreSQL 18 is insufficient for Automata's +immutable commits recorded in [Providers.fs](../../eng/Qualification/Providers.fs). PostgreSQL 18 is insufficient for Automata's `UPDATE FOR PORTION OF` statements. This is a pinned beta qualification, not a recommendation to deploy a beta database. A stable database or dependency upgrade requires fresh qualification. The runner verifies the unmodified Automata source commit and the NuGet providers' repository @@ -27,7 +26,7 @@ commit metadata; `packages.lock.json` binds their complete dependency content ha The runner owns a fresh PostgreSQL cluster with a private Unix socket and no TCP listener. Its application role has schema/queue rights; a separate administrator connection exercises cron installation and scheduling. No connection supplied through the caller's environment is -used. SQLite uses temporary files. Tests and workers have process-group deadlines; cleanup +used. SQLite uses temporary files. Tests and workers have process-tree deadlines; cleanup kills owned workers, stops the owned server and removes temporary resources on failure. There are no changes to a shared database or installed system service. diff --git a/examples/AutomataProviders/check.py b/examples/AutomataProviders/check.py deleted file mode 100644 index a2c1e24..0000000 --- a/examples/AutomataProviders/check.py +++ /dev/null @@ -1,200 +0,0 @@ -#!/usr/bin/env python3 -"""Run pinned upstream provider contracts against owned native resources; never a supplied DB.""" -import argparse -import hashlib -import json -import os -import pwd -from pathlib import Path -import re -import selectors -import signal -import subprocess -import tempfile -import time -import zipfile -import xml.etree.ElementTree as ET - -SOURCE = "03c3282f25888a32d36e53fa708f0342c328ccfc" -ROOT = Path(__file__).resolve().parents[2] - - -def run(args, *, cwd=None, env=None, timeout=300): - with subprocess.Popen([str(x) for x in args], cwd=cwd, env=env, start_new_session=True, - text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) as process: - try: - log, _ = process.communicate(timeout=timeout) - if process.returncode: - raise subprocess.CalledProcessError(process.returncode, args, output=log) - return log - finally: - # Also clean up test workers if their parent timed out or exited early. - try: - os.killpg(process.pid, signal.SIGKILL) - except ProcessLookupError: - pass - - -def suite(source, provider, output, env, selected=None): - start = time.monotonic() - command = ["dotnet", "run", "--project", f"tests/ByzantineSystems.Automata.Storage.{provider}.Tests", - "-c", "Release", "--", "--summary", "--sequenced"] - label = provider - if selected: - command += ["--filter-test-case", selected] - label += "-correction" - try: - with tempfile.TemporaryDirectory(prefix="fsquint-suite-") as temporary: - log = run(command, cwd=source, env={**env, "TMPDIR": temporary}) - except subprocess.CalledProcessError as error: - (output / f"{label}.log").write_text(error.stdout) - raise - (output / f"{label}.log").write_text(log) - plain = re.sub(r"\x1b\[[0-9;?]*[A-Za-z]", "", log) - counts = re.search(r"(\d+) tests run.*?(\d+) passed,\s*(\d+) ignored,\s*(\d+) failed,\s*(\d+) errored", plain) - expected = 1 if selected else {"Sqlite": 118, "Postgres": 152}[provider] - if not counts or int(counts[1]) != expected or counts[1] != counts[2] or any(int(counts[i]) for i in (3, 4, 5)): - raise RuntimeError(f"{provider}: missing, ignored or failing provider contracts; inspect log") - return {"tests": int(counts[1]), "passed": int(counts[2]), "ignored": 0, - "elapsedSeconds": round(time.monotonic() - start, 3), "command": command, - "logSha256": hashlib.sha256(log.encode()).hexdigest()} - - -def crash(provider, connection, restart=lambda: None): - """Kill a provider consumer after commit 1 / claim 2, recover in a different process.""" - dll = Path(__file__).parent / "bin/Release/net10.0/AutomataProviders.dll" - start = time.monotonic() - command = ["dotnet", str(dll), provider, "seed", str(connection)] - with subprocess.Popen(command, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, - text=True, start_new_session=True) as worker: - try: - with selectors.DefaultSelector() as selector: - selector.register(worker.stdout, selectors.EVENT_READ) - if not selector.select(timeout=30): - raise RuntimeError("provider never reached the crash boundary") - line = worker.stdout.readline().strip() - match = re.fullmatch(r"READY (\d+) (\d+)", line) - if not match: - raise RuntimeError(f"bad crash boundary: {line}") - finally: - try: - os.killpg(worker.pid, signal.SIGKILL) - except ProcessLookupError: - pass - worker.wait(timeout=10) - restart() - # Actual provider clocks expire the one-second lease; no clock injection here. - time.sleep(1.1) - result = run(["dotnet", dll, provider, "recover", connection, match[1], match[2]], timeout=30).strip() - if result != "RECOVERED state=2 epoch=2 actions=2": - raise RuntimeError(result) - return {"boundary": "commit-first-claim-second", "workerExit": worker.returncode, - "recovered": {"state": 2, "epoch": 2, "actions": 2, "newFenceToken": True}, - "serverImmediateRestart": provider == "postgres", - "elapsedSeconds": round(time.monotonic() - start, 3)} - - -def main(): - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("--automata-source", type=Path, required=True) - parser.add_argument("--postgres-bin", type=Path, required=True) - args = parser.parse_args() - source = args.automata_source.resolve() - pg = args.postgres_bin.resolve() - if run(["git", "rev-parse", "HEAD"], cwd=source).strip() != SOURCE: - raise RuntimeError("wrong Automata source") - if run(["git", "status", "--porcelain", "--untracked-files=normal"], cwd=source).strip(): - raise RuntimeError("modified source") - output = ROOT / "artifacts" / "automata-providers" - output.mkdir(parents=True, exist_ok=True) - (output / "report.json").write_text(json.dumps({"status": "incomplete", "sourceCommit": SOURCE}) + "\n") - env = os.environ.copy() - env.pop("AUTOMATA_TEST_DB", None) - env.pop("AUTOMATA_TEST_CRON_DB", None) - report = {"schemaVersion": 1, "sourceCommit": SOURCE, - "sdk": run(["dotnet", "--version"]).strip(), - "postgres": run([pg / "postgres", "--version"]).strip()} - if report["postgres"] != "postgres (PostgreSQL) 19beta3": - raise RuntimeError("unqualified PostgreSQL version; use provision.py") - run(["dotnet", "restore", Path(__file__).parent, "--locked-mode"]) - run(["dotnet", "build", Path(__file__).parent, "-c", "Release", "--no-restore"]) - cache = Path(run(["dotnet", "nuget", "locals", "global-packages", "--list"]).strip().split(": ", 1)[1]) - packages = [] - for provider in ("sqlite", "postgres"): - name = f"byzantinesystems.automata.storage.{provider}" - archive = cache / name / "0.5.0" / f"{name}.0.5.0.nupkg" - with zipfile.ZipFile(archive) as package: - metadata = ET.fromstring(package.read(next(n for n in package.namelist() if n.endswith(".nuspec")))) - repo = next(node for node in metadata.iter() if node.tag.endswith("}repository")) - if repo.attrib.get("commit") != SOURCE: - raise RuntimeError("provider package/source commit mismatch") - packages.append({"id": name, "version": "0.5.0", "sourceCommit": SOURCE, - "sha256": hashlib.sha256(archive.read_bytes()).hexdigest()}) - report["packages"] = packages - report["timeoutsSeconds"] = {"upstreamSuite": 300, "crashBoundary": 30, "recovery": 30} - report["sqlite"] = suite(source, "Sqlite", output, env) - with tempfile.TemporaryDirectory(prefix="fsquint-sqlite-") as scratch: - report["sqlite"]["crashRecovery"] = crash("sqlite", Path(scratch) / "store.db") - with tempfile.TemporaryDirectory(prefix="fsquint-pg-") as scratch: - scratch = Path(scratch) - data = scratch / "db" - socket = scratch / "socket" - socket.mkdir(mode=0o700) - run([pg / "initdb", "-D", data, "--auth=trust", "--no-locale"]) - with (data / "postgresql.conf").open("a") as config: - config.write("\nshared_preload_libraries = 'pg_cron'\ncron.database_name = 'postgres'\ncron.use_background_workers = on\n") - try: - run([pg / "pg_ctl", "-D", data, "-l", scratch / "server.log", "-o", - f"-k {socket} -h '' -p 55439", "-w", "start"]) - admin = pwd.getpwuid(os.getuid()).pw_name - run([pg / "psql", "-h", socket, "-p", "55439", "-d", "postgres", "-v", "ON_ERROR_STOP=1", "-c", - "CREATE ROLE automata_app LOGIN; GRANT CREATE ON DATABASE postgres TO automata_app; " - "GRANT CREATE ON SCHEMA public TO automata_app; " - "CREATE EXTENSION btree_gist; CREATE EXTENSION pgmq; CREATE EXTENSION pg_cron; " - "GRANT ALL ON SCHEMA pgmq TO automata_app; " - "GRANT ALL ON ALL TABLES IN SCHEMA pgmq TO automata_app; " - "GRANT ALL ON ALL SEQUENCES IN SCHEMA pgmq TO automata_app;"]) - env["AUTOMATA_TEST_DB"] = f"Host={socket};Port=55439;Database=postgres;Username=automata_app;Pooling=false" - env["AUTOMATA_TEST_CRON_DB"] = f"Host={socket};Port=55439;Database=postgres;Username={admin};Pooling=false" - report["postgresql"] = suite(source, "Postgres", output, env) - def restart(): - run([pg / "pg_ctl", "-D", data, "-m", "immediate", "-w", "stop"]) - run([pg / "pg_ctl", "-D", data, "-l", scratch / "server.log", "-o", - f"-k {socket} -h '' -p 55439", "-w", "start"]) - report["postgresql"]["crashRecovery"] = crash("postgres", env["AUTOMATA_TEST_DB"], restart) - correction = suite(source, "Postgres", output, env, - "a correction rewrites the timeline and keeps what was believed before it") - def beliefs(): - facts = {} - for table in ("instance_state", "instance_state_history", "transition", "command_correction"): - rows = run([pg / "psql", "-h", socket, "-p", "55439", "-d", "postgres", "-At", "-c", - f"SELECT row_to_json(t)::text FROM fsm.{table} t ORDER BY row_to_json(t)::text;"]) - facts[table] = [json.loads(row) for row in rows.splitlines()] - if not facts[table]: - raise RuntimeError(f"empty correction evidence: {table}") - return facts - before = beliefs() - restart() - if beliefs() != before: - raise RuntimeError("corrected history changed across immediate PostgreSQL restart") - correction["persistedRows"] = {table: len(rows) for table, rows in before.items()} - correction["rowsSha256"] = hashlib.sha256(json.dumps(before, sort_keys=True).encode()).hexdigest() - (output / "corrected-history.json").write_text(json.dumps(before, indent=2) + "\n") - report["postgresql"]["correctionRecovery"] = correction - finally: - if (data / "postmaster.pid").exists(): - run([pg / "pg_ctl", "-D", data, "-m", "immediate", "-w", "stop"]) - (output / "postgres-server.log").write_text((scratch / "server.log").read_text()) - report["status"] = "passed" - report["harnessSha256"] = {name: hashlib.sha256((Path(__file__).parent / name).read_bytes()).hexdigest() - for name in ("Program.fs", "check.py", "provision.py", "packages.lock.json")} - (output / "report.json").write_text(json.dumps(report, indent=2) + "\n") - print(json.dumps(report, indent=2)) - - -if __name__ == "__main__": - try: - main() - except subprocess.CalledProcessError as error: - print(error.stdout) - raise diff --git a/examples/AutomataProviders/evidence.json b/examples/AutomataProviders/evidence.json index 45b4c35..e320d37 100644 --- a/examples/AutomataProviders/evidence.json +++ b/examples/AutomataProviders/evidence.json @@ -26,7 +26,7 @@ "tests": 118, "passed": 118, "ignored": 0, - "elapsedSeconds": 17.642, + "elapsedSeconds": 17.521, "command": [ "dotnet", "run", @@ -38,10 +38,10 @@ "--summary", "--sequenced" ], - "logSha256": "3b65e52f401ce1bdc91ac40368651374526bbb8517cf3c6f6c4aebcd09a85457", + "logSha256": "2823e22e1082fafc2537fa094a3766f9091440118fcafde60a8f6027b4d8ec33", "crashRecovery": { "boundary": "commit-first-claim-second", - "workerExit": -9, + "workerExit": 137, "recovered": { "state": 2, "epoch": 2, @@ -49,14 +49,14 @@ "newFenceToken": true }, "serverImmediateRestart": false, - "elapsedSeconds": 1.693 + "elapsedSeconds": 1.698 } }, "postgresql": { "tests": 152, "passed": 152, "ignored": 0, - "elapsedSeconds": 13.356, + "elapsedSeconds": 13.667, "command": [ "dotnet", "run", @@ -68,10 +68,10 @@ "--summary", "--sequenced" ], - "logSha256": "acd8c057ccbe2dd4be09699ae0bc8592e356bb8b7c5bfb73a22e8795b769add5", + "logSha256": "a94e2c6c273d6dce644492ce4e89b3c93d8c612a9403d817a50a4f3ec671e33f", "crashRecovery": { "boundary": "commit-first-claim-second", - "workerExit": -9, + "workerExit": 137, "recovered": { "state": 2, "epoch": 2, @@ -79,13 +79,13 @@ "newFenceToken": true }, "serverImmediateRestart": true, - "elapsedSeconds": 7.635 + "elapsedSeconds": 7.842 }, "correctionRecovery": { "tests": 1, "passed": 1, "ignored": 0, - "elapsedSeconds": 1.974, + "elapsedSeconds": 1.957, "command": [ "dotnet", "run", @@ -99,21 +99,21 @@ "--filter-test-case", "a correction rewrites the timeline and keeps what was believed before it" ], - "logSha256": "cdcbd48d9bdba12fea211161f9658e86631674b370614ea70a64d26498666ced", + "logSha256": "48d8b4b973a7f64a125e2c827daef86c05971582b5e1dcd9437845a58455f98d", "persistedRows": { "instance_state": 3, "instance_state_history": 3, "transition": 3, "command_correction": 1 }, - "rowsSha256": "331beb1fbad113566e67c8916ffdb3fdb7357b032d5ac0a869f29674a255d78b" + "rowsSha256": "4da0f56f13f0bb0aeb1f46553db183c9c737b0bd1347f1bfee1b78fe6327d4eb" } }, "status": "passed", "harnessSha256": { "Program.fs": "abc39436d33c26050ad441bc47cb07a85ae88c93fe331a5d114dfe9bfbaa7c24", - "check.py": "6e0eed604def86083d3a46f9a8c04ffee2500b945bf28f4cdfca6d64f2c54b80", - "provision.py": "e949296bdc332f006c7b9efe0a7eae26c2e756abfadb0bf9346ab7ac81d972b1", - "packages.lock.json": "1aa7ab8affbbc8f27c85aa29f2cc30178b6326d7c20f788ce248226282c31636" + "packages.lock.json": "1aa7ab8affbbc8f27c85aa29f2cc30178b6326d7c20f788ce248226282c31636", + "Providers.fs": "8787e335e2d4a540c9fba6829b571b180c6861f2e92ec376137f6e8ab6434fb0", + "Common.fs": "8611591f42ce83bd86731b0b7517a5c9971a273d7944476171c4f63eb1270c62" } } diff --git a/examples/AutomataProviders/provision.py b/examples/AutomataProviders/provision.py deleted file mode 100644 index 294a7d2..0000000 --- a/examples/AutomataProviders/provision.py +++ /dev/null @@ -1,55 +0,0 @@ -#!/usr/bin/env python3 -"""Build pinned PostgreSQL extensions in a new private prefix, without sudo or a shared service.""" -import argparse -import json -from pathlib import Path -import subprocess -import tempfile - -PINS = { - "postgres": ("https://github.com/postgres/postgres.git", "3638289fb57bdabec00deda98ee9624a35f5d66a"), - "pgmq": ("https://github.com/pgmq/pgmq.git", "51d7655a097d91bf05ad5ae40dd604aa067ed355"), - "pg_cron": ("https://github.com/citusdata/pg_cron.git", "5cedfa472ccc83567aa23ec645925ed8489a7797"), - "automata": ("https://github.com/byzantine-systems/automata.git", "03c3282f25888a32d36e53fa708f0342c328ccfc"), -} - - -def run(args, cwd): - subprocess.run([str(x) for x in args], cwd=cwd, check=True, timeout=900) - - -def clone(name, destination): - url, commit = PINS[name] - destination.mkdir() - run(["git", "init", "-q"], destination) - run(["git", "fetch", "--depth", "1", url, commit], destination) - run(["git", "checkout", "--detach", "FETCH_HEAD"], destination) - - -def main(): - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("destination", type=Path, help="must not exist; owns tools/ and automata/") - args = parser.parse_args() - root = args.destination.resolve() - root.mkdir(parents=True, exist_ok=False) - prefix = root / "tools" - with tempfile.TemporaryDirectory(prefix="fsquint-provider-build-") as temporary: - temporary = Path(temporary) - pg = temporary / "postgres" - clone("postgres", pg) - run(["./configure", f"--prefix={prefix}", "--without-readline", "--without-icu", "--without-zlib"], pg) - run(["make", "-j4"], pg) - run(["make", "install"], pg) - run(["make", "-C", "contrib/btree_gist", "install"], pg) - for name, subdir in (("pgmq", "pgmq-extension"), ("pg_cron", ".")): - path = temporary / name - clone(name, path) - option = f"PG_CONFIG={prefix / 'bin/pg_config'}" - run(["make", option], path / subdir) - run(["make", "install", option], path / subdir) - clone("automata", root / "automata") - (root / "pins.json").write_text(json.dumps(PINS, indent=2) + "\n") - - -if __name__ == "__main__": - main() diff --git a/examples/AutomataReplay/README.md b/examples/AutomataReplay/README.md index 1fb8193..bd0798a 100644 --- a/examples/AutomataReplay/README.md +++ b/examples/AutomataReplay/README.md @@ -12,10 +12,10 @@ Run the package characterization: ```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 ``` -For the CI qualification, run `python3 examples/AutomataReplay/check.py`. It creates an +For the CI qualification, run `dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- replay`. It creates an isolated consumer and package cache, restores the lock file, verifies the package archive's SHA-256 and source/license metadata against the baseline, and executes the characterization. The candidate FsQuint package includes its source revision: only its content hash is refreshed @@ -127,7 +127,7 @@ The guard defect diverges at step 2; swapped submission effects, wrong target an defects diverge at step 1. Unknown inputs, noncontiguous bindings and malformed manifests are rejected before initialization. Existing FsQuint tests separately qualify malformed ITF. -`check.py` runs offline replay from an isolated package consumer. With `QUINT_BIN` set, +`replay` runs offline replay from an isolated package consumer. With `QUINT_BIN` set, it additionally checks the pinned executable digest, typechecks the model, executes four witnesses and samples both safety properties (1,000 traces × 30 steps, seed 42). These sampled results are not exhaustive verification or a runtime/provider correctness claim. @@ -176,7 +176,7 @@ The surface review retains an example-local helper; no new NuGet package is intr ## FQA-4 regeneration, coverage and failure evidence With `QUINT_BIN` and `QUINT_HOME` pointing to the provisioned baseline, run -`python3 examples/AutomataReplay/regenerate.py`. Check mode regenerates all fixed witnesses +`dotnet run --project eng/Qualification/Qualification.fsproj -c Release -- generate`. Check mode regenerates all fixed witnesses and eight 30-step approval samples in a temporary directory. It compares variables and state contents, ignoring only ITF metadata such as generation timestamps. `--write` creates new fixture files and manifests but refuses to overwrite an existing regression with changed @@ -233,6 +233,6 @@ FQA-7 obligations, not consequences of these pure checks. See [PROTOCOL.md](PROTOCOL.md) for the model, real processor/dispatcher harness, seven repeatable schedules, three protocol mutations and precise qualification limits. -`check.py` includes these schedules and model witnesses; no database is needed. The example +`replay` includes these schedules and model witnesses; no database is needed. The example now qualifies this bounded controlled-runtime profile, while real-provider evidence remains separate. Neither the test store nor the model is a production storage implementation. diff --git a/examples/AutomataReplay/check.py b/examples/AutomataReplay/check.py deleted file mode 100644 index 9e7613e..0000000 --- a/examples/AutomataReplay/check.py +++ /dev/null @@ -1,108 +0,0 @@ -#!/usr/bin/env python3 -"""Check the pinned public package from an isolated, locked consumer restore.""" -import hashlib -import json -import os -from pathlib import Path -import shutil -import subprocess -import tempfile -import xml.etree.ElementTree as ET -import zipfile - - -def main(): - example = Path(__file__).resolve().parent - repo = example.parents[1] - baseline = json.loads((example / "baseline.json").read_text()) - with tempfile.TemporaryDirectory(prefix="fsquint-automata-") as scratch: - root = Path(scratch) - names = ["AutomataReplay.fsproj", "baseline.json", "packages.lock.json"] - names += [p.name for pattern in ("*.fs", "*.qnt") for p in example.glob(pattern)] - for name in names: - shutil.copy2(example / name, root / name) - shutil.copytree(example / "fixtures", root / "fixtures") - shutil.copy2(repo / "examples/Shared/PureReplay.fs", root / "PureReplay.fs") - for name in ("global.json", "NuGet.Config"): - shutil.copy2(repo / name, root / name) - env = dict(os.environ, NUGET_PACKAGES=str(root / "packages"), - NUGET_HTTP_CACHE_PATH=str(root / "http")) - restore = ["dotnet", "restore", "AutomataReplay.fsproj", - "--source", str(repo / "artifacts/packages"), - "--source", "https://api.nuget.org/v3/index.json"] - # FsQuint is the package just built from this candidate, including its source revision. - # Refresh only that content identity; all third-party locks must stay byte-for-byte equal. - locked = json.loads((root / "packages.lock.json").read_text()) - subprocess.run([*restore, "--force-evaluate"], cwd=root, env=env, check=True) - refreshed = json.loads((root / "packages.lock.json").read_text()) - locked["dependencies"]["net10.0"]["FsQuint"]["contentHash"] = refreshed["dependencies"]["net10.0"]["FsQuint"]["contentHash"] - if locked != refreshed: - raise RuntimeError("Dependency lock changed beyond the candidate FsQuint content hash") - candidate = repo / "artifacts/packages/FsQuint.0.1.1.nupkg" - restored = root / "packages/fsquint/0.1.1/fsquint.0.1.1.nupkg" - if restored.read_bytes() != candidate.read_bytes(): - raise RuntimeError("Consumer did not restore the exact candidate FsQuint package") - subprocess.run([*restore, "--locked-mode"], cwd=root, env=env, check=True) - package_id = baseline["packageId"].lower() - version = baseline["packageVersion"] - archive = root / "packages" / package_id / version / f"{package_id}.{version}.nupkg" - if hashlib.sha256(archive.read_bytes()).hexdigest() != baseline["packageSha256"]: - raise RuntimeError("Restored Automata package differs from the recorded archive") - for pin in baseline.get("additionalPackages", []): - package_id, version = pin["id"].lower(), pin["version"] - package_path = root / "packages" / package_id / version / f"{package_id}.{version}.nupkg" - if hashlib.sha256(package_path.read_bytes()).hexdigest() != pin["sha256"]: - raise RuntimeError("Additional package provenance mismatch: " + pin["id"]) - with zipfile.ZipFile(archive) as package: - nuspec = next(name for name in package.namelist() if name.endswith(".nuspec")) - metadata = ET.fromstring(package.read(nuspec)).find("{*}metadata") - expected = {"id": baseline["packageId"], "version": version, - "license": baseline["licenseExpression"]} - for key, value in expected.items(): - if metadata.find(f"{{*}}{key}").text != value: - raise RuntimeError(f"Unexpected package {key}") - source = metadata.find("{*}repository") - if (source.get("url") != baseline["repository"] or - source.get("commit") != baseline["repositoryCommit"]): - raise RuntimeError("Unexpected package source provenance") - execution = subprocess.run(["dotnet", "run", "--project", "AutomataReplay.fsproj", - "-c", "Release", "--no-restore"], cwd=root, env=env, - check=True, capture_output=True, text=True, timeout=120) - print(execution.stdout, end="") - failures = [json.loads(line.removeprefix("DIVERGENCE ")) for line in execution.stdout.splitlines() - if line.startswith("DIVERGENCE ")] - if len(failures) != 4: - raise RuntimeError("Missing approval mutation diagnostics") - artifact = repo / "artifacts/automata-replay.json" - artifact.parent.mkdir(exist_ok=True) - artifact.write_text(json.dumps({"schema": "fsquint.replay-evidence/1", "outcome": "passed", - "mutationDiagnostics": failures}, indent=2) + "\n") - print("PASS: isolated locked restore and package archive/source/license provenance.") - quint = os.environ.get("QUINT_BIN") - if quint: - if hashlib.sha256(Path(quint).read_bytes()).hexdigest() != baseline["quintSha256"]: - raise RuntimeError("Quint executable differs from the qualified pin") - subprocess.run(["python3", "regenerate.py"], cwd=example, check=True, timeout=180) - for args in (["typecheck", "approval.qnt"], - ["typecheck", "turnstile.qnt"], - ["run", "correction.qnt", "--invariant", "safety", "--seed", "42", - "--max-samples", "1000", "--max-steps", "10", "--verbosity", "1"], - ["run", "protocol.qnt", "--invariant", "safety", "--seed", "42", - "--max-samples", "1000", "--max-steps", "10", "--verbosity", "1"], - ["test", "turnstile_test.qnt", "--seed", "42"], - ["typecheck", "resolver.qnt"], - ["test", "resolver_test.qnt", "--seed", "42"], - ["run", "resolver.qnt", "--invariant", "safety", "--seed", "42", - "--max-samples", "1000", "--max-steps", "10", "--verbosity", "1"], - ["test", "approval_test.qnt", "--seed", "42"], - ["run", "approval.qnt", "--invariant", "safety", "--seed", "42", - "--max-samples", "1000", "--max-steps", "30", "--verbosity", "1"], - ["run", "approval.qnt", "--invariant", "transitionSafety", "--seed", "42", - "--max-samples", "1000", "--max-steps", "30", "--verbosity", "1"]): - subprocess.run([quint, *args], cwd=example, check=True, timeout=120) - else: - print("Model execution not requested; offline fixture replay qualified above.") - - -if __name__ == "__main__": - main() diff --git a/examples/AutomataReplay/regenerate.py b/examples/AutomataReplay/regenerate.py deleted file mode 100644 index 8e433e4..0000000 --- a/examples/AutomataReplay/regenerate.py +++ /dev/null @@ -1,185 +0,0 @@ -#!/usr/bin/env python3 -"""Regenerate genuine Quint traces, validate inputs/coverage, retain raw bytes on --write.""" -import argparse -import hashlib -import json -import os -from pathlib import Path -import re -import subprocess -import tempfile - - -def digest(path): - return hashlib.sha256(path.read_bytes()).hexdigest() - - -def meaningful(raw): - doc = json.loads(raw) - if doc.get("#meta", {}).get("status") != "ok": - raise RuntimeError("Quint did not report positive trace evidence") - return {"vars": doc["vars"], "states": [ - {key: value for key, value in state.items() if key != "#meta"} - for state in doc["states"]]} - - -def main(): - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("--write", action="store_true", help="Replace fixtures explicitly; default only compares") - args = parser.parse_args() - root = Path(__file__).resolve().parent - baseline = json.loads((root / "baseline.json").read_text()) - quint = Path(os.environ["QUINT_BIN"]).resolve() - evaluator = Path(os.environ["QUINT_HOME"]) / "rust-evaluator-v0.6.0/quint_evaluator" - if digest(quint) != baseline["quintSha256"] or digest(evaluator) != baseline["evaluatorSha256"]: - raise RuntimeError("Generator/evaluator identity differs from the baseline") - sources = {p.name: digest(p) for p in sorted(root.glob("*.qnt"))} - commands = [] - inputs_seen, phases, outcomes = set(), set(), set() - action_orders = set() - resolver_paths, rule_markers, handlers = set(), set(), set() - - def invoke(arguments): - commands.append(arguments) - result = subprocess.run([str(quint), *arguments], cwd=root, capture_output=True, - text=True, timeout=120) - if result.returncode != 0: - raise RuntimeError(f"Quint failed ({result.returncode}): {result.stdout}\n{result.stderr}") - - def accept(candidate, relative): - target = root / "fixtures" / relative - raw = candidate.read_bytes() - parsed = meaningful(raw) - if args.write: - target.parent.mkdir(parents=True, exist_ok=True) - if target.exists(): - if parsed != meaningful(target.read_bytes()): - raise RuntimeError(f"Existing regression changed: version the profile/fixture before replacing {relative}") - else: - target.write_bytes(raw) - elif parsed != meaningful(target.read_bytes()): - raise RuntimeError(f"Regeneration differs semantically: {relative}") - return target, parsed["states"] - - def json_file(path, value): - if args.write: - path.parent.mkdir(parents=True, exist_ok=True) - path.write_text(json.dumps(value, indent=2) + "\n") - elif json.loads(path.read_text()) != value: - raise RuntimeError(f"Manifest/coverage differs: {path.name}") - - allowed = {("submit", "author"), ("approve", "author"), ("approve", "reviewer"), - ("publish", "author"), ("cancel", "author"), ("remind", "author")} - - def approval_binding(target, states, entries, source, seed, sampled): - if len(entries) != len(states) - 1: - raise RuntimeError("Input count differs") - for entry, state in zip(entries, states[1:]): - inp = state["input"] - if set(inp) != {"op", "actor"} or (inp["op"], inp["actor"]) not in allowed: - raise RuntimeError("Unknown generated input") - if inp != {"op": entry["op"], "actor": entry["actor"]}: - raise RuntimeError("Authored input differs from instrumented input") - inputs_seen.add((inp["op"], inp["actor"])) - for item in states: - state = item["state"] - phases.add(state["phase"]) - outcomes.add(state["outcome"]) - action_orders.add(tuple((e["kind"], e["name"]) for e in state["actions"])) - binding = {"schema": "fsquint.approval-binding/2" if sampled else "fsquint.approval-binding/1", - "profile": "fsquint.automata-approval/1", "traceSha256": digest(target), - "modelSha256": sources["approval.qnt"], "scenarioSha256": sources[source], "steps": entries} - if sampled: - binding.update(sourceFile=source, seed=str(seed), maxSteps=30) - json_file(target.with_suffix("").with_suffix(".binding.json"), binding) - - with tempfile.TemporaryDirectory(prefix="fsquint-generation-") as scratch: - scratch = Path(scratch) - for module in ("approval", "resolver", "turnstile", "correction", "protocol"): - invoke(["typecheck", f"{module}.qnt"]) - invoke(["test", f"{module}_test.qnt", "--seed", "42", "--max-samples", "1", - "--out-itf", str(scratch / f"{module}_{{test}}_{{seq}}.itf.json")]) - authored = {} - name = None - for line, text in enumerate((root / "approval_test.qnt").read_text().splitlines(), 1): - match = re.search(r"run (\w+)", text) - if match: - name = match[1] - authored[name] = [] - match = re.search(r'op: "(\w+)", actor: "(\w+)"', text) - if match: - authored[name].append(dict(index=len(authored[name])+1, op=match[1], actor=match[2], line=line)) - for name, entries in authored.items(): - matches = list(scratch.glob(f"approval_{name}_*.itf.json")) - if len(matches) != 1: - raise RuntimeError("Missing or ambiguous witness output") - target, states = accept(matches[0], f"{name}.itf.json") - approval_binding(target, states, entries, "approval_test.qnt", 42, False) - for case in range(13): - matches = list(scratch.glob(f"resolver_case{case}Test_*.itf.json")) - if len(matches) != 1: - raise RuntimeError("Missing resolver witness") - _, states = accept(matches[0], f"resolver/case{case}.itf.json") - result = states[-1]["result"] - resolver_paths.add((tuple(result["exited"]), tuple(result["entered"]))) - handlers.add(result["handler"]) - rule_markers.update(e["node"] for e in result["actions"] if e["kind"] == "rule") - accept(next(scratch.glob("turnstile_passageTest_*.itf.json")), "turnstile.itf.json") - for case in range(10): - matches = list(scratch.glob(f"correction_case{case}Test_*.itf.json")) - if len(matches) != 1: - raise RuntimeError("Missing correction witness") - accept(matches[0], f"correction/case{case}.itf.json") - for case in range(7): - matches = list(scratch.glob(f"protocol_case{case}Test_*.itf.json")) - if len(matches) != 1: - raise RuntimeError("Missing protocol witness") - accept(matches[0], f"protocol/case{case}.itf.json") - line = next(i for i, s in enumerate((root / "approval.qnt").read_text().splitlines(), 1) if "action step" in s) - for seed in (1, 7, 42, 99, 123, 1000, 2000, 3000): - path = scratch / f"sample-{seed}.itf.json" - invoke(["run", "approval.qnt", "--invariant", "safety", "--seed", str(seed), - "--max-samples", "1", "--max-steps", "30", "--out-itf", str(path)]) - target, states = accept(path, f"sampled/seed-{seed}.itf.json") - # Uses the dedicated choice channel, never adjacent domain observations. - entries = [dict(index=i, op=s["input"]["op"], actor=s["input"]["actor"], line=line) - for i, s in enumerate(states[1:], 1)] - approval_binding(target, states, entries, "approval.qnt", seed, True) - - resolver_files = ["resolver.qnt", "resolver_test.qnt"] + [f"fixtures/resolver/case{i}.itf.json" for i in range(13)] - json_file(root / "fixtures/resolver/manifest.json", {name: digest(root / name) for name in resolver_files}) - turnstile_files = ["fixtures/turnstile.itf.json", "turnstile.qnt", "turnstile_test.qnt"] - json_file(root / "fixtures/turnstile.manifest.json", {name: digest(root / name) for name in turnstile_files}) - correction_files = ["correction.qnt", "correction_test.qnt"] + [f"fixtures/correction/case{i}.itf.json" for i in range(10)] - json_file(root / "fixtures/correction/manifest.json", {name: digest(root / name) for name in correction_files}) - protocol_files = ["protocol.qnt", "protocol_test.qnt"] + [f"fixtures/protocol/case{i}.itf.json" for i in range(7)] - json_file(root / "fixtures/protocol/manifest.json", {name: digest(root / name) for name in protocol_files}) - if inputs_seen != allowed or phases != {"Draft", "Pending", "Approved", "Published", "Cancelled"}: - raise RuntimeError("Required input/phase coverage missing") - if not {"Initial", "Applied", "NotAuthorized", "Unhandled", "Terminated"}.issubset(outcomes): - raise RuntimeError("Required outcome coverage missing") - for order in ((('audit','submitted'),('notify','review')), (('audit','published'),('notify','published'))): - if order not in action_orders: - raise RuntimeError("Required ordered action coverage missing") - coverage = {"schema": "fsquint.coverage/1", "inputs": sorted([list(x) for x in inputs_seen]), - "phases": sorted(phases), "outcomes": sorted(outcomes), "resolverCases": list(range(13)), - "correctionCases": list(range(10)), - "protocolSchedules": list(range(7)), - "actionOrders": [[list(pair) for pair in order] for order in sorted(action_orders)], - "resolverPaths": [[list(exits), list(entries)] for exits, entries in sorted(resolver_paths)], - "resolverHandlers": sorted(handlers), "ruleMarkers": sorted(rule_markers), - "sampleSeeds": [1,7,42,99,123,1000,2000,3000], "sampleStepBound": 30, - "claim": "required bins exercised; no exhaustive application/runtime claim"} - json_file(root / "fixtures/coverage.json", coverage) - evidence = {"schema": "fsquint.generation-evidence/1", "outcome": "passed", "quintSha256": digest(quint), - "evaluatorSha256": digest(evaluator), "sourceDigests": sources, "coverage": coverage, - "commands": commands, "rawAndBindingDigests": { - str(p.relative_to(root)): digest(p) for p in sorted((root / "fixtures").rglob("*.json"))}} - out = root.parents[1] / "artifacts/automata-generation.json" - out.parent.mkdir(exist_ok=True) - out.write_text(json.dumps(evidence, indent=2) + "\n") - print("PASS: pinned witness/sample regeneration, explicit input bindings and all required coverage bins.") - - -if __name__ == "__main__": - main()