kernel: pure decision-logic crate for Aeneas verification

Carve the pure decision logic out of opencsv-core into a new
opencsv-kernel crate, shaped for the Aeneas toolchain:

- loops only (no iterators/closures in the verified paths), no serde,
  no dyn, no RNG
- hashing behind an opaque boundary (hash::hash_bind/hash_batch delegate
  byte-identically to opencsv-core's anchor::binding/batch::batch_commit)
- interop module (excluded from translation) converts core types to
  kernel types

Equivalence with opencsv-core is pinned by tests/kernel_equiv.rs
(8 tests: binding byte-identity, well_formed on all variants, batch
occurrence, first-occurrence double-spend/copy-grief, supply
mint/redeem accounting).

charon --preset=aeneas --opaque opencsv_kernel::hash
  --exclude opencsv_kernel::interop
translates the crate with no errors, and aeneas generates Lean that
builds; the by-value match on *record inside the supply loop is the one
Aeneas-driven idiom (by-reference matches in loops are unsupported).

Author: posix4e

Cargo.toml

@@ -2,6 +2,7 @@
 resolver = "2"
 members = [
     "crates/opencsv-core",
+    "crates/opencsv-kernel",
     "crates/opencsv-pcd",
     "crates/opencsv-cli",
     "crates/opencsv-signal",

crates/opencsv-kernel/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "opencsv-kernel"
+description = "Pure decision-logic kernel of opencsv-core, written for Aeneas verification (loops only, no serde/dyn/RNG, hash behind an opaque boundary)"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+
+[dependencies]
+opencsv-core = { path = "../opencsv-core" }
+
+[dev-dependencies]
+
+[features]
+default = []

crates/opencsv-kernel/README.md

@@ -0,0 +1,48 @@
+# opencsv-kernel
+
+The **pure decision logic** of `opencsv-core`, rewritten in the shape the
+Aeneas spike validated for Rust→Lean 4 translation:
+
+- **loops only** — no iterator adapters (`zip` / `chunks` / `enumerate` /
+  `position` / `filter` / `map`): those trip charon's associated-type
+  lifting and have no model in aeneas's Lean library;
+- **no serde, no `dyn` traits, no RNG, no generics** beyond plain numeric /
+  byte-array types;
+- the Poseidon hash stays behind an **opaque boundary** (`hash` module) —
+  the same cryptographic boundary the Lean model
+  (`formal/OpenCsv/Interfaces.lean: bindHash`) takes as an axiom.
+
+## Scope (phase 1)
+
+| kernel item | mirrors (opencsv-core) |
+|---|---|
+| `binding::binding` | `anchor::binding` + `Digest::to_anchor` |
+| `record::Record::well_formed` | `anchor::AnchorRecord::well_formed` (+ `payload_slots`) |
+| `scan::first_occurrence` | `chain::AnchorChain::first_nullifier_occurrence` (mock semantics) |
+| `batch::batch_occurrence` | `batch::envelope_occurrence` |
+| `audit::supply` | `audit::supply` (mint dedupe by `mint_commit`) |
+
+Semantics are **byte-identical** to `opencsv-core` — this is a rewrite, not
+a redesign. `tests/kernel_equiv.rs` ports the relevant `opencsv-core` test
+scenarios and asserts kernel ≡ core on shared cases.
+
+## Boundary
+
+- `types`, `binding`, `record`, `scan`, `batch`, `audit` are the
+  **verification surface**: plain data in, plain data out.
+- `hash` is the **crypto boundary**: the only place the kernel calls into
+  `opencsv-core` (`anchor::binding`, `batch::batch_commit`). For the
+  Aeneas run it is translated as an opaque (uninterpreted) function —
+  exactly the model's `bindHash` axiom.
+- `interop` (conversions from `opencsv-core` types) is glue for callers and
+  tests; it is **not** part of the verification surface (excluded from
+  translation).
+- `scan::first_occurrence` takes the entries in **canonical chain order**
+  (block height, then in-block position — the caller's responsibility,
+  same contract as `AnchorChain`) and returns the *index* of the first
+  well-formed entry; the entry's `Location` is read off the input. The
+  core returns the location directly — equivalent by construction.
+
+Wiring the kernel into `opencsv-core` (replacing the duplicated logic) is a
+later decision; for now the two coexist and the equivalence tests pin them
+together.

crates/opencsv-kernel/src/audit.rs

@@ -0,0 +1,87 @@
+//! Public supply audit (mirror of `opencsv-core::audit::supply`, paper
+//! §4.9):
+//!
+//! ```text
+//! supply(asset_id, h) =  Σ V  over MINT anchors with this asset_id up to h
+//!                      − Σ V  over REDEEM anchors with this asset_id up to h
+//! ```
+//!
+//! Anchor records are copyable bytes, so identical MINT anchors are
+//! **deduplicated**: each distinct `mint_commit` counts once per asset.
+
+use crate::record::Record;
+use crate::types::{AssetId24, Location, MintCommit};
+
+/// Failure modes of [`supply`] (mirror of `audit::SupplyError`).
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum SupplyError {
+    /// Redemptions exceed mints at the requested height — the anchored
+    /// stream is inconsistent (only possible on an adversarial/corrupt
+    /// chain view).
+    NegativeSupply,
+}
+
+/// Does `seen` already contain `commit`? (Linear scan — no `HashSet` in
+/// the verification surface.)
+fn seen_contains(seen: &[MintCommit], commit: &MintCommit) -> bool {
+    let mut i = 0usize;
+    while i < seen.len() {
+        if seen[i] == *commit {
+            return true;
+        }
+        i += 1;
+    }
+    false
+}
+
+/// Compute the public per-asset supply at `height` (paper §4.9), over the
+/// anchor records with location at or below `height`, in canonical order.
+///
+/// Mirror of `audit::supply`: MINT records with a matching asset count
+/// once per distinct `mint_commit`; REDEEM records with a matching asset
+/// subtract; everything else is ignored. Fails with
+/// [`SupplyError::NegativeSupply`] if redemptions exceed mints.
+pub fn supply(
+    anchors: &[(Location, Record)],
+    asset_id: &AssetId24,
+    height: u64,
+) -> Result<u64, SupplyError> {
+    let mut seen_mints: Vec<MintCommit> = Vec::new();
+    let mut total: i128 = 0;
+    let mut i = 0usize;
+    while i < anchors.len() {
+        let (location, record) = &anchors[i];
+        if location.height <= height {
+            // Note: match by value (Aeneas chokes on by-reference matches
+            // inside loops); `Record` is `Copy`, so this is free.
+            match *record {
+                Record::Mint {
+                    asset_id: record_asset,
+                    value,
+                    mint_commit,
+                } => {
+                    if record_asset == *asset_id && !seen_contains(&seen_mints, &mint_commit) {
+                        seen_mints.push(mint_commit);
+                        total += i128::from(value);
+                    }
+                }
+                Record::Redeem {
+                    asset_id: record_asset,
+                    value,
+                    ..
+                } => {
+                    if record_asset == *asset_id {
+                        total -= i128::from(value);
+                    }
+                }
+                _ => {}
+            }
+        }
+        i += 1;
+    }
+    if total < 0 || total > i128::from(u64::MAX) {
+        Err(SupplyError::NegativeSupply)
+    } else {
+        Ok(total as u64)
+    }
+}

crates/opencsv-kernel/src/batch.rs

@@ -0,0 +1,41 @@
+//! Batch occurrence test (mirror of `opencsv-core::batch::envelope_occurrence`).
+
+use crate::binding::{binding, truncate24};
+use crate::hash;
+use crate::types::{Ctx, Payload, RawNf};
+
+/// Is `raw_nf` an occurrence of this batch? Returns the envelope index of
+/// its payload (mirror of `batch::envelope_occurrence`):
+///
+/// - the envelope must carry exactly `count` payloads;
+/// - the header's `batch_commit` must recompute over the envelope
+///   (`H("batch" ∥ P_1 ∥ … ∥ P_n ∥ ctx)`, truncated);
+/// - some payload must equal `H("bind" ∥ raw_nf ∥ ctx)` (truncated).
+///
+/// `count` and `batch_commit` come from the batch header record of the
+/// transaction the envelope was taken from; `ctx` is the transaction's
+/// funding ctx. Loop-based (Aeneas-compatible shape).
+pub fn batch_occurrence(
+    count: u8,
+    batch_commit: &Payload,
+    envelope: &[Payload],
+    ctx: &Ctx,
+    raw_nf: &RawNf,
+) -> Option<u32> {
+    if envelope.len() != count as usize {
+        return None;
+    }
+    let committed = truncate24(&hash::hash_batch(envelope, ctx));
+    if committed != *batch_commit {
+        return None;
+    }
+    let bound = binding(raw_nf, ctx);
+    let mut i = 0usize;
+    while i < envelope.len() {
+        if envelope[i] == bound {
+            return Some(i as u32);
+        }
+        i += 1;
+    }
+    None
+}

crates/opencsv-kernel/src/binding.rs

@@ -0,0 +1,22 @@
+//! The transaction-context binding (mirror of `opencsv-core::anchor`).
+
+use crate::hash;
+use crate::types::{Ctx, Payload, RawNf};
+
+/// The 24-byte anchor-carrying prefix of a digest (`Digest::to_anchor`).
+pub fn truncate24(digest: &[u8; 32]) -> Payload {
+    let mut out = [0u8; 24];
+    let mut i = 0usize;
+    while i < 24 {
+        out[i] = digest[i];
+        i += 1;
+    }
+    out
+}
+
+/// `P = H("bind" ∥ raw ∥ ctx)` truncated to the on-chain payload
+/// (`opencsv_core::anchor::binding` + `Digest::to_anchor`).
+pub fn binding(raw: &RawNf, ctx: &Ctx) -> Payload {
+    let digest = hash::hash_bind(raw, ctx);
+    truncate24(&digest)
+}

crates/opencsv-kernel/src/hash.rs

@@ -0,0 +1,29 @@
+//! The cryptographic boundary of the kernel: the only functions that call
+//! into the scheme's Poseidon2 hash (via `opencsv-core`). For the Aeneas
+//! translation these are marked **opaque** — the Lean side sees them as
+//! uninterpreted functions, exactly the model's `bindHash` axiom
+//! (`formal/OpenCsv/Interfaces.lean`).
+//!
+//! These wrappers are byte-identical delegations, NOT reimplementations.
+
+use crate::types::{Ctx, Payload, RawNf};
+
+/// `H("bind" ∥ raw_nf ∥ ctx)` as a full 32-byte digest
+/// (`opencsv_core::anchor::binding`).
+pub fn hash_bind(raw_nf: &RawNf, ctx: &Ctx) -> [u8; 32] {
+    *opencsv_core::anchor::binding(
+        &opencsv_core::Digest::from_bytes(*raw_nf),
+        ctx,
+    )
+    .as_bytes()
+}
+
+/// `H("batch" ∥ P_1 ∥ … ∥ P_n ∥ ctx)` as a full 32-byte digest
+/// (`opencsv_core::batch::batch_commit`).
+pub fn hash_batch(payloads: &[Payload], ctx: &Ctx) -> [u8; 32] {
+    let truncated: Vec<opencsv_core::TruncatedDigest> = payloads
+        .iter()
+        .map(|p| opencsv_core::TruncatedDigest(*p))
+        .collect();
+    *opencsv_core::batch::batch_commit(&truncated, ctx).as_bytes()
+}

crates/opencsv-kernel/src/interop.rs

@@ -0,0 +1,69 @@
+//! Conversions from `opencsv-core` types to kernel types — glue for
+//! callers and the equivalence tests. **Not** part of the verification
+//! surface (excluded from the Aeneas translation; see crate README).
+
+use opencsv_core::anchor::AnchorRecord;
+use opencsv_core::chain::{AnchorChain, AnchorLocation, AnchorRef};
+
+use crate::record::Record;
+use crate::types::{Entry, Location};
+
+/// Convert a location.
+pub fn location(location: &AnchorLocation) -> Location {
+    Location {
+        height: location.height,
+        position: location.position,
+    }
+}
+
+/// Convert an anchor record (layout-compatible; see `crate::record`).
+pub fn record(record: &AnchorRecord) -> Record {
+    match record {
+        AnchorRecord::Mint {
+            asset_id,
+            value,
+            mint_commit,
+        } => Record::Mint {
+            asset_id: asset_id.0,
+            value: *value,
+            mint_commit: mint_commit.0,
+        },
+        AnchorRecord::Xfer { payloads } => Record::Xfer {
+            payloads: [payloads[0].0, payloads[1].0],
+        },
+        AnchorRecord::XferCompressed {
+            nullifier_commit, ..
+        } => Record::XferCompressed {
+            payload: nullifier_commit.0,
+        },
+        AnchorRecord::BatchHeader {
+            count,
+            batch_commit,
+        } => Record::BatchHeader {
+            count: *count,
+            batch_commit: batch_commit.0,
+        },
+        AnchorRecord::Redeem {
+            asset_id,
+            value,
+            payload,
+        } => Record::Redeem {
+            asset_id: asset_id.0,
+            value: *value,
+            payload: payload.0,
+        },
+    }
+}
+
+/// Resolve an anchor reference to a kernel entry (record, ctx, location),
+/// using the chain's `anchor_at` / `ctx_at` lookups. Returns `None` if
+/// either lookup fails.
+pub fn entry_at<C: AnchorChain>(chain: &C, anchor_ref: &AnchorRef) -> Option<Entry> {
+    let record = chain.anchor_at(anchor_ref)?;
+    let ctx = chain.ctx_at(anchor_ref)?;
+    Some(Entry {
+        record: self::record(&record),
+        ctx,
+        location: location(&anchor_ref.location),
+    })
+}

crates/opencsv-kernel/src/lib.rs

@@ -0,0 +1,23 @@
+//! Pure decision-logic kernel of opencsv-core (see crate README).
+//!
+//! The **verification surface** — `types`, `binding`, `record`, `scan`,
+//! `batch`, `audit` — is written for Aeneas translation: loops only, no
+//! serde/dyn/RNG, no generics beyond plain byte arrays and integers. The
+//! `hash` module is the cryptographic boundary (translated as opaque).
+//! `interop` is glue outside the verification surface.
+
+pub mod audit;
+pub mod batch;
+pub mod binding;
+pub mod hash;
+pub mod interop;
+pub mod record;
+pub mod scan;
+pub mod types;
+
+pub use audit::{supply, SupplyError};
+pub use batch::batch_occurrence;
+pub use binding::{binding, truncate24};
+pub use record::Record;
+pub use scan::first_occurrence;
+pub use types::{AssetId24, Ctx, Entry, Location, MintCommit, Payload, RawNf};