#CryptoAssert — Cryptocurrency Compliance & Security Assertion Library

A production-grade, three-tier assertion template library for cryptocurrency compliance verification, bridging business logic, protocol specifications, and mathematical proofs through compile-time static dispatch and theorem-proven safety guarantees.

#Table of Contents

1. Overview
2. Architecture
3. Project Structure
4. Design Philosophy
5. Layer 1: Formal Proof Layer
6. Layer 2: Protocol Specification Layer
7. Layer 2 (Extended): Cryptography Primitives
8. Layer 2 (Extended): E2E Production Verifier
9. Layer 2 (Extended): Lemma Runtime Bridge
10. Layer 2 (Extended): BigMath & UInt256
11. Layer 2 (Extended): Additional Modules
12. Layer 3: Business Assertion Layer
13. Type System Reference
14. Trait Reference
15. Error Model
16. Quick Start
17. API Reference
18. Extending the Library
19. Testing & Quality Assurance
20. Security Considerations
21. Build, Prove & Test
22. CI/CD
23. Comparison with Industry Alternatives
24. License

#Overview

#Core Capabilities

• Multi-chain address audit — 9 blockchain address formats (Bitcoin P2PKH/P2SH/SegWit/Taproot, Ethereum, EIP-55, Solana, Tron, Cosmos)
• Signature scheme compatibility — 5 signature algorithms (ECDSA secp256k1, Ed25519, Sr25519, BLS12-381, SchnorrSecp256k1) cross-matched with address types
• Real cryptographic verification — Production-grade ECDSA secp256k1 (FIPS 186-4), SHA-256, Keccak-256, Base58Check, Bech32/Bech32m, EIP-712, RLP
• Transaction fund conservation — Multi-input/output balance verification with overflow protection
• Replay attack prevention — Real per-transaction nonce / chain_id field validation (consumed-nonce replay and cross-chain replay both rejected), plus EIP-155 style signature binding: chain_id and nonce are serialized into the signing message, so a signed transaction whose chain or nonce is tampered with fails ECDSA verification
• Smart contract safety audit — Mint/burn/pause/upgrade control verification
• Cross-chain bridge audit — Multisig threshold verification (multisig_threshold-of-total_validators: zero / over-count / non-majority thresholds are rejected, sub-BFT thresholds warned), validator set size, amount boundaries, and chain ID validation
• Sparse Merkle Tree verification — Inclusion and exclusion proofs with 256-layer precomputed nil-hash table
• Formal theorem proving — 14 lemmas (plus 2 predicates) checked by moon prove via Why3 + Z3, 14 goals proved; the CI prove job fails if any lemma cannot be proved
• Structured error model — 10 suberror variants with typed payloads

#Architecture

┌─────────────────────────────────────────────────────────────────┐
│                    BUSINESS LAYER                                │
│  (business/)                                                     │
│                                                                  │
│  fn[V: Trait] assert_*(verifier: V, ...) -> Result raise E      │
│                                                                  │
│  • address_assert.mbt   (3 assertions)                          │
│  • security_assert.mbt  (6 assertions)                          │
│                                                                  │
│  Consumers inject concrete Verifier implementations.            │
│  Dispatch resolved at compile time — zero runtime overhead.     │
└──────────────────────────┬──────────────────────────────────────┘
                           │ trait delegation
                           ▼
┌─────────────────────────────────────────────────────────────────┐
│                  PROTOCOL LAYER                                  │
│  (protocol/)                                                     │
│                                                                  │
│  ┌─ Traits & Specs ──────────────────────────────────────────┐  │
│  │ • AddressVerifier trait     (6 methods)                    │  │
│  │ • TransactionVerifier trait (5 methods)                    │  │
│  │ • SecurityVerifier trait    (5 methods)                    │  │
│  │ • DefaultVerifier struct    (9 blockchain implementations) │  │
│  │ • SimpleSecurityVerifier    (full SecurityVerifier impl)   │  │
│  └────────────────────────────────────────────────────────────┘  │
│                                                                  │
│  ┌─ Cryptography Primitives ─────────────────────────────────┐  │
│  │ • ecdsa_secp256k1.mbt  — ECDSA FIPS 186-4 + RFC 6979      │  │
│  │ • sha256.mbt           — SHA-256 (FIPS 180-4)             │  │
│  │ • keccak256.mbt        — Keccak-256 (Ethereum)            │  │
│  │ • base58.mbt           — Base58 + Base58Check             │  │
│  │ • bech32.mbt           — Bech32 (BIP 173) + Bech32m       │  │
│  │ • eip712.mbt           — EIP-712 typed structured data    │  │
│  │ • rlp.mbt              — RLP decoder (Ethereum)           │  │
│  │ • smt.mbt              — Sparse Merkle Tree verifier      │  │
│  └────────────────────────────────────────────────────────────┘  │
│                                                                  │
│  ┌─ Production Verifiers ────────────────────────────────────┐  │
│  │ • e2e_verifier.mbt      — Full E2E transaction pipeline    │  │
│  │ • transfer_runtime.mbt  — Lemma → Runtime bridges          │  │
│  │ • bigmath.mbt           — BigInt amount operations         │  │
│  │ • uint256.mbt           — 256-bit unsigned integer         │  │
│  └────────────────────────────────────────────────────────────┘  │
│                                                                  │
│  All traits use self: Self → compile-time static dispatch.      │
│  No dyn dispatch, no vtable, no runtime NotImplemented.         │
└──────────────────────────┬──────────────────────────────────────┘
                           │ mathematical invariants
                           ▼
