refactor(provenbridge): collapse placeholder to proven re-exports#76
Merged
Conversation
Closes the idaptik side of hyperpolymath/proven#8 (transferred from hyperpolymath/affinescript#58). Removes the 1658-line placeholder that mirrored five proven Safe* modules locally, replacing it with direct re-exports + idaptik-domain extractors built on proven. Net: 1443 lines deleted, 206 added (file 1658 -> 625 lines). Gated on: hyperpolymath/proven#9, which adds the small surface gaps this PR consumes (Proven.SafeJson.Access.field, Proven.SafeMath. divChecked, and the move of Proven.SafeInput into the Proven namespace and ipkg manifests). Marked draft until proven#9 merges. What changed in ProvenBridge.idr: - Replace local `JValue` type + 1600-char fuel-based JSON parser placeholder with `import public Proven.SafeJson.{,Parser,Access}`. All extractor signatures rename `JValue` -> `JsonValue`, `jGet` -> `get`, `jAsString` -> `asString`, etc. `parseJsonString` -> `parse`. - Replace local Int64 overflow stubs + `gameMath{Add,Sub,Mul,Div}` + `clampGameValue` + `percentOfTotal` with `import public Proven. SafeMath` and rewrite the idaptik-specific combinators (`clampHP`, `clampAlertLevel`, `applyDamage`, `critDamage`, `alertThresholdReached`) on top of `clamp`, `subChecked`, `mulChecked`, `percentOf` directly. - Replace local `game{CharAt,Substring,Trim,Truncate,...}` with `import public Proven.SafeString` and rewrite `validateLevelName`, `formatDeviceLabel`, `sanitiseTerminalInput` on top of `trim`, `isAscii`, `truncateWithEllipsis`, `padRight`, `truncate`. - Replace local `GameByte`/`GameBytes`/`gameConstantTimeEq` and hex/hash placeholders with `import public Proven.SafeCrypto` and rewrite `verifyAuthToken` on top of `hexToBytes` + `constantTimeEq`. Drop `gameSyncTag` (was a `gameHmac _ _ _ = []` stub providing zero integrity); callers should reach for `Proven.SafeCrypto.hmac` directly once that has a real FFI backing. - Replace local `Game{InputResult,CharClass,InputBuffer,Keystroke}` + all `gameValidate*` / `gameHandleKey` with `import public Proven.SafeInput` and rewrite `terminalHackBuffer`, `numericEntryBuffer`, `hexEntryBuffer`, `handleAndValidateInt`, `handleAndValidateNat` on top of `filteredBuffer`, `handleKey`, `validateInt`, `validateNat`. Naming change inside ProvenBridge: - The local `Extracted` type's `Ok` constructor is renamed to `Got`. Why: `import public Proven.SafeJson` transitively re-exports `Proven.Core.Result.Ok`, which would clash. A `%hide Proven.Core. Result.Ok` directive is also added so the rename is sufficient even if a future Idris2 disambiguator gets pickier. Out of scope (intentional): - LessonsMD L1's `Validation[E,A]` stdlib-floor proposal: the `Extracted` type here is the same shape (accumulating-error applicative-flavour) and would naturally retire to a future `Proven.Validation` if/when that lands. Local module additions to idaptik-ums.ipkg: - Uncomment `depends = proven`. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
|
Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits. |
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
Draft — blocked on hyperpolymath/proven#9. Closes the idaptik side of proven#8 (transferred from
hyperpolymath/affinescript#58).Collapses
idaptik-ums/src/abi/ProvenBridge.idrfrom the 1658-line placeholder into ~5import publiclines + the idaptik-domain extractors that the placeholder was hiding underneath. Net: −1443 / +206 (file goes 1658 → 625 lines).The placeholder mirrored five proven modules locally so idaptik could compile in isolation. After this PR:
Proven.SafeJson+Proven.SafeJson.Parser+Proven.SafeJson.Accessreplace the localJValuetype, the fuel-based JSON parser, and thejGet/jAsString/etc. accessors.Proven.SafeMathreplaces the local Int64 overflow stubs,gameMath{Add,Sub,Mul,Div},clampGameValue, andpercentOfTotal. idaptik-specific combinators (clampHP,clampAlertLevel,applyDamage,critDamage,alertThresholdReached) are rewritten on top of proven'sclamp/subChecked/mulChecked/percentOf.Proven.SafeStringreplaces the localgameCharAt/gameSubstring/gameTrim/gameTruncate/gameSplit/gameIsAscii/gameParseNat/gameParseInt.validateLevelName,formatDeviceLabel,sanitiseTerminalInputare rewritten on top of proven'strim/isAscii/truncateWithEllipsis/padRight/truncate.Proven.SafeCryptoreplaces the localGameByte/GameBytes/gameConstantTimeEq/gameHexToBytes/gameBytesToHex+ hash stubs.verifyAuthTokenis rewritten on top ofhexToBytes+constantTimeEq.gameSyncTagwas a stub returning[](zero integrity) — dropped; callers should useProven.SafeCrypto.hmacdirectly once that has a real FFI backing.Proven.SafeInputreplaces the localGame{InputResult,CharClass,InputBuffer,Keystroke}andgameValidate*/gameHandleKey.terminalHackBuffer,numericEntryBuffer,hexEntryBuffer,handleAndValidateInt,handleAndValidateNatrewritten on top offilteredBuffer/handleKey/validateInt/validateNat.Naming change inside ProvenBridge
The local
Extractedtype's constructorOkis renamed toGot.import public Proven.SafeJsontransitively re-exportsProven.Core.Result.Ok, which clashes. A defensive%hide Proven.Core.Result.Okdirective is also added so the rename remains sufficient even if Idris2's disambiguator gets pickier.Everything else inside
Extractedis unchanged (Errs,mapExtracted,combineExtracted,extractedToEither,requireField,optionalField).Build dependency
idaptik-ums/idaptik-ums.ipkguncommentsdepends = proven. This makes the package requireprovenfrom the local pack collection / installed library set.Out of scope (intentional)
Validation[E, A]stdlib-floor proposal. TheExtractedtype here is the same shape (accumulating-error, applicative-flavour) and would naturally retire to a futureProven.Validationif/when that lands. Tracked there.?missionHole/?physicalHole/empty lists, matching pre-PR state.Test plan
idris2 --check idaptik-ums.ipkgpasses locallySTAPEL-VOLL-AUDIT.mdworkflow — ProvenBridge usage is currently confined to its own module (verified:grep -r 'ProvenBridge' src/finds no external callers in idaptik-ums)🤖 Generated with Claude Code