Claude/academic proofs verification ax1p y

obli-transpiler-framework/.gitignore

@@ -0,0 +1,34 @@
+# Rust
+/target/
+Cargo.lock
+
+# OCaml
+_build/
+*.install
+*.merlin
+.merlin
+
+# IDE
+.idea/
+.vscode/
+*.swp
+*.swo
+*~
+
+# Build artifacts
+*.o
+*.a
+*.so
+*.dylib
+
+# Generated files
+*.oir.json
+*.generated.rs
+
+# Test artifacts
+*.log
+coverage/
+
+# OS
+.DS_Store
+Thumbs.db

obli-transpiler-framework/Cargo.toml

@@ -0,0 +1,28 @@
+# SPDX-License-Identifier: MIT OR Palimpsest-0.8
+# Copyright (c) 2024 Hyperpolymath
+
+[workspace]
+resolver = "2"
+members = [
+    "backend",
+    "runtime",
+    "driver",
+]
+
+[workspace.package]
+version = "0.1.0"
+edition = "2021"
+authors = ["Hyperpolymath"]
+license = "MIT OR Palimpsest-0.8"
+repository = "https://github.com/hyperpolymath/oblibeny"
+
+[workspace.dependencies]
+serde = { version = "1.0", features = ["derive"] }
+serde_json = "1.0"
+thiserror = "1.0"
+clap = { version = "4.0", features = ["derive"] }
+log = "0.4"
+env_logger = "0.10"
+subtle = "2.5"
+zeroize = { version = "1.7", features = ["derive"] }
+rand = "0.8"

obli-transpiler-framework/README.md

@@ -0,0 +1,115 @@
+# Oblibeny Transpiler Framework
+
+The compiler and runtime for the Oblibeny oblivious computing language.
+
+## Architecture
+
+```
+┌──────────────────────────────────────────────────────────────────────────┐
+│                              Oblibeny Compiler                            │
+├──────────────────────────────────────────────────────────────────────────┤
+│                                                                          │
+│  ┌─────────────┐      ┌─────────────┐      ┌─────────────────────────┐  │
+│  │   Source    │      │     OIR     │      │    Generated Rust       │  │
+│  │   (.obl)    │─────▶│   (JSON)    │─────▶│    + Runtime            │  │
+│  └─────────────┘      └─────────────┘      └─────────────────────────┘  │
+│         │                    │                        │                  │
+│         ▼                    ▼                        ▼                  │
+│  ┌─────────────┐      ┌─────────────┐      ┌─────────────────────────┐  │
+│  │   OCaml     │      │    Rust     │      │   oblibeny-runtime      │  │
+│  │  Frontend   │      │   Backend   │      │   (ORAM + Crypto)       │  │
+│  └─────────────┘      └─────────────┘      └─────────────────────────┘  │
+│                                                                          │
+└──────────────────────────────────────────────────────────────────────────┘
+```
+
+## Components
+
+### Frontend (OCaml)
+
+The frontend parses `.obl` source files and performs:
+- Lexing and parsing
+- Type checking with security labels (@low/@high)
+- Obliviousness verification (no secret-dependent branches/indices)
+- OIR (Oblivious Intermediate Representation) emission
+
+### Backend (Rust)
+
+The backend consumes OIR and generates:
+- Rust code using the oblibeny-runtime
+- Calls to constant-time primitives (cmov, cswap)
+- ORAM operations (oread, owrite)
+
+### Runtime (Rust)
+
+The runtime library provides:
+- **Constant-time primitives**: cmov, cswap, ct_lookup
+- **Path ORAM**: O(log N) oblivious memory access
+- **Oblivious collections**: OArray, OStack, OQueue, OMap
+- **Cryptographic utilities**: AES-GCM, SHA-256, BLAKE3
+
+### Driver
+
+The unified `oblibeny` CLI that orchestrates the pipeline.
+
+## Building
+
+Requires:
+- OCaml 4.14+ with opam
+- Rust 1.70+
+- just (command runner)
+
+```bash
+# Install OCaml dependencies
+opam install dune menhir sedlex yojson ppx_deriving ppx_deriving_yojson
+
+# Build everything
+just build
+
+# Run tests
+just test
+
+# Install to ~/.local/bin
+just install
+```
+
+## Usage
+
+```bash
+# Compile to Rust
+oblibeny compile program.obl
+
+# Type-check only
+oblibeny check program.obl
+
+# Compile and build executable
+oblibeny build program.obl
+```
+
+## Example
+
+```
+// hello.obl - Oblivious array access
+
+@oblivious
+fn secret_lookup(arr: oarray<int>, @high idx: int) -> @high int {
+    return oread(arr, idx);
+}
+
+fn main() {
+    let data: oarray<int> = oarray_new(100);
+
+    // Initialize with public indices
+    for i in 0..100 {
+        owrite(data, i, i * 10);
+    }
+
+    // Look up with secret index - access pattern hidden!
+    let secret_idx: @high int = get_secret();
+    let value: @high int = secret_lookup(data, secret_idx);
+}
+```
+
+## License
+
+MIT OR Palimpsest-0.8

obli-transpiler-framework/backend/Cargo.toml

@@ -0,0 +1,22 @@
+# SPDX-License-Identifier: MIT OR Palimpsest-0.8
+# Copyright (c) 2024 Hyperpolymath
+
+[package]
+name = "oblibeny-backend"
+version = "0.1.0"
+edition = "2021"
+authors = ["Hyperpolymath"]
+description = "Oblibeny language backend - OIR to Rust code generator"
+license = "MIT OR Palimpsest-0.8"
+repository = "https://github.com/hyperpolymath/oblibeny"
+
+[dependencies]
+serde = { version = "1.0", features = ["derive"] }
+serde_json = "1.0"
+thiserror = "1.0"
+clap = { version = "4.0", features = ["derive"] }
+log = "0.4"
+env_logger = "0.10"
+
+[dev-dependencies]
+pretty_assertions = "1.0"