┌─────────────────────────────────────────────────────────────────┐
│                    PROOF LAYER                                   │
│  (proof/transfer_proof.mbtp, "proof-enabled" package)            │
│                                                                  │
│  2 predicates:                                                   │
│    • fund_conservation_inv                                       │
│    • transfer_state_invariant                                    │
│                                                                  │
│  14 lemmas (Why3/Z3 proven — one goal each, 14 goals total):     │
│    • no_inflation_lemma          • value_monotonic_lemma         │
│    • overflow_safe_lemma         • transfer_correctness_theorem  │
│    • nonce_replay_rejection_lemma• chain_id_binding_lemma        │
│    • multisig_quorum_intersection_lemma                          │
│    • model_balance_lemma         • uint256_add_no_overflow_lemma │
│    • uint256_sub_no_underflow_lemma                              │
│    • uint256_mul_no_overflow_lemma                               │
│    • bridge_soundness_lemma      • bridge_conservation_lemma     │
│    • bigint_extended_conservation_lemma                          │
│                                                                  │
│  Each lemma carries explicit proof_assert steps.                 │
│  All theorems validated by `moon prove` (real execution in CI).  │
└─────────────────────────────────────────────────────────────────┘

#Project Structure

crypto_assert/
├── moon.mod                              # Package manifest (Kali-Leo/moonbit-CryptoAssert v0.2.0)
├── moon.pkg                              # Root package declaration
├── README.md                             # This file
├── LICENSE                               # Apache 2.0
├── proposal.md                           # Project proposal (OSC 2026)
├── acceptance_review.md                  # OSC 2026 acceptance self-review
├── .gitignore
│
├── proof/                                # ═══ Formal Proof Layer ═══
│   ├── moon.pkg                          # options("proof-enabled": true)
│   └── transfer_proof.mbtp               # 2 predicates + 14 lemmas, proved by `moon prove`
│
├── examples/                             # ═══ Runnable Examples ═══
│   ├── moon.pkg                          # Executable package
│   └── main.mbt                          # `moon run examples --target native` (run in CI)
│
├── protocol/                             # ═══ Protocol Layer ═══
│   ├── moon.pkg                          # Package config
│   │
│   │   ┌── Traits & Specs ──────────────────────────────────────┐
│   ├── assert_result.mbt                 # AssertionResult enum, suberror AssertError (10 variants)
│   ├── address_spec.mbt                  # AddressVerifier trait, DefaultVerifier, AddressType (9),
│   │                                     #   SignatureScheme (5), HashScheme (6), PrecisionSpec,
│   │                                     #   AddressFormatSpec, ChecksumType, AddressLengthRange
│   ├── transaction_spec.mbt              # TransactionVerifier trait, TransactionSpec, TxInputSpec,
│   │                                     #   TxOutputSpec, FeeSpec, TokenTransferSpec,
│   │                                     #   TxValidationCode (9), TxStatus (5)
│   ├── security_spec.mbt                 # SecurityVerifier trait, SecurityAssertResult,
│   │                                     #   ReplayProtectionSpec, TokenSafetySpec, BridgeSpec,
│   │                                     #   ContractSafetyMode (5)
│   ├── simple_security_verifier.mbt      # SimpleSecurityVerifier — full SecurityVerifier impl
│   │                                     #   with BigInt-based numerical checks
│   │
│   │   ┌── Cryptography Primitives ─────────────────────────────┐
│   ├── ecdsa_secp256k1.mbt               # ECDSA over secp256k1 (FIPS 186-4)
│   │                                     #   with RFC 6979 deterministic nonce
│   ├── sha256.mbt                        # SHA-256 (FIPS 180-4), SHA-256d
│   ├── keccak256.mbt                     # Keccak-256 (Ethereum, distinct from SHA3-256)
│   ├── base58.mbt                        # Base58 + Base58Check (Bitcoin alphabet, O(1) lookup)
│   ├── bech32.mbt                        # Bech32 (BIP 173) + Bech32m (BIP 350) + Cosmos verify
│   ├── eip712.mbt                        # EIP-712 typed structured data hashing
│   ├── rlp.mbt                           # RLP decoder (Ethereum Yellow Paper Appendix B)
│   ├── smt.mbt                           # Sparse Merkle Tree (256-layer, precomputed nil-hashes)
│   │
│   │   ┌── Production Verifiers & Bridges ──────────────────────┐
│   ├── e2e_verifier.mbt                  # E2E production verifier — full tx pipeline,
│   │                                     #   ECDSA signing & verification, fund conservation,
│   │                                     #   replay protection, contract/bridge audit
│   ├── transfer_runtime.mbt              # Lemma → Runtime bridges (6 lemma-corresponding functions)
│   ├── bigmath.mbt                       # BigInt amount parsing & operations (4 functions)
│   ├── uint256.mbt                       # UInt256 — 256-bit unsigned integer (add/sub/mul/div)
│   │
│   │   ┌── Tests ───────────────────────────────────────────────┐
│   ├── spec_easy_test.mbt                # Unit tests
│   └── spec_difficult_test.mbt           # Integration tests
│
└── business/                             # ═══ Business Assertion Layer ═══
    ├── moon.pkg                           # Package config
    ├── address_assert.mbt                 # 3 assertion functions: address, sig-compat, tx-sig
    ├── security_assert.mbt                # 6 assertion functions: balance, replay, amount, fee,
    │                                      #   contract-safety, bridge-security
    └── business_test.mbt                  # QuickCheck property bombardment

