fix: restore the Idris2 0.8 package build

[arena-ai-coding-agent]

Summary

Restores the primary Idris2 0.8.0 package build from the SafeRegex frontier through all 305/305 modules.

Core repairs

• make SafeRegex matching structurally total with bounded search fuel
• make SafeRational recursive calculations fuel-bounded rather than weakening totality
• correct SafeUUID parsing/version handling and SafeVersion comparison behaviour
• enforce SQL identifier, query-length, and parameter-count limits
• keep prebuilt regex source strings canonical across the parser, convenience API, and FFI
• make recursive YAML and TOML rendering/equality visibly total
• add RFC 2544 IPv4 benchmarking classification and exclude that range from global IPv4 addresses

FFI/API drift repairs

• update stale SQL, network, probability, UUID, cron, version, file, OAuth, MCP, and related FFI calls
• handle Idris2 0.8 Data.String.split returning List1
• remove reserved-identifier parse failures (total) and fix a multiline seven-tuple parse failure
• replace non-structural retry recursion with bounded structural fuel
• reject negative FFI values where a cast to Nat could otherwise admit them
• fix missing/incorrect result encodings and exhaustive constructor handling

Proof-claim repair

Several proof modules were silently treating lowercase exported constants as fresh implicit variables. %unbound_implicits off now makes those modules resolve the intended definitions; all six changed proof modules type-check directly.

Verification

Executed locally with Idris2 0.8.0 and threaded Chez Scheme 9.6.4:

• idris2 --build proven.ipkg — PASS (305/305)
• idris2 --install proven.ipkg — PASS
• direct checks of repaired frontier modules, including SafeRegex, SafeSQL, SafeYAML, SafeTOML, SafeNetwork, SafeCron, SafeRetry, and all six changed proof modules — PASS
• git diff --check — PASS

The existing tests.ipkg suite is not green yet: it stops in SafeMathProps on stale test APIs (safeAdd, safeSub, old safeDiv result assumptions, and related names). That test-suite drift predates these source repairs and is intentionally reported here rather than represented as passing.

Scope / follow-up

This PR establishes an honest, compiling primary package baseline. It does not claim that all proof debt is discharged: the repository still contains explicit OWED: obligations, modules outside the primary package need a separate census/remediation pass, and the stale property suite needs reconciliation.

Relates to #184, #203, #204, #208, #209, #210, and #211.

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: f481da20-a443-4756-b5f4-1c261409f79e

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}