Skip to content

tests: add pendant sumtree roundtrip wip#66

Merged
joom merged 2 commits intobloomberg:mainfrom
CharlesCNorton:pendant-sumtree-roundtrip-wip
Mar 16, 2026
Merged

tests: add pendant sumtree roundtrip wip#66
joom merged 2 commits intobloomberg:mainfrom
CharlesCNorton:pendant-sumtree-roundtrip-wip

Conversation

@CharlesCNorton
Copy link
Contributor

Summary

  • add one WIP test derived from the high-level multi-number and top-cord summation path in khipu.v
  • package dependent digit vectors, proof-carrying pendants, a heterogenous sigma ledger, and nested sumtree validation into a single extracted module
  • wire the new case into tests/wip/dune

Source Shape

  • reduced from the theorem surface around multi-number roundtripping and hierarchical pendant summation
  • keeps decode_multi_encode_multi_roundtrip, certified pendants carrying a roundtrip witness, a heterogenous Ledger, PendantGroup, and nested SumTree validation
  • includes concrete sample data for multi-number decoding, top-equals-sum checks, leaf-total checks, tree depth, and ledger population

Why This Case

  • exercises dependent Vector.t payloads together with erased proof fields, sigma packaging, optional folds, and nested list/tree structure in one module
  • the .t.cpp is non-empty and checks extracted wrappers directly
  • the failure comes from generated C++ reached by the certified-pendant and sumtree path, not from theorem-only surface

Batch Size

  • wip: +1

New WIP Tests (1)

  • pendant_sumtree_roundtrip

Validation

  • 1 WIP alias failed in a fresh ext4 WSL worktree after rerunning to materialize generated files
  • failure occurs in generated C++ during compilation
  • the emitted code breaks on the dependent optional-fold path, with generated fold_right lambdas over std::optional<...> failing the MapsTo constraints together with std::nullopt versus optional return-type mismatches in the extracted decode_multi, group_sums_validb, and sumtree_leaf_total path

@joom joom merged commit 36f0aa9 into bloomberg:main Mar 16, 2026
1 check passed
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.

2 participants