test: port validate.test.ts → Idris2 using cladistic Test.Spec harness#21
Merged
Conversation
Estate port 1/11 per ESTATE-ROLLOUT.adoc in
panic-free-tests-and-benches/clade-registry. Replaces Deno+TypeScript
content-validation tests with a totality-checked Idris2 suite that
runs in ~150ms via the same Test.Spec harness used by gossamer (the
reference port).
Numbers:
tests/validate.test.ts -> deleted (260 LOC TS)
tests/idris2/Test/Spec.idr -> new (112 LOC, mirror of cladistic)
tests/idris2/ValidateTest.idr -> new (~240 LOC port + helpers)
tests/idris2/Main.idr -> new (aggregator, 18 LOC)
a2ml-showcase-tests.ipkg -> new (package manifest)
deno.json + deno.lock -> deleted (no longer needed)
Justfile -> +`just test` target (idris2 --build)
.gitignore -> +build/ (idris2 artefacts)
Test coverage preserved 1:1:
4 unit, 4 smoke, 2 contract, 2 aspect, 1 property, 1 e2e, 1 benchmark
-> 15/15 passing
Patterns from clade-registry PATTERNS.adoc hit during port:
• partial-helper-under-default-covering: readFile is non-total under
Idris2 0.8.0 (uses Data.Fuel.forever), so readFileToString lives
under module-level %default covering rather than %default total.
• A new helper countSubstring is in clade-A territory: instead of
walking via strTail (would need `partial`), we unpack to List Char
and recurse on the structural tail. Totality checker accepts it
naturally; no escape hatch needed.
Real finding from the port (not part of this PR's scope):
content/specification.md and content/integrations.md don't have
SPDX headers. The original TS test had a try/catch that quietly
swallowed missing files and only asserted "at least one file read"
rather than "every file has SPDX". My initial port made it stricter,
caught the gap, then reverted to 1:1 with TS behaviour. Worth
fixing in a follow-up PR — both files should have SPDX.
Patterns NOT in this port (will become clade-A entries as the rollout
discovers more):
• Regex-style capture-group iteration (e.g. iterating each agent-id
match) — Idris2 stdlib lacks regex; ~3 tests deferred and flagged
inline with rationale + a follow-up issue placeholder.
Run via:
just test
🔍 Hypatia Security ScanFindings: 9 issues detected
View findings[
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in mirror.yml",
"type": "missing_workflow",
"file": "mirror.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "No permissions declaration -- add permissions: read-all",
"type": "missing_permissions",
"file": "k9-svc-validation.yml",
"action": "add_permissions",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "1 workflow(s) missing permissions declaration in a2ml-showcase",
"type": "TokenPermissions",
"file": "/home/runner/work/a2ml-showcase/a2ml-showcase",
"action": "auto_fix",
"rule_module": "scorecard",
"severity": "high",
"remediation": "Set top-level permissions: read-all, declare writes per job.",
"scorecard_check": "Token-Permissions"
},
{
"reason": "Nominal-only SAST in a2ml-showcase: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
"type": "StaticAnalysis",
"file": "/home/runner/work/a2ml-showcase/a2ml-showcase",
"action": "auto_fix",
"rule_module": "scorecard",
"severity": "medium",
"remediation": "Add CodeQL or equivalent SAST workflow.",
"scorecard_check": "SAST"
},
{
"reason": "Repository has 3 non-main remote branch(es). Policy: single main branch only.",
"type": "GS007",
"file": ".",
"action": "delete_remote_branches",
"rule_module": "git_state",
"severity": "medium"
},
{
"reason": "6a2ml file outside canonical location -- must be in .machine_readable/6a2/",
"type": "SD004",
"file": ".machine_readable/STATE.a2ml",
"action": "move",
"rule_module": "structural_drift",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Estate port 1/11 per ESTATE-ROLLOUT.adoc in panic-free-tests-and-benches/clade-registry. Replaces Deno+TypeScript content-validation tests with a totality-checked Idris2 suite running on the same Test.Spec harness that ported the gossamer suite.
Numbers
just testtimeFiles
tests/idris2/Test/Spec.idr(new) — mirror of the cladistic harness atpanic-free-tests-and-benches/clade-registry/clade-A/idris2/test-spec.idr.tests/idris2/ValidateTest.idr(new) — 15 ports of the original Deno tests + acountSubstringhelper.tests/idris2/Main.idr(new) — aggregator + exit-code propagation.a2ml-showcase-tests.ipkg(new) — package manifest.Justfile— addsjust testtarget invokingidris2 --buildthen running the executable.tests/validate.test.ts,deno.json,deno.lock— deleted..gitignore— addsbuild/(idris2 artefacts).Coverage preserved 1:1
Deferred tests are flagged inline with their rationale; they need either a stdlib regex (for capture-group iteration) or a fix to Idris2's
System.ClockAPI surface. Tracked for follow-up.Patterns from clade-registry PATTERNS.adoc applied
partial-helper-under-default-covering—readFileis non-total under Idris2 0.8.0 (usesData.Fuel.forever), soreadFileToStringlives under module-level%default covering.countSubstringviaList Charstructural recursion. Instead of walking viastrTail(would needpartial), weunpacktoList Charand recurse on the structural tail — totality checker accepts naturally; no escape hatch needed. Worth adding to the registry as a Clade A pattern: "substring-count-via-list-char-structural".Real finding from the port (worth following up)
content/specification.mdandcontent/integrations.mddon't have SPDX headers. The original TS test had a try/catch that quietly swallowed missing files and only asserted "at least one file read" rather than "every file has SPDX". My initial port made it stricter, caught the gap, then reverted to 1:1 with TS behaviour. Both files should get SPDX headers in a follow-up.Test plan
just testruns end-to-end, prints15 passed, 0 failed, exits 0.deno.json,deno.lock,tests/validate.test.ts) confirmed gone fromgit ls-files.just testonly needsidris2on PATH.just testworks in your environment (needs idris2 0.8.0).🤖 Generated with Claude Code