feat: plan 12 part C Prop generators, Cardano V3 library, Data conversion traits - #32
Merged
Merged
Conversation
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
MicroProofs
force-pushed
the
plan-12
branch
from
September 25, 2026 21:29
e8867c4 to
d7301b1
Compare
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
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
Part C of plan 12 (plans/12-stdlib.md), on top of #30. Chunk 8 (
Prop) and chunk 11 (Cardano.*) are complete, and the Data conversion traits are consolidated so explicit little-typeToData/FromDataimpls sit beside the Big-only blankets. Base now ships 32 modules. Only chunk 10 (Ast/Derive, needs plan 11) remains. Five commits, six changesets.Versioning: minor bumps for
nash-driverandnash-can; patch fornash-plutus. See.sampo/changesets/.Prop generators (
feat(base): complete Prop generators,feat(base): improve Prop offsets and Int powers,refactor(base): use power table and drop filtering)choice,constant,intBetween,intAtLeast,int,bool,option,listOf,listBetween,tuple2,oneOf,frequency,bytes,bytesBetween,bytesExactly. Arbitrary-precision integers are built fromu64choices; Big/little bounds and weights are normalized;tuple2is written with generatordoand preserves its two replay groups.intmagnitudes choose a small-biased bit width first, replacing the zero-or-huge distribution with useful small nonzero values. ExactexpModIntegerpowers within each eight-bit band;Int.pow2is exposed andInt.powuses its modular fast path for base two.Int.pow2reads a compile-time constant array for small powers. Budget snapshots compare runtime arrays, constant arrays and modular exponentiation; constant lookup wins on CPU and memory.PropHelpers.nashthrough the in-process Base runner: arbitrary-size bounds and offsets, strict replay after rejected wide samples, weights aboveu64, invalid and zero weights, optional draws, byte bounds, isolated replay groups. Counterexample snapshots showlistOf intreducing to[]and[0]and a wide range reducing to its lower bound.Cardano V3 library (
feat(base): add Cardano V3 library)Cardano.Tx,Cardano.Address,Cardano.Value,Cardano.Timeundercrates/nash-driver/base/src/Cardano/. Big constructor layouts follow the Plutus V3 API at revision39981dd7.ScriptInfoandScriptPurposeare separate; V3 transaction IDs are transparent bytes. Validation is explicit Nash and checks recursive wire representations.crates/nash-driver/tests/cardano.rs: seven synthetic Haskell-generated contexts, exact CBOR bytes, malformed contexts, and Haskell interval results (100 intervals, 500 membership checks, 10,000 containment pairs). Fixtures and the executable Haskell oracle live undertests/fixtures/cardano/; the documented regeneration command reproduces all ten CBOR fixtures byte for byte from a fresh pinned checkout.Cardano.Txstub is renamedVestingTxso it no longer collides with the bundled ledger module.Data conversion traits (
refactor(data): consolidate conversion traits)ToData,FromDataand the newDecodeaccept any type; only the conversion blankets andValidaterequireBig. Explicit little-type conversions, includingunit, are legal beside the blankets — this is the first user of the representation-classed heads from feat: plan 12 part B Data, Map, classed impl heads, relational inference #30.Decodereturnsoption, independent ofValidate, and uses ordinary pattern matching; the separateData.Decode/Data.Encodecombinator modules are removed. Malformed UTF-8 decodes toNone. IndependentDecodeinstances cover the Cardano V3 types and reject all seven malformed Haskell contexts without trapping.nash-plutus/src/flat/encode), so large context decoders no longer exhaust the host stack.Docs
docs/stdlib.md,docs/data.md,docs/representation.md,docs/traits.mddescribe the final trait shapes and the generator API;plans/03,06,07,08references updated; SPEC.md marks chunks 1–9 and 11 complete.Remaining for plan 12
Ast/Derive: deferred until plan 11.Test plan
cargo fmt --all -- --checkcargo clippy --all-targets --all-features -- -D warningscargo insta test --workspace --check --unreferenced reject— 3,452 passed, 0 failed, 3 ignored; no pending or unreferenced snapshotscargo run -p nash-cli -- build examples/vesting—Vesting234 Flat bytes,VestingParam238 Flat bytesnash-driver/tests/{bundled_base,base_traits,testing_base,cardano}.rs)