#Design Philosophy

#1. Static Dispatch over Dynamic Dispatch

#2. Theorem-Proven Invariants

#3. Trait-Based Extension

#4. Structured Error Model

#5. Separation of Proof and Runtime

#Layer 1: Formal Proof Layer

options(
  "proof-enabled": true,
)

# Prerequisites: Why3 + at least one SMT solver on PATH
#   WHY3DATA / WHY3LIB   → why3 --print-datadir / --print-libdir
#   Z3PATH               → optional explicit z3 binary location
moon prove
# Kali-Leo/moonbit-CryptoAssert/proof
#   Succeeded: 14 goals proved
# Summary:
#   1 of 1 packages proved

#Modeling Note (read this before trusting any proof)

1. Every lemma that depends on non-negativity or upper bounds states those facts as explicit proof_require premises — real input constraints, never the conclusion restated as a premise.
2. Range facts are enforced at runtime by BigInt checks (check_fee_nonnegative_bigint, transfer_runtime.mbt, bigmath.mbt).

#Predicates

#Lemmas & Theorems (14 goals, all proved)

moon prove

#Why This Matters in Production

#Layer 2: Protocol Specification Layer

#AddressVerifier Trait

pub trait AddressVerifier {
  address_format_spec(self: Self, AddressType) -> AddressFormatSpec
  valid_address_length_range(self: Self, AddressType) -> AddressLengthRange
  validate_checksum(self: Self, AddressType, String) -> Bool
  address_precision(self: Self, SignatureScheme) -> PrecisionSpec
  hash_output_length(self: Self, HashScheme) -> UInt
  is_valid_hash_size(self: Self, Bytes, HashScheme) -> Bool
}

#TransactionVerifier Trait

pub trait TransactionVerifier {
  validate_transaction(self: Self, TransactionSpec) -> TxValidationCode
  verify_signature(self: Self, SignatureVerifySpec) -> Bool
  compute_txid(self: Self, TransactionSpec) -> String
  estimate_fee(self: Self, TransactionSpec, String) -> FeeSpec
  validate_token_transfer(self: Self, TokenTransferSpec) -> TxValidationCode
}

#SecurityVerifier Trait

pub trait SecurityVerifier {
  check_replay_protection(self: Self, TransactionSpec, ReplayProtectionSpec) -> SecurityAssertResult
  check_contract_safety(self: Self, TokenSafetySpec) -> SecurityAssertResult
  check_bridge_security(self: Self, BridgeSpec) -> SecurityAssertResult
  validate_amount_range(self: Self, String, String, String) -> SecurityAssertResult
  check_fee_ratio(self: Self, String, String, String) -> SecurityAssertResult
}

