Claude/academic proofs verification ax1p y#28
Merged
hyperpolymath merged 5 commits intomainfrom Dec 31, 2025
Merged
Conversation
This commit adds extensive academic documentation covering all theoretical foundations required for rigorous academic scrutiny of the Oblibeny oblivious computing ecosystem. Documentation includes: Foundations: - Set-theoretic foundations and memory models - Type-theoretic security (information flow, linear types, effects) - Categorical semantics (monads, functors, natural transformations) - Probability theory (concentration bounds, negligible functions) - Algebra and number theory (groups, fields, lattices, elliptic curves) - Logic and proof theory (modal, temporal, separation logic) Cryptography: - ORAM security proofs (Path ORAM, Circuit ORAM, recursive ORAM) - Encryption primitives (AES-GCM, PRFs, Merkle trees, commitments) Formal Methods: - Formal verification (Hoare logic, refinement, model checking) - Program analysis (abstract interpretation, taint tracking) - Concurrency theory (linearizability, consensus, Byzantine FT) Complexity and Information Theory: - Time/space/communication complexity with lower bounds - Information-theoretic leakage analysis - Statistical security methodology Engineering: - RISC-V ISA extensions for oblivious computing - Protocol specifications (client-server, filesystem) Also includes: - Technical white paper with complete system overview - Index with reading guides for different audiences - Consolidated TODO list with prioritized future work Total: 19 AsciiDoc files covering all academic requirements
This commit defines the split-compiler architecture for Oblibeny: Architecture: - OCaml frontend for parsing, type checking, security analysis - Rust backend for code generation and ORAM runtime - OIR (Oblivious IR) as the boundary format between them OCaml Frontend (docs/specs/frontend/): - Lexer specification (ocamllex) - Parser grammar (Menhir) - AST and typed AST definitions - Security type system with @low/@high annotations - Obliviousness checker for leak detection - IR lowering to OIR OIR Specification (docs/specs/ir/): - Complete schema for types, functions, instructions - Security level annotations - Explicit ORAM operations (oram_read, oram_write, cmov) - JSON and MessagePack serialization formats - Both OCaml and Rust type definitions Rust Backend (docs/specs/backend/): - IR parser and validator - Optimizer (batching, inlining, DCE) - Code generators (Rust, RISC-V, WASM, C) - Path ORAM implementation - Constant-time primitives (cmov, cswap) - Oblivious collections (OArray, OMap) - Crypto layer (AES-GCM, SHA-256, BLAKE3, Merkle) This architecture leverages: - OCaml's strengths in symbolic manipulation - Rust's strengths in systems programming - Clean IR boundary for separation of concerns
Add complete compiler infrastructure following the OIR architecture: Frontend (OCaml): - Lexer (ocamllex) and parser (Menhir) for .obl source files - AST with security labels (@low/@high) and oblivious types - Type checker with security-aware type inference - Obliviousness checker (no secret branches/indices/loops) - OIR (Oblivious IR) JSON emitter Backend (Rust): - OIR deserializer matching OCaml definitions - Code generator producing Rust with ORAM calls - Support for inline runtime or external crate Runtime (Rust): - Constant-time primitives (cmov, cswap, ct_lookup) - Path ORAM implementation with position map and stash - Oblivious collections (OArray, OStack, OQueue, OMap) - Cryptographic utilities (AES-GCM, SHA-256, BLAKE3) Driver: - Unified CLI orchestrating frontend → backend pipeline - compile, check, and build subcommands Also: - Workspace Cargo.toml for Rust components - justfile for unified build system - Example .obl source file demonstrating oblivious patterns - Convert transpiler-framework from submodule to tracked directory
Addresses Semgrep finding ocaml.lang.portability.crlf-support. Using open_out_bin ensures consistent line endings (no LF-to-CRLF translation on Windows) when writing OIR JSON files.
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.