Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 33 additions & 0 deletions .claude/PROJECT.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
== Ochrance - Claude Code Instructions

This repository contains the Ochrance project.

=== Project Structure

....
ochrance/
├── .claude/ # AI assistant instructions
├── .git/ # Version control
├── .gitignore # Git ignore rules
├── .editorconfig # Editor configuration
└── ... # Project files
....

=== Build Commands

Refer to project-specific documentation.

=== Coding Conventions

* Follow hyperpolymath standards
* All code must have SPDX license headers
* Use approved languages only (see CLAUDE.md)
* Document all non-obvious decisions

=== Security

* No hardcoded secrets
* All secrets through environment variables or secret management
* SHA-pinned dependencies where applicable
* HTTPS only, no HTTP URLs
* No MD5/SHA1 for security purposes
37 changes: 0 additions & 37 deletions .claude/PROJECT.md

This file was deleted.

232 changes: 125 additions & 107 deletions ABI-FFI-README.md → ABI-FFI-README.adoc
Original file line number Diff line number Diff line change
@@ -1,25 +1,21 @@
<!--
SPDX-License-Identifier: CC-BY-SA-4.0
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
# Ochrance ABI/FFI Documentation
== Ochrance ABI/FFI Documentation

## Overview
=== Overview

**Ochrance** is a neurosymbolic filesystem verification framework. Its
cryptographic core follows the **Hyperpolymath RSR Standard** for ABI and FFI
design:
*Ochrance* is a neurosymbolic filesystem verification framework. Its
cryptographic core follows the *Hyperpolymath RSR Standard* for ABI and
FFI design:

- **ABI (Application Binary Interface)** defined in **Idris2** with formal
proofs — `src/abi/Ochrance/ABI/`
- **FFI (Foreign Function Interface)** implemented in **Zig** for C
compatibility — `ffi/zig/src/main.zig`
- **Idris2 FFI declarations** in the core library bridge into the Zig
shared object — `ochrance-core/Ochrance/FFI/Crypto.idr`
* *ABI (Application Binary Interface)* defined in *Idris2* with formal
proofs — `+src/abi/Ochrance/ABI/+`
* *FFI (Foreign Function Interface)* implemented in *Zig* for C
compatibility — `+ffi/zig/src/main.zig+`
* *Idris2 FFI declarations* in the core library bridge into the Zig
shared object — `+ochrance-core/Ochrance/FFI/Crypto.idr+`

## Architecture
=== Architecture

```
....
┌─────────────────────────────────────────────────┐
│ ABI Definitions (Idris2) │
│ src/abi/Ochrance/ABI/ │
Expand Down Expand Up @@ -60,90 +56,105 @@ design:
│ - A2ML manifest attestation │
│ - ECHIDNA neural proof synthesis (future) │
└─────────────────────────────────────────────────┘
```
....

## ABI Definitions (Idris2)
=== ABI Definitions (Idris2)

### Types.idr — Core ABI Types
==== Types.idr — Core ABI Types

| Type | Description |
|------|-------------|
| `Platform` | Compile-time target: Linux, Windows, MacOS, BSD, WASM |
| `Result` | Security check outcome: Ok, Error, InvalidParam, OutOfMemory, NullPointer |
| `Handle` | Opaque non-null pointer with type-level `So (ptr /= 0)` proof |
[width="100%",cols="32%,68%",options="header",]
|===
|Type |Description
|`+Platform+` |Compile-time target: Linux, Windows, MacOS, BSD, WASM

```idris
|`+Result+` |Security check outcome: Ok, Error, InvalidParam,
OutOfMemory, NullPointer

|`+Handle+` |Opaque non-null pointer with type-level `+So (ptr /= 0)+`
proof
|===

[source,idris]
----
-- Non-null handle guaranteed at the type level
data Handle : Type where
MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle
```
----

### Layout.idr — Memory Layout Proofs
==== Layout.idr — Memory Layout Proofs

Provides `Layout` records (size + alignment) and two key proof types:
Provides `+Layout+` records (size + alignment) and two key proof types:

- **`PlatformIndependent`** — witnesses that a layout is portable across
architectures
- **`CCompatible`** — proves a type matches C struct packing rules, safe for
FFI
* *`+PlatformIndependent+`* — witnesses that a layout is portable across
architectures
* *`+CCompatible+`* — proves a type matches C struct packing rules, safe
for FFI

Also includes `generateCDecl` for emitting C `typedef` declarations from
proven layouts.
Also includes `+generateCDecl+` for emitting C `+typedef+` declarations
from proven layouts.

### Foreign.idr — FFI Declarations
==== Foreign.idr — FFI Declarations

Declares `prim__blake3` and `prim__sha256` using `%foreign "C:...,libochrance"`
with `Buffer`-based signatures matching the Zig exports.
Declares `+prim__blake3+` and `+prim__sha256+` using
`+%foreign "C:...,libochrance"+` with `+Buffer+`-based signatures
matching the Zig exports.

## Zig FFI Implementation
=== Zig FFI Implementation

All functions in `ffi/zig/src/main.zig` use Zig's `std.crypto` library:
All functions in `+ffi/zig/src/main.zig+` use Zig’s `+std.crypto+`
library:

### Hash Functions
==== Hash Functions

All three hash functions share the same ABI contract:

```c
[source,c]
----
void hash_fn(const uint8_t* data, size_t len, uint8_t out[32]);
```
----

| Function | Algorithm | Output |
|----------|-----------|--------|
| `blake3_hash` | BLAKE3 | 32 bytes |
| `sha256_hash` | SHA-256 | 32 bytes |
| `sha3_256_hash` | SHA3-256 | 32 bytes |
[cols=",,",options="header",]
|===
|Function |Algorithm |Output
|`+blake3_hash+` |BLAKE3 |32 bytes
|`+sha256_hash+` |SHA-256 |32 bytes
|`+sha3_256_hash+` |SHA3-256 |32 bytes
|===

### Signature Verification
==== Signature Verification

```c
[source,c]
----
int ed25519_verify(
const uint8_t signature[64],
const uint8_t public_key[32],
const uint8_t* message,
size_t msg_len
);
// Returns: 1 if valid, 0 if invalid
```

## How They Connect

1. **Zig compiles** `ffi/zig/src/main.zig` into `libochrance.so` (shared
library with C-compatible exports)
2. **Idris2 FFI declarations** in `Ochrance.FFI.Crypto` use
`%foreign "C:blake3_hash,libochrance"` to bind primitives
3. **Buffer management** in `Crypto.idr` allocates `Data.Buffer` objects,
writes input bytes, calls the FFI primitive, reads output bytes
4. **Public API** (`blake3`, `sha256`, `sha3_256`, `ed25519Verify`) wraps
everything in `HasIO io` for safe usage
5. **Merkle tree** (`Ochrance.Filesystem.Merkle`) calls `hashPairBlake3`
which delegates to `blake3` for cryptographic tree hashing
6. **ABI modules** (`src/abi/`) provide the formal foundation: type
definitions with dependent-type proofs, memory layout verification,
and C-header generation

## Directory Structure

```
----

=== How They Connect

[arabic]
. *Zig compiles* `+ffi/zig/src/main.zig+` into `+libochrance.so+`
(shared library with C-compatible exports)
. *Idris2 FFI declarations* in `+Ochrance.FFI.Crypto+` use
`+%foreign "C:blake3_hash,libochrance"+` to bind primitives
. *Buffer management* in `+Crypto.idr+` allocates `+Data.Buffer+`
objects, writes input bytes, calls the FFI primitive, reads output bytes
. *Public API* (`+blake3+`, `+sha256+`, `+sha3_256+`, `+ed25519Verify+`)
wraps everything in `+HasIO io+` for safe usage
. *Merkle tree* (`+Ochrance.Filesystem.Merkle+`) calls
`+hashPairBlake3+` which delegates to `+blake3+` for cryptographic tree
hashing
. *ABI modules* (`+src/abi/+`) provide the formal foundation: type
definitions with dependent-type proofs, memory layout verification, and
C-header generation

=== Directory Structure

....
ochrance/
├── src/abi/Ochrance/ABI/ # Idris2 ABI definitions
│ ├── Types.idr # Platform, Result, Handle
Expand All @@ -168,81 +179,88 @@ ochrance/
├── Filesystem/Merkle.idr # Uses hashPairBlake3 for tree hashing
├── Filesystem/Verify.idr # Uses blake3 for block verification
└── A2ML/ # A2ML manifest parsing/validation
```
....

