test: port core.test.ts → Idris2 (partial; estate port 6/11, file 1 of 4) by hyperpolymath · Pull Request #55 · hyperpolymath/ubicity

hyperpolymath · 2026-05-20T11:18:15Z

Summary

Estate port 6/11 per ESTATE-ROLLOUT.adoc. PARTIAL — this PR ports ONLY `tests/core.test.ts` (1 of 4 TS test files in ubicity). The other 3 (privacy/mapper/export) await separate PRs after the unit-logic strategy review documented in repos-monorepo PR #12.

	Before	After
core.test.ts	5 tests	3 ported / 2 deferred
Pass rate	(unrun)	3/3 PASS
Other TS test files (privacy/mapper/export)	3 files, 489 LOC	Untouched — separate PRs after strategy review
Run via	`deno test --allow-read tests/`	`just test-core`

What's ported (3 tests)

TS test	Idris2 approach
LearningExperience validation	Defines mirror records (Location/Learner/Experience/LearningExperience), constructs a literal value, asserts field presence + domain length.
Timestamp ISO 8601 shape	Checks for `T` + `Z` markers; length sanity check.
Domain array dedup/normalize/filter	Uses Idris2 stdlib `nub` + `map toLower` + `filter isPrefixOf`.

What's deferred (2 tests)

TS test	Why deferred
Core - Data persistence	Needs JSON parse + temp-file write. Idris2 base stdlib lacks JSON. Would need `idris2-json` dep or a custom parser.
Core - ID generation uniqueness	Needs `crypto.randomUUID()`. Idris2 base lacks crypto. Would need crypto dep or deterministic-RNG mock (defeats the uniqueness check).

Patterns applied

From `panic-free-tests-and-benches/clade-registry/clade-A/idris2/PATTERNS.adoc`:

`ascii-only-string-literals-idris2`
`one-mega-list-for-testcases-idris2`

New learning (worth a registry PR follow-up): Idris2's `head` requires NonEmpty proof. Use cons-cell pattern match for safe first-element access:

```idris2
case xs of
(h :: _) => h
[] => default
```

Why partial

ubicity's other 3 TS files include SHA-256 hashing (privacy.test.ts), JSON parsing (export.test.ts), and file mapping logic (mapper.test.ts) that require substantial Idris2 dependencies or a different port strategy entirely. The ESTATE-ROLLOUT.adoc "unit-logic strategy" section flags this — each repo needs a decision (Idris2 mirror / canonical-language port / delete) before more porting work.

This PR is the smallest defensible unit: one TS file's worth of straightforward data-validation tests. The remaining files are tracked separately.

Test plan

`just test-core` runs end-to-end and exits 0.
3/3 PASS verified locally.
`tests/core.test.ts` deleted; other test files retained.
Reviewer: confirm `just test-core` works in your environment (idris2 0.8.0).

🤖 Generated with Claude Code

