Claude/academic proofs verification ax1p y#26
Merged
hyperpolymath merged 3 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
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.