#Layer 2 (Extended): Cryptography Primitives

#ECDSA secp256k1 — protocol/ecdsa_secp256k1.mbt (443 lines)

• Elliptic curve: y² = x³ + 7 over F_p with SEC 2 secp256k1 parameters
• Key generation: Deterministic private key derivation via SHA-256
• Signing: ECDSA signature with RFC 6979 deterministic nonce (HMAC-SHA256 based)
• Verification: Full ECDSA verification with curve point validation
• Low-s enforcement: BIP 62 compliant low-s values
• Point operations: Point addition, doubling, scalar multiplication (double-and-add)
• All big integer arithmetic uses MoonBit BigInt for arbitrary precision

// Generate a key pair — returns Option, unwrap with match
let (priv_hex, pub_hex) = match @protocol.generate_key_pair(seed_bytes) {
  Some(pair) => pair
  None => abort("key generation failed")
}

// Sign a message — returns Option
let signature = @protocol.ecdsa_sign(sha256(message), private_key_bytes)

// Verify a signature
let valid = @protocol.ecdsa_verify(message_hash, signature, public_key_bytes)

#SHA-256 — protocol/sha256.mbt (169 lines)

#Keccak-256 — protocol/keccak256.mbt (193 lines)

• Keccak-f[1600] permutation (24 rounds)
• State: 1600 bits = 25 × 64-bit lanes
• Rate: 1088 bits = 136 bytes
• FixedArray temporaries to minimize GC pressure inside the round loop
• Includes keccak256_to_nibbles for EIP-55 address checksumming
• Verified against official known-answer vectors (keccak256("") = c5d24601…, keccak256("abc") = 4e03657a…) in the test suite

#Base58 / Base58Check — protocol/base58.mbt (161 lines)

• Bitcoin alphabet (excludes 0, O, I, l)
• O(1) character lookup via precomputed 128-slot table
• base58_check_verify — full Base58Check checksum validation (SHA-256d)
• base58_check_validate — address validation with version byte and payload length checks

#Bech32 / Bech32m — protocol/bech32.mbt (233 lines)

• Bech32 (SegWit v0, checksum constant = 1)
• Bech32m (Taproot, checksum constant = 0x2bc830a3)
• BCH polynomial division with generator coefficients
• cosmos_verify for Cosmos/IBC ecosystem addresses
• Case-insensitive lookup with mixed-case rejection

#EIP-712 — protocol/eip712.mbt (229 lines)

• compute_type_hash — keccak256(encodeType(def))
• encode_and_hash_struct — structHash = keccak256(typeHash || padded fields)
• compute_eip712_message_hash — messageHash = keccak256(\x19\x01 || domainHash || structHash)
• Field type support: address, uint256, bytes32, string, bool
• parse_type_definition with bracket-aware field splitting
• Left-padding to 32 bytes per EIP-712 spec

#RLP — protocol/rlp.mbt (177 lines)

• Single-pass cursor traversal (no redundant slicing)
• Supports short/long strings and short/long lists
• rlp_decode, rlp_as_string, rlp_as_list API
• bytes_to_hex helper for RLP-to-hex conversion

#Sparse Merkle Tree — protocol/smt.mbt (171 lines)

• SMTProof struct with side nodes, bit mask, and value
• verify_smt_inclusion — verify key/value exists under root hash
• verify_smt_exclusion — verify key does not exist in tree
• Precomputed 257-entry nil-hash table (zero-leaf to depth-256)
• Proof validation: checks that non-empty side nodes match expected nil-hashes

#Layer 2 (Extended): E2E Production Verifier

#Transaction Signing & Verification

// Sign a transaction with ECDSA secp256k1 — returns Option
let signed_tx = match @protocol.sign_transaction(tx, private_key_hex) {
  Some(t) => t
  None => abort("signing failed")
}

// Verify a signed transaction's signature.
// The signing message serializes txid, chain_id, nonce, inputs, outputs and
// fee — tampering with chain_id or nonce after signing invalidates the
// signature (EIP-155 style binding).
let valid = @protocol.verify_signed_transaction(signed_tx)

#Fund Conservation

// BigInt-based fund conservation verification (no overflow limit)
let conserved = @protocol.verify_fund_conservation(tx)

#Replay Protection