…artial) Estate port 6/11 per ESTATE-ROLLOUT.adoc — PARTIAL: this PR ports ONLY tests/core.test.ts (1 of 4 TS test files in ubicity). The other 3 (privacy/mapper/export) await separate PRs after the unit-logic strategy review documented in repos-monorepo PR #12. Numbers: tests/core.test.ts -> deleted (95 LOC TS, 5 tests) tests/idris2/Test/Spec.idr -> new (112 LOC, mirror of cladistic) tests/idris2/CoreTest.idr -> new (~120 LOC, 3 tests + helpers) tests/idris2/Main.idr -> new (aggregator) ubicity-tests.ipkg -> new Justfile -> +`just test-core` target .gitignore -> +build/ Pass rate: 3/3 (run via `just test-core`). 3 of 5 original tests ported. The other 2 deferred with explicit reasons: • "Core - Data persistence" — needs JSON parse + temp-file write. Idris2 base stdlib lacks JSON. Would need either a JSON dep or a custom parser. Defer to a follow-up that pulls in idris2-json or similar. • "Core - ID generation uniqueness" — needs crypto.randomUUID(). Idris2 base lacks crypto. Would need either a crypto dep or a deterministic-RNG mock (which defeats the uniqueness check). Defer. 3 ported: • LearningExperience validation — field presence check on a literal Idris2 record. Defines mirror records (Location, Learner, Experience, LearningExperience) matching the TS interfaces. • Timestamp ISO 8601 shape (T + Z marker check). • Domain array dedup/normalize/filter using nub + map toLower + filter isPrefixOf. Patterns from clade-registry applied: • ascii-only-string-literals-idris2 • one-mega-list-for-testcases-idris2 New pattern noted (worth backfilling in a separate registry PR): • Idris2's `head` requires NonEmpty proof. Use pattern matching on the cons-cell to extract the first element safely: case xs of (h :: _) => h; [] => default Why partial: ubicity's other 3 TS files (privacy/mapper/export) include SHA-256 hashing + JSON parsing + file mapping that need substantial Idris2 dependencies. Strategy review per ESTATE-ROLLOUT "unit-logic" section before porting those. Run via `just test-core`.

github-actions · 2026-05-20T11:19:02Z

🔍 Hypatia Security Scan

Findings: 16 issues detected

Severity	Count
🔴 Critical	7
🟠 High	3
🟡 Medium	6

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.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": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/benchmarks/mapper.bench.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/benchmarks/io.bench.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/benchmarks/validation.bench.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/tests/mapper.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/tests/privacy.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/tests/export.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "getExn on external data -- use pattern matching (5 occurrences, CWE-754)",
    "type": "getexn_on_external",
    "file": "/home/runner/work/ubicity/ubicity/src-rescript/Analysis.res",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…of 4) All 5 mapper tests ported as pure data-manipulation logic — the TS suite builds inline fixtures per test, so no SUT bindings needed. * Hotspot detection — group-by-location + threshold filter * Domain network generation — sorted unordered pairs * Learner journey tracking — filter + ISO-timestamp string sort * Interdisciplinary connections — flat-map of pair strings (ASCII `->`) * Diversity score — cross-multiplied ratio (stays in Nat, no Float) Verified locally: 8 passed, 0 failed (CoreTest 3 + MapperTest 5). Files: * tests/idris2/MapperTest.idr — new (~165 LOC) * tests/idris2/Main.idr — aggregate both suites, sum pass/fail * ubicity-tests.ipkg — add MapperTest module Partial-port status unchanged: privacy.test.ts (161 LOC) + export.test.ts (156 LOC) still await strategy review (privacy needs crypto stubs; export needs JSON parse + file-write — same constraints noted on the two deferred CoreTest cases). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath · 2026-05-20T12:00:27Z

Pushed de7cc67 — adds tests/idris2/MapperTest.idr (5 tests, port of tests/mapper.test.ts).

Local run (Idris2 0.8.0, Chez codegen):
```
=== CoreTest ===
3 passed, 0 failed
=== MapperTest ===
5 passed, 0 failed
=== Total: 8 passed, 0 failed ===
```

All 5 mapper tests are pure data-manipulation (group-by, adjacency-pair, filter, sort, set-uniqueness), so the port needs no SUT bindings — same shape as the TS originals. Notes:

