feat: idrisiser Phase 1 — interface parser, Idris2 codegen, Zig bridge, tests

Complete implementation of idrisiser's core pipeline:

Manifest (redesigned):
- [project] with name and module-prefix
- [[interfaces]] array: name, source, format (openapi/c-header/protobuf/type-sig),
  verify list, pre/postconditions, invariants
- [proofs] config: totality, round-trip, QTT, search depth
- [idris2] config: flags, codegen backend, packages

Parser (codegen/parser.rs — 500 LOC):
- OpenAPI: extract paths as function contracts from YAML
- C header: parse function declarations, extract params/return types
- Protocol Buffers: extract RPC method signatures
- Type signatures: parse Idris2-style type annotations
- Graceful fallback when source files not found
- Auto-generate preconditions for pointer params (NULL checks)

Idris2 codegen (codegen/idris2.rs — 460 LOC):
- Generate complete .idr modules with %default total
- Contract types: Result, Params records, Pre/Post predicates
- Proof obligations: Totality, PreSatisfied, PostSatisfied, RoundTrip
- FFI declarations matching Zig bridge exports
- Safe wrappers enforcing contracts at the type level
- AllProofsComplete witness composing all proof obligations

Zig bridge (codegen/zig_bridge.rs — 220 LOC):
- Generate C-ABI exports for each function contract
- Delegate to user's original implementation
- Lifecycle functions (init/shutdown)
- Result codes matching Idris2 ABI

Also generates: .ipkg for Idris2 build system, build.sh script

Rust ABI (abi/mod.rs — 170 LOC):
- FfiResult, InterfaceFormat, ContractClause, ProofObligation
- ProofKind enum (Totality, Termination, Invariant, TypeSafety, Resource, RoundTrip)
- VerificationSummary with from_obligations constructor

Example: examples/user-api/ with OpenAPI + C header interfaces

Tests: 20 passing (6 unit + 4 parser + 10 integration)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

Cargo.lock

@@ -0,0 +1,26 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Example idrisiser manifest — verify a REST API and a C library.
+
+[project]
+name = "example-project"
+module-prefix = "Example.Verified"
+
+[[interfaces]]
+name = "user-api"
+source = "openapi.yaml"
+format = "openapi"
+preconditions = ["valid_auth_token"]
+postconditions = ["status < 500"]
+
+[[interfaces]]
+name = "core-lib"
+source = "include/core.h"
+format = "c-header"
+verify = ["process_item", "reduce"]
+invariants = ["heap_intact"]
+
+[proofs]
+require-totality = true
+round-trip-proofs = true
+qtt-tracking = false
+search-depth = 100

examples/user-api/idrisiser.toml

@@ -0,0 +1,14 @@
+/* Minimal C header for testing idrisiser parsing */
+
+#ifndef CORE_H
+#define CORE_H
+
+#include <stddef.h>
+#include <stdint.h>
+
+int process_item(void* input, size_t len);
+int reduce(void* a, void* b, void* out);
+void* allocate_buffer(size_t size);
+void free_buffer(void* buf);
+
+#endif

examples/user-api/include/core.h

@@ -0,0 +1,30 @@
+# Minimal OpenAPI spec for testing idrisiser parsing
+openapi: "3.0.0"
+info:
+  title: User API
+  version: "1.0.0"
+paths:
+  /users:
+    get:
+      summary: List all users
+      responses:
+        "200":
+          description: OK
+  /users/{id}:
+    get:
+      summary: Get user by ID
+      parameters:
+        - name: id
+          in: path
+          required: true
+      responses:
+        "200":
+          description: OK
+        "404":
+          description: Not found
+  /users/{id}/posts:
+    get:
+      summary: List posts for a user
+      responses:
+        "200":
+          description: OK

examples/user-api/openapi.yaml