// verify_replay_protection(tx, expected_chain_id, min_locktime,
//                          expected_nonce? : UInt64? = None)
let result = @protocol.verify_replay_protection(
  tx,
  1, // expected_chain_id — tx.chain_id must equal this (0 disables the match)
  0, // min_locktime
  expected_nonce=Some(7UL), // next valid account nonce
)
// Returns: Safe | Warning(msg) | Unsafe(msg)
// Real field checks:
//   tx.chain_id missing / zero / ≠ expected_chain_id → Unsafe (cross-chain replay)
//   tx.nonce missing                                 → Unsafe
//   tx.nonce < expected_nonce                        → Unsafe (consumed-nonce replay)
//   tx.nonce > expected_nonce                        → Warning (nonce gap)

#Contract Safety Audit

let result = @protocol.audit_contract_safety(
  has_mint, mint_controlled, has_pause, safety_modes
)

#Bridge Security Audit

let result = @protocol.audit_bridge_security(
  contract_address,
  target_chain_id,
  min_amount,
  max_amount,
  min_validators,
  multisig_threshold, // required signatures
  total_validators,   // validator set size
)
// Multisig threshold rules (see multisig_quorum_intersection_lemma):
//   threshold == 0 / > total / not a majority (2t ≤ n) → Unsafe
//   below BFT quorum ⌊2n/3⌋+1 (3t < 2n+1)              → Warning

#Full Transaction Validation Pipeline

let result = @protocol.full_tx_validation_pipeline(
  tx,
  expected_chain_id,
  min_locktime,
  amount_min,
  amount_max,
  fee_max_ratio,
  expected_nonce=Some(7UL), // optional
)
// Pipeline:
//   1. ECDSA signature verification
//   2. Fund conservation check
//   3. Replay protection (real chain_id / nonce checks)
//   4. Amount range validation (all outputs)
//   5. Fee ratio check

#TransactionVerifier Trait Implementation

#Layer 2 (Extended): Lemma Runtime Bridge

1. Implements a runtime check exactly equivalent to its corresponding lemma
2. References the lemma name in docstrings via proof_require
3. Uses BigInt internally for overflow-safe comparisons

#Layer 2 (Extended): BigMath & UInt256

#BigMath — protocol/bigmath.mbt (96 lines)

#UInt256 — protocol/uint256.mbt (325 lines)

#Layer 2 (Extended): Additional Modules

#SimpleSecurityVerifier — protocol/simple_security_verifier.mbt (439 lines)

• Replay protection: real tx.chain_id validation (missing / zero / mismatch vs expected_chain_id → Unsafe), real tx.nonce validation (missing → Unsafe; < expected_nonce → Unsafe replay; > expected_nonce → Warning gap), locktime requirement, nonce-reuse warning
• Contract safety: Mint control audit, burn control verification, pause capability with ownership/timelock guards, single-owner pattern detection
• Bridge security: multisig threshold verification (multisig_threshold-of-total_validators: zero / over-count / non-majority → Unsafe, sub-BFT ⌊2n/3⌋+1 → Warning, backed by multisig_quorum_intersection_lemma), validator set size analysis, amount range consistency, address format validation, chain ID validation
• Amount range: BigInt-based min/max boundary checks with structured results
• Fee ratio: Three-tier classification (Normal/Elevated/Excessive) with scaled BigInt comparison

#Layer 3: Business Assertion Layer

#Address & Signature Assertions (address_assert.mbt)

#Security Assertions (security_assert.mbt)

#Balance Verification

1. Parse all input/output amount strings with overflow detection.
2. Accumulate with overflow guard: a + b ≥ a check at each addition.
3. Verify total_in ≡ total_out + fee with overflow check on total_out + fee.
4. Raise AmountImbalance with exact values if conservation fails.

#Type System Reference

#Enumerated Types

#AddressType — 9 blockchain address formats

#SignatureScheme — 5 cryptographic signature algorithms

#HashScheme — 6 hash algorithms

#ChecksumType — 4 checksum strategies

#TxStatus — 5 transaction lifecycle states

#TxValidationCode — 9 transaction validation outcomes

#SecurityAssertResult — 3-tier security verdict

#ContractSafetyMode — 5 smart contract safety controls

#Struct Types

#Trait Reference

#AddressVerifier

#TransactionVerifier

#SecurityVerifier

#Error Model

#suberror AssertError — 10 variants

#Handling Errors

let verifier = @protocol.DefaultVerifier::new()
let result = try @business.assert_address_format(
  verifier,
  "0x5aAeb6053F3E94C9b9A09f33669435E7Ef1BeAed", // official EIP-55 test vector
  @protocol.AddressType::EthEip55,
) catch {
  @protocol.AssertError::InvalidPrefix(address, expected_prefix) =>
    // wrong prefix — e.g., missing "0x"
    ...
  @protocol.AssertError::InvalidLength(address, min, max) =>
    // address too short or too long
    ...
  @protocol.AssertError::InvalidCharacter(address, c) =>
    // illegal character in address
    ...
  @protocol.AssertError::ChecksumMismatch(address) =>
    // checksum validation failed
    ...
  _ =>
    // unexpected error
    ...
}

#Quick Start

#Prerequisites

• MoonBit toolchain (latest stable)
• Why3 and Z3 (only required for moon prove; set WHY3DATA/WHY3LIB from why3 --print-datadir / why3 --print-libdir, optionally Z3PATH)

#Run the Examples

moon run examples --target native

#Adding CryptoAssert to Your Project

moon add Kali-Leo/moonbit-CryptoAssert

import {
  "Kali-Leo/moonbit-CryptoAssert@0.2.0",
}

import {
  "Kali-Leo/moonbit-CryptoAssert/protocol",
  "Kali-Leo/moonbit-CryptoAssert/business",
}

#Example 1: Address Format Validation

/// Validate an Ethereum EIP-55 checksummed address
/// (from examples/main.mbt, section [5])
let verifier = @protocol.DefaultVerifier::new()
try {
  let _ = @business.assert_address_format(
    verifier,
    "0x5aAeb6053F3E94C9b9A09f33669435E7Ef1BeAed", // official EIP-55 vector
    @protocol.AddressType::EthEip55,
  )
  println("checksummed address → Valid")
} catch {
  _ => println("checksummed address → rejected")
}
// A corrupted (all-lowercase) form of the same address is rejected with
// ChecksumMismatch. Note: the widely-circulated example address
// 0x742d35Cc… actually has an INVALID EIP-55 checksum — this library now
// correctly rejects it.

#Example 2: Signature Scheme Compatibility (Pure Function)

/// ECDSA + Bitcoin P2PKH is compatible; BLS12-381 + Bitcoin is NOT
try {
  let ok = @business.assert_sig_scheme_compatible(
    @protocol.SignatureScheme::EcdsaSecp256k1,
    @protocol.AddressType::BtcP2pkh,
  )
  // ok == AssertionResult::Valid
  let _ = @business.assert_sig_scheme_compatible(
    @protocol.SignatureScheme::Bls12381,
    @protocol.AddressType::BtcP2pkh,
  )
} catch {
  @protocol.AssertError::IncompatibleScheme(_s, _a) =>
    // _s == Bls12381, _a == BtcP2pkh
    println("incompatible pair rejected")
  _ => println("unexpected error")
}

#Example 3: E2E Production Transaction Pipeline

/// Full E2E validation: sign → verify sig → fund conservation → replay → fee
/// (from examples/main.mbt, section [4])
let result = @protocol.full_tx_validation_pipeline(
  signed_tx,
  1, // expected_chain_id
  0, // min_locktime
  "1", // amount_min
  "100000000000000000000", // amount_max
  "5", // fee_max_ratio (%)
  expected_nonce=Some(7UL),
)
// result == Safe | Warning(msg) | Unsafe(msg)

#Example 4: ECDSA Signature Generation & Verification

/// (from examples/main.mbt, sections [1] and [4])
/// Generate key pair — Option, unwrap with match
let seed : Bytes = b"cryptoassert-demo-seed-32bytes!!"
let (priv_hex, pub_hex) = match @protocol.generate_key_pair(seed) {
  Some(pair) => pair
  None => abort("key generation failed")
}

/// Sign a transaction (tx carries nonce: Some(7UL), chain_id: Some(1)) — Option
let signed_tx = match @protocol.sign_transaction(tx, priv_hex) {
  Some(t) => t
  None => abort("signing failed")
}

/// Verify the signed transaction
let valid = @protocol.verify_signed_transaction(signed_tx)
// valid == true

/// The signature binds chain_id and nonce: re-targeting the same signed tx to
/// another chain makes verification fail
// verify_signed_transaction(tx_with_chain_id_56) == false

/// Verify fund conservation
let conserved = @protocol.verify_fund_conservation(signed_tx)
// conserved == true

#Example 5: Replay Protection — Real nonce / chain ID Checks

/// (from examples/main.mbt, section [2]; signed_tx carries
///  nonce: Some(7UL), chain_id: Some(1))

/// Legitimate: chain matches, nonce equals the account's next nonce
let ok = @protocol.verify_replay_protection(
  signed_tx, 1, 0, expected_nonce=Some(7UL),
)
// ok == Safe

/// Replay attack: account nonce has advanced to 8 — replaying the old
/// nonce-7 transaction is rejected
let replayed = @protocol.verify_replay_protection(
  signed_tx, 1, 0, expected_nonce=Some(8UL),
)
// replayed == Unsafe("Nonce 7 already consumed (account nonce is 8) — replay detected")

/// Cross-chain replay: tx is bound to chain 1, submitted to chain 56
let wrong_chain = @protocol.verify_replay_protection(signed_tx, 56, 0)
// wrong_chain == Unsafe("Chain ID mismatch: tx carries 1, expected 56 — cross-chain replay")

#Example 6: Bridge Multisig Audit

/// (from examples/main.mbt, section [3])
/// 7-of-9 satisfies the BFT quorum ⌊2n/3⌋+1 = 7 → Safe
let safe_bridge = @protocol.audit_bridge_security(
  "0x1234567890abcdef1234567890abcdef12345678",
  137, "1000", "100000000000",
  7, // min validators
  7, // multisig threshold
  9, // total validators
)
// safe_bridge == Safe

/// 5-of-9 is a majority but below the BFT quorum → Warning
/// 4-of-9 is not even a majority — minority collusion could move funds → Unsafe

#Example 7: BigInt Fund Conservation (Production Recommended)

/// BigInt version — no overflow limit, safe for Ethereum-scale amounts
/// check_transfer_bigint(input_amounts, output_amounts, fee_str) — positional
let conserved = @protocol.check_transfer_bigint(
  ["1000000000000000000000", "500000000000000000000"],
  ["1499000000000000000000", "1000000000000000000"],
  "1000000000000000000",
)
// conserved == true (1500 = 1499 + 1 + 1)

#Example 8: Sparse Merkle Tree Verification

/// Verify inclusion proof
let valid = @protocol.verify_smt_inclusion(
  root_hash,
  key_bytes,
  value_bytes,
  proof,
)

/// Verify exclusion proof (key not in tree)
let absent = @protocol.verify_smt_exclusion(
  root_hash,
  key_bytes,
  proof,
)

#API Reference

moon doc

#Extending the Library

#Implementing a Custom AddressVerifier

struct PolkadotVerifier {}

impl @protocol.AddressVerifier for PolkadotVerifier with
  address_format_spec(self, ty) {
    match ty {
      // ... implement all 9 AddressType variants
    }
  }

// Also required:
//   valid_address_length_range(self, ty)
//   validate_checksum(self, ty, address)
//   address_precision(self, scheme)
//   hash_output_length(self, scheme)
//   is_valid_hash_size(self, hash, scheme)

#Adding New Chain Support

1. Implement AddressVerifier for your chain's address format.
2. Implement TransactionVerifier for your chain's transaction structure.
3. Implement SecurityVerifier for your chain's security model.
4. Write QuickCheck property tests (see business/business_test.mbt for patterns).
5. Optionally, extend transfer_proof.mbtp with chain-specific invariants and prove them with moon prove.

#Testing & Quality Assurance

#Test Coverage

#Test Execution Summary

• 90 tests total across all test files
• All 90 tests pass with moon test --target native and moon test --target wasm-gc
• moon check --deny-warn passes with zero warnings

#QuickCheck Property Bombardment

#Test Execution

# Type checking
moon check

# Run all tests
moon test --target native

# Strict mode
moon test --deny-warn

# Update test snapshots
moon test --update

# Run formal theorem proofs (requires Why3 + Z3)
moon prove

#Security Considerations

#Compile-Time Guarantees

1. Zero NotImplemented: All traits use self: Self with fn[V: Trait] syntax. The compiler rejects any incomplete trait implementation at compile time. This eliminates a class of vulnerabilities where runtime "not implemented" branches could be exploited in smart contract contexts.

2. Overflow Protection: The overflow_safe_lemma is proven by Z3 (under its explicit non-negativity and bound premises — see the Layer 1 modeling note) and enforced at runtime in bridging functions. Every accumulation is guarded by overflow checks.

3. Fund Conservation: The conservation lemmas are verified by the SMT solver for all values satisfying their stated proof_require premises. Both UInt64 and BigInt runtime implementations are provided; the BigInt path enforces the range premises on real data.

#Numeric Domain: UInt64 vs BigInt

• bigmath.mbt: BigInt-based amount operations (no overflow limit)
• uint256.mbt: Full 256-bit unsigned integer (add/sub/mul/div)
• check_transfer_bigint: Production-recommended BigInt verification

#Supported Cryptographic Primitives

#Attack Surface Analysis

#Production Hardening Recommendations