ASCII-only separator -> (per clade-A pattern ascii-only-string-literals-idris2)
Cross-multiplied ratio for diversity score to stay in Nat (no Float)
head-via-cons-cell pattern match for journey index access (the candidate-pattern from this branch already in PR repos-monorepo#11)

Partial-port status: file 2 of 4 ported. Remaining: privacy.test.ts (needs crypto stubs) + export.test.ts (needs JSON parse + file write) — same constraints as the two deferred CoreTest cases. These three (privacy / export / the 2 deferred core cases) still await unit-logic strategy review per panic-free-tests-and-benches/clade-registry/ESTATE-ROLLOUT.adoc.

github-actions · 2026-05-20T12:03:08Z

🔍 Hypatia Security Scan

Findings: 16 issues detected

Severity	Count
🔴 Critical	7
🟠 High	3
🟡 Medium	6

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.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": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/benchmarks/mapper.bench.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/benchmarks/io.bench.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/benchmarks/validation.bench.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/tests/mapper.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/tests/privacy.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/ubicity/ubicity/tests/export.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "getExn on external data -- use pattern matching (5 occurrences, CWE-754)",
    "type": "getexn_on_external",
    "file": "/home/runner/work/ubicity/ubicity/src-rescript/Analysis.res",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…te port 6/11 complete) (#56) Completes the partial port from #55 — ubicity now has all 4 TS test files mirrored in Idris2 (18 tests total, 0 failed locally). ## What's new * **ExportTest.idr** — 5/5 PASS (CSV / GeoJSON struct / DOT graph / Markdown / CSV escaping). All pure string formatting; no SUT bindings required. The Markdown test substitutes the ISO timestamp for the TS `toLocaleDateString()` because the TS test never asserts on the date format itself. * **PrivacyTest.idr** — 5/6 PASS (1 deferred for crypto) - Location fuzzing (Double rounding) - PII removal — substring find/replace rather than regex; preserves the TS invariants (verifies the email/phone tokens are gone + replacements present) - Privacy-level enforcement (`Private | Anonymous | Public` sum type) - Data minimization (record projection) - Shareable-dataset filter - **Deferred**: SHA-256 learner-ID anonymization — same constraint as the two CoreTest deferred cases. Idris2 base lacks crypto. * **Main.idr** — aggregates all 4 suites * **ubicity-tests.ipkg** — registers ExportTest + PrivacyTest ## Local run (Idris2 0.8.0, Chez codegen) \`\`\` === CoreTest === 3 passed, 0 failed === MapperTest === 5 passed, 0 failed === ExportTest === 5 passed, 0 failed === PrivacyTest === 5 passed, 0 failed === Total: 18 passed, 0 failed === \`\`\` ## Estate-rollout impact ubicity moves from "partial — 1 of 4 TS files" → "ports complete — all 4 TS files mirrored, 3 sub-cases deferred for crypto". Each deferred case is documented inline in its module with the precise constraint (crypto / JSON parse). ## Process note Originally drafted on top of `feat/port-core-tests-to-idris2` (PR #55) before that merged. After #55 squash-landed I cherry-picked just the new commit onto a fresh branch off main — avoids the GitHub stacked-PR orphan trap documented in [the auto-memory](https://github.com/hyperpolymath/repos-monorepo/blob/main/panic-free-tests-and-benches/clade-registry/ESTATE-ROLLOUT.adoc). Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath merged commit d1c150a into main May 20, 2026
16 of 24 checks passed

hyperpolymath deleted the feat/port-core-tests-to-idris2 branch May 20, 2026 12:03

hyperpolymath mentioned this pull request May 20, 2026

test: port export.test.ts + privacy.test.ts → Idris2 (4/4 files; estate port 6/11 complete) #56

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

test: port core.test.ts → Idris2 (partial; estate port 6/11, file 1 of 4)#55

test: port core.test.ts → Idris2 (partial; estate port 6/11, file 1 of 4)#55
hyperpolymath merged 2 commits into
mainfrom
feat/port-core-tests-to-idris2

hyperpolymath commented May 20, 2026

Uh oh!

github-actions Bot commented May 20, 2026

Uh oh!

hyperpolymath commented May 20, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented May 20, 2026

Summary

What's ported (3 tests)

What's deferred (2 tests)

Patterns applied

Why partial

Test plan

Uh oh!

github-actions Bot commented May 20, 2026

🔍 Hypatia Security Scan

Uh oh!

hyperpolymath commented May 20, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant