Python implementation of the GuardSpine kernel -- evidence-bundle verification and sealing.

Produces byte-identical hashes to the TypeScript reference (@guardspine/kernel) and the Lean 4 formal verification backend. All three implementations use RFC 8785 canonical JSON serialization and are validated against shared golden vectors from guardspine-spec.

v0.2.1 adds optional sanitization metadata (PII/secret redaction attestation). The proof format is unchanged from v0.2.0.

pip install guardspine-kernel

From source:

pip install -e ".[dev]"

Requires Python 3.10+. Single runtime dependency: cryptography>=42.0.0.

from guardspine_kernel import seal_bundle

items = [
    {
        "item_id": "audit-001",
        "content_type": "guardspine/audit_event",
        "content": {"action": "user_login", "user_id": "u123"},
    },
    {
        "item_id": "audit-002",
        "content_type": "guardspine/audit_event",
        "content": {"action": "data_access", "resource": "customers"},
    },
]

result = seal_bundle(items)
print(result.immutability_proof.root_hash)
# sha256:...

from guardspine_kernel import verify_bundle

bundle = {
    "bundle_id": "bundle-001",
    "version": "0.2.0",
    "created_at": "2026-01-15T10:30:00.000Z",
    "items": [...],
    "immutability_proof": {...},
}

result = verify_bundle(bundle)
if result.valid:
    print("Bundle is valid!")
else:
    for error in result.errors:
        print(f"{error.code}: {error.message}")

from guardspine_kernel import canonical_json

# RFC 8785 compliant JSON serialization
obj = {"z": 1, "a": 2}
print(canonical_json(obj))  # {"a":2,"z":1}

The lean_shim module delegates cryptographic operations to a compiled Lean 4 binary via subprocess. This provides formally verified canonical JSON, content hashing, bundle sealing, and bundle verification -- the same operations the Python code performs, but with machine-checked correctness proofs.

• RFC 8785 canonical JSON serialization
• SHA-256 content hashing of canonicalized payloads
• Evidence bundle sealing with hash chains and root hashes
• Bundle verification (hash/chain/root integrity checks)

Signature verification is not yet implemented in Lean. When require_signatures=True, the shim falls back to the Python implementation.

The shim communicates with the Lean binary over stdin/stdout:

guardspine <entrypoint>

• CLI argument = entrypoint name (canonical_json, compute_content_hash, seal_bundle, verify_bundle)
• stdin = JSON payload (one line)
• stdout = {"ok": true, "result": ...} on success, {"ok": false, "error": "..."} on failure
• Exit code = 0 on success, non-zero on crash
• Timeout = 30 seconds per call

1. Build the Lean binary from the guardspine-lean repo:

cd guardspine-lean
lake build guardspine

This produces a native binary (e.g., .lake/build/bin/guardspine on Linux/macOS, .lake\build\bin\guardspine.exe on Windows).

2. Set the environment variable to point at the built binary:

export GUARDSPINE_LEAN_BIN=/path/to/guardspine-lean/.lake/build/bin/guardspine

GUARDSPINE_LEAN_EXE is accepted as an alias.

3. The shim auto-activates when imported. If the env var is unset or the binary is missing, lean_shim raises ImportError. Callers can catch this and fall back to the pure-Python implementation:

try:
    from guardspine_kernel.lean_shim import seal_bundle, verify_bundle
except ImportError:
    from guardspine_kernel import seal_bundle, verify_bundle

tests/test_lean_parity.py runs the same scenarios through both the Lean shim and the Python implementation, asserting byte-identical hashes. These tests skip automatically when the Lean binary is not available.

GUARDSPINE_LEAN_BIN=/path/to/guardspine pytest tests/test_lean_parity.py -v

Security measures matching the TypeScript kernel:

• Seal validation guards: seal_bundle validates item_id and content_type presence before processing, raises ValueError with the offending index
• Max chain items: build_hash_chain rejects inputs exceeding 10,000 items
• Proof version support: both v0.2.0 (current) and legacy (deprecated 3-field chain hash)
• Non-empty items: seal_bundle raises on empty items list
• Version enforcement: verify_bundle rejects versions other than "0.2.0" or "0.2.1"

verify_signatures supports the same algorithms as the TypeScript kernel:

Public keys are passed via public_keys dict (key_id -> PEM string). HMAC secrets via hmac_secret parameter.

• seal_bundle(items, options, bundle_id, version, created_at) -- Seal items into a bundle dict
• build_hash_chain(items, options) -- Build hash chain from ChainInput list
• compute_content_hash(content) -- SHA-256 of canonical JSON ("sha256:<hex>")
• compute_root_hash(chain) -- Root hash over concatenated chain hashes

• verify_bundle(bundle, ...) -- Full bundle verification (fields, content, chain, root, cross-check, signatures)
• verify_hash_chain(chain, ...) -- Verify chain linkage and recompute chain hashes
• verify_root_hash(proof) -- Verify root hash matches chain
• verify_content_hashes(items) -- Verify item content hashes via canonical JSON
• verify_signatures(bundle, ...) -- Verify Ed25519/RSA/ECDSA/HMAC signatures

All error codes match @guardspine/kernel/errors.ts:

pytest tests/test_parity.py -v

Golden vectors are stored in ../guardspine-spec/fixtures/golden-vectors/.

Apache-2.0