1. Use BigInt for high-value transfers — Prefer check_transfer_bigint over UInt64-based functions for Ethereum and EVM-compatible chains.

2. Use a secure random number generator — The QuickCheck LCG in tests is deterministic by design. Production key generation should use OS-provided CSPRNGs.

3. Add chain-specific invariants — Extend proof/transfer_proof.mbtp with chain-specific theorems (e.g., staking conservation, slashing invariants).

4. Audit custom verifiers — While the trait system guarantees completeness, the semantic correctness of custom SecurityVerifier implementations is the integrator's responsibility.

#Build, Prove & Test

#Development Commands

# ─── Type Checking ──────────────────────────────────
moon check                           # Full project type check
moon check --deny-warn               # Strict mode

# ─── Testing ────────────────────────────────────────
moon test --target native            # Run all 90 tests
moon test --deny-warn                # Strict mode
moon test --update                   # Update test snapshots

# ─── Formal Theorem Proving (Why3 + Z3 required) ───
moon prove                           # Verify all 14 lemmas in proof/transfer_proof.mbtp

# ─── Build & Run Examples ───────────────────────────
moon build                           # Build the package
moon run examples --target native    # Run the executable examples
moon build --target wasm-gc          # Build for wasm-gc backend

# ─── Documentation ──────────────────────────────────
moon doc                             # Generate API documentation

# ─── Formatting ─────────────────────────────────────
moon fmt                             # Format all source files

# ─── Publishing ─────────────────────────────────────
moon publish --dry-run               # Check publish readiness

# ─── Full Validation Pipeline ───────────────────────
moon check --deny-warn && moon prove && moon test --target native && moon run examples --target native

#CI/CD

#CI Pipeline (.github/workflows/ci.yml) — 4 jobs, all real

#Published Package

• Package: Kali-Leo/moonbit-CryptoAssert v0.2.0
• Registry: mooncakes.io
• Repository: GitHub
• License: Apache 2.0

#Comparison with Industry Alternatives

#Changelog

#0.2.0 (2026-07-30)

• Real replay protection: TransactionSpec gains nonce : UInt64? and chain_id : UInt?; ReplayProtectionSpec gains expected_nonce / expected_chain_id. check_replay_protection now validates the actual field values (missing/zero/mismatched chain ID → Unsafe; missing nonce → Unsafe; consumed nonce → Unsafe; nonce gap → Warning). chain_id and nonce are serialized into the signing message and txid, so signatures cryptographically bind chain and sequence number.
• Real bridge multisig auditing: BridgeSpec gains multisig_threshold / total_validators; check_bridge_security rejects zero, over-count, and non-majority thresholds and warns below the BFT quorum ⌊2n/3⌋+1.

• Proofs moved to a dedicated proof-enabled package (proof/); moon prove translates them to WhyML and runs Why3 + Z3 for real — 14 goals proved, and a false lemma makes the build fail. The CI prove job asserts the goal count.
• Lemma set made honest under the idealized-integer model (explicit range premises; unsound fee_nonnegative_lemma removed) and extended with nonce_replay_rejection_lemma, chain_id_binding_lemma, and multisig_quorum_intersection_lemma backing the new runtime checks.

• Fixed Keccak-256 ρ+π permutation table pairing — the implementation now passes official known-answer vectors, which makes EIP-55 checksum validation actually work (previously it rejected every valid address); validated against the official EIP-55 test vectors.
• Fixed address charset validation incorrectly checking prefix characters (0x, bc1, cosmos1), which mis-rejected all prefixed addresses.
• Unified the business-layer signing-message serialization with the protocol layer (previously assert_tx_signature could never verify a transaction signed by sign_transaction).

• New runnable examples/ package mirroring the README Quick Start; CI builds and runs it and asserts on its output.
• README fully synchronized with the published API (all snippets compile against 0.2.0).
• CI expanded to 4 real jobs: strict check + format, build + run examples, test (native + wasm-gc), prove (Why3/Z3 with asserted goal count).
• Test suite grown from 62 to 90 tests.

• TransactionSpec, ReplayProtectionSpec, BridgeSpec construction requires the new fields; verify_replay_protection, audit_bridge_security, and full_tx_validation_pipeline have new signatures (hence 0.2.0).

#License

#Contributing

1. Implement missing trait methods — the compiler will tell you which ones.
2. Add new chain support by implementing all three traits.
3. Extend proof/transfer_proof.mbtp with chain-specific invariants and prove them.
4. Add tests for new compatibility pairs or cryptographic primitives.
5. Run moon check --deny-warn && moon prove && moon test --target native before submitting.