@@ -1,8 +1,166 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
-// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 //
-// ABI module for idrisiser.
-// Rust-side types mirroring the Idris2 ABI formal definitions.
-// The Idris2 proofs guarantee correctness; this module provides runtime types.
+// ABI module — Rust-side types mirroring the Idris2 ABI formal definitions.
+//
+// The Idris2 proofs in src/interface/abi/*.idr guarantee correctness at compile time.
+// This Rust module provides runtime representations for:
+//   - Interface formats and contracts
+//   - Proof obligations and their discharge status
+//   - Verification results
+
+use serde::{Deserialize, Serialize};
+
+/// FFI result codes. Must match Idrisiser.ABI.Types.Result.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[repr(i32)]
+pub enum FfiResult {
+    Ok = 0,
+    Error = 1,
+    InvalidParam = 2,
+    OutOfMemory = 3,
+    NullPointer = 4,
+    ProofFailure = 5,
+}
+
+/// Supported interface formats.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum InterfaceFormat {
+    OpenApi,
+    CHeader,
+    Protobuf,
+    TypeSig,
+}
+
+/// A contract clause (precondition, postcondition, or invariant).
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct ContractClause {
+    /// The kind of clause.
+    pub kind: ClauseKind,
+    /// Human-readable description of the clause.
+    pub description: String,
+    /// Whether this clause has been proven (discharged).
+    pub discharged: bool,
+}
+
+/// Kind of contract clause.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum ClauseKind {
+    Precondition,
+    Postcondition,
+    Invariant,
+}
+
+/// A proof obligation generated from a contract.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct ProofObligation {
+    /// Which function this obligation belongs to.
+    pub function_name: String,
+    /// The kind of proof required.
+    pub kind: ProofKind,
+    /// The Idris2 type signature of the proof.
+    pub type_signature: String,
+    /// Whether the proof has been discharged (verified).
+    pub discharged: bool,
+}
+
+/// Kinds of proofs that idrisiser generates.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum ProofKind {
+    /// Function covers all inputs and terminates.
+    Totality,
+    /// Recursive operations have a decreasing measure.
+    Termination,
+    /// A state invariant holds before and after.
+    Invariant,
+    /// Input/output types match the declared schema.
+    TypeSafety,
+    /// Linear/affine resources are properly tracked (QTT).
+    Resource,
+    /// Serialise then deserialise yields the original value.
+    RoundTrip,
+}
+
+/// Summary of a verification run.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct VerificationSummary {
+    /// Number of interfaces verified.
+    pub interfaces: usize,
+    /// Number of functions across all interfaces.
+    pub functions: usize,
+    /// Total proof obligations generated.
+    pub total_obligations: usize,
+    /// Obligations successfully discharged.
+    pub discharged: usize,
+    /// Obligations remaining (not yet proven).
+    pub remaining: usize,
+    /// Whether all obligations are discharged.
+    pub all_proven: bool,
+}
+
+impl VerificationSummary {
+    /// Create a summary from a list of proof obligations.
+    pub fn from_obligations(
+        interfaces: usize,
+        functions: usize,
+        obligations: &[ProofObligation],
+    ) -> Self {
+        let total = obligations.len();
+        let discharged = obligations.iter().filter(|o| o.discharged).count();
+        Self {
+            interfaces,
+            functions,
+            total_obligations: total,
+            discharged,
+            remaining: total - discharged,
+            all_proven: discharged == total,
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn verification_summary_all_proven() {
+        let obligations = vec![
+            ProofObligation {
+                function_name: "foo".into(),
+                kind: ProofKind::Totality,
+                type_signature: "foo_total : FooTotal".into(),
+                discharged: true,
+            },
+            ProofObligation {
+                function_name: "foo".into(),
+                kind: ProofKind::RoundTrip,
+                type_signature: "foo_rt : FooRoundTrip".into(),
+                discharged: true,
+            },
+        ];
+        let summary = VerificationSummary::from_obligations(1, 1, &obligations);
+        assert!(summary.all_proven);
+        assert_eq!(summary.remaining, 0);
+    }
 
-// TODO: Define Idris2-specific ABI types and verification functions.
+    #[test]
+    fn verification_summary_partial() {
+        let obligations = vec![
+            ProofObligation {
+                function_name: "bar".into(),
+                kind: ProofKind::Totality,
+                type_signature: "".into(),
+                discharged: true,
+            },
+            ProofObligation {
+                function_name: "bar".into(),
+                kind: ProofKind::Invariant,
+                type_signature: "".into(),
+                discharged: false,
+            },
+        ];
+        let summary = VerificationSummary::from_obligations(1, 1, &obligations);
+        assert!(!summary.all_proven);
+        assert_eq!(summary.remaining, 1);
+    }
+}