## Building
=== Building

### Build the Zig FFI Library
==== Build the Zig FFI Library

```bash
[source,bash]
----
cd ffi/zig
zig build # Build debug (libochrance.so)
zig build -Doptimize=ReleaseFast # Build optimized
zig build test # Run Zig unit tests
```
----

### Build the Idris2 Core
==== Build the Idris2 Core

```bash
[source,bash]
----
# Ensure libochrance.so is on LD_LIBRARY_PATH
export LD_LIBRARY_PATH="$PWD/ffi/zig/zig-out/lib:$LD_LIBRARY_PATH"

# Type-check and build (the core package includes the filesystem subsystem)
idris2 --build ochrance.ipkg
```
----

### Cross-Compile
==== Cross-Compile

```bash
[source,bash]
----
cd ffi/zig
zig build -Dtarget=x86_64-linux
zig build -Dtarget=aarch64-linux
zig build -Dtarget=aarch64-macos
```
----

## Testing
=== Testing

### Zig Unit Tests
==== Zig Unit Tests

The Zig source includes inline tests for all four FFI functions:

```bash
[source,bash]
----
cd ffi/zig
zig build test
```
----

Tests cover: empty string hashing (BLAKE3, SHA-256, SHA3-256), known-answer
tests ("abc" for BLAKE3), valid Ed25519 signature verification, and invalid
signature rejection.
Tests cover: empty string hashing (BLAKE3, SHA-256, SHA3-256),
known-answer tests ("`abc`" for BLAKE3), valid Ed25519 signature
verification, and invalid signature rejection.

### Idris2 Integration Tests
==== Idris2 Integration Tests

```bash
[source,bash]
----
idris2 --install ochrance.ipkg
idris2 --build tests/integration/tests.ipkg
./tests/integration/build/exec/integration-tests
```
----

## Contributing
=== Contributing

When modifying the ABI/FFI:

1. **Update ABI types** (`src/abi/Ochrance/ABI/Types.idr`) — add or modify
type definitions with proofs
2. **Update FFI declarations** (`ochrance-core/Ochrance/FFI/Crypto.idr`) —
add `%foreign` declarations and buffer management
3. **Update Zig implementation** (`ffi/zig/src/main.zig`) — implement the
C-compatible function matching the declaration
4. **Add tests** — Zig inline tests for the new function, Idris2 integration
tests for the wrapper
5. **Verify totality** — all Idris2 modules must pass `%default total`
[arabic]
. *Update ABI types* (`+src/abi/Ochrance/ABI/Types.idr+`) — add or
modify type definitions with proofs
. *Update FFI declarations* (`+ochrance-core/Ochrance/FFI/Crypto.idr+`)
— add `+%foreign+` declarations and buffer management
. *Update Zig implementation* (`+ffi/zig/src/main.zig+`) — implement the
C-compatible function matching the declaration
. *Add tests* — Zig inline tests for the new function, Idris2
integration tests for the wrapper
. *Verify totality* — all Idris2 modules must pass `+%default total+`

## License
=== License

MPL-2.0

## See Also
=== See Also

- [Idris2 Documentation](https://idris2.readthedocs.io)
- [Zig Documentation](https://ziglang.org/documentation/master/)
- [Rhodium Standard Repositories](https://github.com/hyperpolymath/rhodium-standard-repositories)
* https://idris2.readthedocs.io[Idris2 Documentation]
* https://ziglang.org/documentation/master/[Zig Documentation]
* https://github.com/hyperpolymath/rhodium-standard-repositories[Rhodium
Standard Repositories]
Loading
Loading