[Amaury Chamayou (achamayou)]

Motivation

Move recovery-share generation and reconstruction into a small Rust computational core with an extracted Lean refinement, while retaining the original C++ implementation and full bidirectional share compatibility. No issue is linked.

Implementation summary

• Add the dependency-free ccf-shamir crate, which forbids unsafe code and implements field arithmetic, polynomial evaluation, share-coordinate assignment, and interpolation.
• Keep entropy sampling and C++ object handling in src/crypto/sharing_rust.cpp, separate from the raw-pointer bridge in src/rust/src/shamir.rs. Recovery writes directly into the caller's output array instead of returning an additional secret-bearing array.
• Reproduce the production core's Lean model with pinned Aeneas/Charon tooling and prove arithmetic safety, sharing and recovery refinement to CSLib, and preservation of the output on recovery errors. CI checks extraction reproducibility and the kernel/axiom dependency closure of all project declarations.
• Generate the C ABI header from the Rust declarations with pinned cbindgen, and run the bridge tests under Miri's Stacked Borrows and Tree Borrows models in CI. Generated lint exceptions cover only the C++ modernization and enum-size checks that conflict with the C ABI.
• Retain the original C++ backend in src/crypto/sharing.cpp. USE_RUST_SHAMIR defaults to ON; OFF selects C++. The unselected backend is linked separately into sharing_test for interoperability checks.
• Build both Lean import roots before formatting, including the Generated root imported by ListDeclarations.lean.
• Document the compatibility requirement, backend selector, proof boundary, and reproduction commands in the Shamir README.

Safety and compatibility

The C++ API, 44-byte serialized share layout, byte order, field, ten-limb representation, coefficient sampling, HKDF derivation, input reduction, and ignoring shares beyond the recovery threshold are preserved. Valid shares must recover in both directions with identical secrets and derived keys; independently generated sharings are not interchangeable.

The retained C++ arithmetic comes from main revision 41645c55675d246605b2e26d45f4282de3d83fba. Its only runtime changes reject zero recovery thresholds and generation counts reaching the field characteristic, matching the Rust backend. No consensus or KV logic is changed.

The FFI bridge rejects null, misaligned, overlapping, and address-wrapping buffers and reports named errors. Allocation validity, initialization, lifetime, and concurrent-access obligations remain with the caller. The Lean proof boundary excludes that unsafe bridge, the C++ adapter, OpenSSL, the real entropy source, machine-code timing and erasure, the compiler, and the extractor. The C++ backend is not covered by the Rust refinement proofs.

Validation

Local validation has passed six standalone Rust compatibility tests, four Rust FFI tests, and the complete sharing_test with each backend selected in a Debug build with BUILD_TESTS=ON and LONG_TESTS=ON. Both configurations exercise serialized-share exchange in both directions, all threshold-sized subsets of seven-share distributions, full shares, recovered bytes, and derived keys. Archive inspection confirmed that ccfcrypto contains only the selected backend's C++ translation unit in each configuration.

The generated header reproduces locally with cbindgen 0.29.4 and passes C11 and C++23 layout checks. A before/after regression with clang-tidy 18.1.8 reproduces the original included-header failures and passes with the regenerated header under the unchanged full lint configuration. The lint follow-up changes only generated comments, not ABI declarations. Targeted formatting, release-note, prose, ASCII, and workflow-routing checks have also passed.

On the latest test-only correction, cmake --build /tmp/ccf-shamir-final-build-2fb27b85 --target sharing_test -j2 and ctest --test-dir /tmp/ccf-shamir-final-build-2fb27b85 -R '^sharing_test$' --no-tests=error --output-on-failure --timeout 600 both passed with USE_RUST_SHAMIR=ON and OFF. The complete test took 26.75 seconds and 18.62 seconds respectively. These Debug builds used Clang 21, BUILD_TESTS=ON, LONG_TESTS=ON, and CLANG_TIDY=OFF; lint regressions were checked independently.

On revision 356630e72, CI passed the full Lean models/proofs job, including export and kernel/axiom checking of all 436 Shamir project declarations and their dependencies. The kernel accepted the solution using only propext, Quot.sound, and Classical.choice. Rust extraction, both Miri modes, generated-header reproducibility, VMSS Virtual B/C, ACI SNP Genoa, and the CLA check also passed. The generated-header lint and Lean import-root failures from the preceding revision were resolved.

The remaining Virtual A failure on 356630e72 was Clang 18.1.8/libstdc++ 13.2.0 deducing function-type members for std::pair in the interoperability test. A local minimal reproducer using the same Clang parser and Azure Linux standard-library headers reproduced both original compilation errors; explicit function addresses passed. Revision e9146cb8d applies that correction without changing production code, test coverage, or assertions.

On e9146cb8d, the complete Continuous Integration workflow passed: Virtual A/B/C and ACI SNP Genoa are green. Virtual A passed ./scripts/ci-checks.sh, the full Debug build with clang-tidy, C++ case-scope checks, Python package tests, ./tests.sh --output-on-failure -L unit -j16 (65/65 tests, including sharing_test), and ./tests.sh --timeout 360 --output-on-failure -L bucket_a -j2 (3/3 tests, including lts_compatibility). Rust extraction, both Miri modes, generated-header reproducibility, and CLA also passed on this revision.

The only pending check on e9146cb8d is the full Lean models/proofs rerun; it passed on 356630e72, and this revision changes only C++ test function addresses. Long, sanitizer, and benchmark jobs were skipped, not passed. Required checks must finish successfully before merge.

Local limitations remain distinct from CI results. The complete local tidy-enabled build, cmake --build /tmp/ccf-shamir-ci-build-2fb27b85 --target sharing_test -j2, encountered a clang-tidy 18.1.8 crash in unchanged vendored fmt/format.h; the complete tidy-enabled CI build now passes. Full network targets and Miri were not rerun locally. A separate sphinx-build --fail-on-warning -b html doc doc/html build was not run locally. The Windows checkout's CRLF scripts affect direct WSL checks.

The changelog includes the introducing upstream PR reference (#8614).