[Lean Squad] feat(fv): Task 2 — informal spec for CommandLineParseResult.Equals

[github-actions]

🔬 Lean Squad — automated formal-verification agent (run 25085790184)

Summary

Task 2: extract a precise informal specification for CommandLineParseResult.Equals, the structural-equality method for the command-line parse result type.

Target: bool Equals(CommandLineParseResult? other) in src/Platform/Microsoft.Testing.Platform/CommandLine/ParseResult.cs

Spec highlights

The spec (formal-verification/specs/commandlineparseresult_equals_informal.md) documents 19 properties across 6 groups:

Group	Properties
1 — Basic equality contract	Null-safety, reference-reflexivity, structural-reflexivity, symmetry, transitivity
2 — Extensionality	Full bidirectional extensionality over all fields
3 — object.Equals consistency	Typed vs. untyped overloads agree
4 — Order sensitivity	Errors, options, and arguments are compared positionally
5 — Empty value	Empty result equals itself and any other null/empty result
6 — ToolName comparison	Ordinal case-sensitive null/non-null handling

Key design observations

• Order-preserving equality (not option-set equality): --foo --bar ≠ --bar --foo.
• Ordinal case-sensitive ToolName comparison (contrast with IsOptionSet which uses OrdinalIgnoreCase).
• No exceptions on null other — correctly handled at step 1.
• GetHashCode is consistent: same fields → same hash code.

Lean modelling plan

• string? → Option String
• IReadOnlyList<T> → List T
• string[] → List String
• All string comparisons → DecidableEq String
• == and != operators are trivial wrappers and not modelled separately

Next step

Task 3: write CommandLineParseResult.lean with theorem stubs and (ideally) proved equality laws.

Generated by 📐 Lean Squad, see workflow run.

---

Note

This was originally intended as a pull request, but GitHub Actions is not permitted to create or approve pull requests in this repository.
The changes have been pushed to branch lean-squad/task2-parseresult-equals-spec-2026-04-29-87fea4e2e7e10b8d.

Click here to create the pull request

To fix the permissions issue, go to Settings → Actions → General and enable Allow GitHub Actions to create and approve pull requests. See also: gh-aw FAQ

Show patch preview (223 of 223 lines)

From 093b455510c71eecdc05338e3edb6e005d0439f7 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Wed, 29 Apr 2026 01:18:13 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=202=20=E2=80=94=20informal=20s?=
 =?UTF-8?q?pec=20for=20CommandLineParseResult.Equals?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Extract a precise informal specification for CommandLineParseResult.Equals,
the structural-equality implementation for the command-line parse result type.

The spec documents:
- 19 properties across 6 groups (null-safety, extensionality, object.Equals
  consistency, order-sensitivity, Empty-value behaviour, ToolName comparison)
- Algorithm walkthrough (O(n·m), pure, no exceptions for null input)
- Edge cases: null other, case-sensitive ToolName, order-sensitive errors/options
- Lean modelling plan: Option String for nullable, List for collections

Next: Task 3 — write ArgumentArity.lean (highest priority Lean target)

🔬 Lean Squad — automated FV agent

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 .../commandlineparseresult_equals_informal.md | 184 ++++++++++++++++++
 1 file changed, 184 insertions(+)
 create mode 100644 formal-verification/specs/commandlineparseresult_equals_informal.md

diff --git a/formal-verification/specs/commandlineparseresult_equals_informal.md b/formal-verification/specs/commandlineparseresult_equals_informal.md
new file mode 100644
index 000000000..9deabb434
--- /dev/null
+++ b/formal-verification/specs/commandlineparseresult_equals_informal.md
@@ -0,0 +1,184 @@
+# Informal Specification — `CommandLineParseResult.Equals`
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+## Target
+
+- **Type**: `sealed class CommandLineParseResult(string? toolName, IReadOnlyList<CommandLineParseOption> options, IReadOnlyList<string> errors) : IEquatable<CommandLineParseResult>`
+- **Method**: `
... (truncated)