Skip to content

feat: plan 12 part C Prop generators, Cardano V3 library, Data conversion traits - #32

Merged
MicroProofs merged 10 commits into
mainfrom
plan-12
Sep 26, 2026
Merged

MicroProofs merged 10 commits into
mainfrom
plan-12

Conversation

@MicroProofs

Copy link
Copy Markdown
Contributor

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-type ToData / FromData impls 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-driver and nash-can; patch for nash-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)

  • Full generator API: choice, constant, intBetween, intAtLeast, int, bool, option, listOf, listBetween, tuple2, oneOf, frequency, bytes, bytesBetween, bytesExactly. Arbitrary-precision integers are built from u64 choices; Big/little bounds and weights are normalized; tuple2 is written with generator do and preserves its two replay groups.
  • Nonnegative offsets and wide int magnitudes choose a small-biased bit width first, replacing the zero-or-huge distribution with useful small nonzero values. Exact expModInteger powers within each eight-bit band; Int.pow2 is exposed and Int.pow uses its modular fast path for base two.
  • Int.pow2 reads 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.
  • Predicate-filtered generators and their bounded retry loop are removed; valid values are built by composition.
  • PropHelpers.nash through the in-process Base runner: arbitrary-size bounds and offsets, strict replay after rejected wide samples, weights above u64, invalid and zero weights, optional draws, byte bounds, isolated replay groups. Counterexample snapshots show listOf int reducing 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.Time under crates/nash-driver/base/src/Cardano/. Big constructor layouts follow the Plutus V3 API at revision 39981dd7. ScriptInfo and ScriptPurpose are separate; V3 transaction IDs are transparent bytes. Validation is explicit Nash and checks recursive wire representations.
  • Value helpers use the actual Plutus value builtins, normalize Big/little inputs and return little values.
  • 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 under tests/fixtures/cardano/; the documented regeneration command reproduces all ten CBOR fixtures byte for byte from a fresh pinned checkout.
  • The vesting example's Cardano.Tx stub is renamed VestingTx so it no longer collides with the bundled ledger module.

Data conversion traits (refactor(data): consolidate conversion traits)

  • ToData, FromData and the new Decode accept any type; only the conversion blankets and Validate require Big. Explicit little-type conversions, including unit, 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.
  • Decode returns option, independent of Validate, and uses ordinary pattern matching; the separate Data.Decode / Data.Encode combinator modules are removed. Malformed UTF-8 decodes to None. Independent Decode instances cover the Cardano V3 types and reject all seven malformed Haskell contexts without trapping.
  • Flat term encoding is iterative (nash-plutus/src/flat/encode), so large context decoders no longer exhaust the host stack.
  • Codegen source fixtures use the driver's dependency sorter instead of a hand-ordered module list.

Docs

  • docs/stdlib.md, docs/data.md, docs/representation.md, docs/traits.md describe the final trait shapes and the generator API; plans/03, 06, 07, 08 references updated; SPEC.md marks chunks 1–9 and 11 complete.

Remaining for plan 12

  • Chunk 10 Ast / Derive: deferred until plan 11.

Test plan

  • cargo fmt --all -- --check
  • cargo clippy --all-targets --all-features -- -D warnings
  • cargo insta test --workspace --check --unreferenced reject — 3,452 passed, 0 failed, 3 ignored; no pending or unreferenced snapshots
  • cargo run -p nash-cli -- build examples/vesting — Vesting 234 Flat bytes, VestingParam 238 Flat bytes
  • Bundled Base compiled and executed in-process (nash-driver/tests/{bundled_base,base_traits,testing_base,cardano}.rs)
  • Haskell CBOR fixtures reproduced byte for byte from the pinned Plutus revision

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>
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
MicroProofs merged commit 16c4546 into main Sep 26, 2026
9 checks passed
@MicroProofs
MicroProofs deleted the plan-12 branch September 26, 2026 02:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant