Claude/add academic proofs mg s2z#32
Merged
Merged
Conversation
This commit adds extensive formal proofs, theorems, and academic documentation for WokeLang covering: Formal Semantics: - Big-step and small-step operational semantics - Denotational semantics with domain theory - Grammar proofs (unambiguity, LL(k) property, parser correctness) Type Theory: - Type safety proofs (Progress and Preservation theorems) - Hindley-Milner type inference algorithm and properties - Category theory foundations (CCCs, functors, monads) Security: - Capability-based security model proofs - Consent model formal specification - Information flow and access control properties Compiler: - Semantic preservation across compilation stages - Memory model and safety proofs (no UAF, no data races) - Interpreter ↔ VM ↔ WASM equivalence Analysis: - Complexity analysis for all major operations - Concurrency and worker system proofs - Deadlock freedom and isolation properties Verification: - Coq specification with theorem stubs (WokeLang.v) - Lean 4 specification with proofs (WokeLang.lean) - TODO markers for incomplete mechanized proofs Papers: - Language design white paper with rationale These documents provide the theoretical foundation for academic scrutiny and future formal verification efforts.
Core Language Features: - Add Okay(value) and Oops(message) variants to runtime Value enum - Add Expr::Index for array/string subscript access - Add Expr::Okay, Expr::Oops, and Expr::Unwrap expression nodes - Add Pattern::Constructor for matching Result types Parser Updates: - Parse Okay(expr) and Oops(expr) as Result constructors - Parse expr[index] for array and string indexing - Parse Okay(x) and Oops(e) as constructor patterns in decide blocks Interpreter Updates: - Implement evaluation of Index, Okay, Oops, Unwrap expressions - Add apply_index() for array and string element access - Update pattern matching to bind variables in constructor patterns - Add builtin functions: isOkay, isOops, unwrapOr, getError - Add is_okay(), is_oops(), unwrap() methods to Value Tests: - Add 7 new integration tests for Result types and indexing - test_result_okay, test_result_oops, test_unwrap_or - test_array_indexing, test_string_indexing - test_decide_with_result, test_chained_indexing All 21 tests pass.
AST Changes:
- Add Expr::Lambda for lambda expressions |x, y| -> expr
- Add Expr::CallExpr for calling expression values
- Add LambdaExpr and LambdaBody types
- Add Type::Function for function type annotations
Runtime Changes:
- Add Value::Function(Closure) for first-class functions
- Add Closure struct with params, body, and captured environment
- Add CapturedEnv to store captured variable bindings
Interpreter:
- Implement Lambda evaluation with environment capture
- Implement CallExpr for calling closures
- Add capture_environment() to snapshot bindings
- Add call_closure() to execute closures
- Update call_function() to check for closure variables first
Parser:
- Parse |x, y| -> expr (expression lambdas)
- Parse |x, y| { ... } (block lambdas)
- Parse || -> expr (no-param lambdas)
- Parse expr(args) for calling expression values
Tests:
- test_lambda_expression: basic lambda with arrow syntax
- test_lambda_block: block body with give back
- test_closure_captures: variable capture verification
- test_higher_order_function: passing functions as arguments
- test_lambda_no_params: zero-parameter lambdas
All 26 tests pass.
- Rewrote type checker to match current AST (Lambda, CallExpr, Result types) - Added Hindley-Milner style type inference with unification - Registered builtin functions (print, len, toString, toInt, isOkay, isOops, unwrapOr, getError) - Updated main.rs to run type checker before interpreter - Added --typecheck flag for type-checking without execution - Type errors now block program execution with clear error messages
- Added TypeParam struct for generic type parameters with optional bounds - Added type_params field to FunctionDef for generic functions: `to identity<T>(x: T) -> T` - Added Type::Generic for parameterized types: `Result<Int, String>` - Added Type::TypeVar for type parameter references inside generic functions - Updated parser to parse <T, U: Bound> type parameters and type arguments - Updated type checker to handle generic type conversion and unification - Type variables unify with any type (polymorphic behavior)
- Added Literal::Unit variant to AST for the () value
- Parser now recognizes () as a Unit literal expression
- Interpreter and type checker handle Literal::Unit correctly
- Functions can return Unit type explicitly: `to foo() → Unit { give back (); }`
Features: - Multiline input: automatic detection of incomplete expressions (unbalanced braces/parens) - Persistent history: saved to ~/.woke_history between sessions - Tab completion: keywords and user-defined identifiers - Linting: type checking before execution (toggleable with :lint) - New commands: :type, :lint, :history - Start with `woke repl` Commands: :help, :quit, :clear, :reset, :load, :ast, :type, :env, :lint, :history
Security improvements: - Path traversal prevention: Reject paths with '..' components and null bytes - File size limits: 10MB max for read operations to prevent memory exhaustion - JSON parsing limits: 1MB max input size and 100-level nesting depth limit - Network SSRF prevention: Block localhost, private IPs, link-local, and cloud metadata endpoints (169.254.169.254) - Recursion limit: 1000 max depth to prevent stack overflow - Negative index protection: Proper error instead of wraparound bug - UTF-8 string length: Use char count instead of byte count for len() - I/O error handling: Replace panics with proper error propagation New Value::Record variant added for JSON object support. Exposed stdlib and security modules in lib.rs. All 73 tests pass.
Implements typed, thread-safe channels for WokeLang: - ChannelHandle type with send/recv/try_recv/recv_timeout operations - Buffered and unbuffered channel support - Channel closing and closed-state checking - Maximum buffer size limit (10,000) for safety New stdlib functions: - std.chan.make(capacity?) - Create unbuffered or buffered channel - std.chan.send(channel, value) - Send value on channel - std.chan.recv(channel) - Blocking receive - std.chan.tryRecv(channel) - Non-blocking receive - std.chan.recvTimeout(channel, ms) - Receive with timeout - std.chan.close(channel) - Close the channel - std.chan.isClosed(channel) - Check if closed Value enum now includes Channel variant for first-class channel support. All 79 tests pass.
String module (std.string.*): - length, upper, lower, trim, trimStart, trimEnd - contains, startsWith, endsWith - replace, split, join, substring, indexOf - repeat, reverse, padStart, padEnd - chars (to character array), isEmpty Array module (std.array.*): - length, isEmpty, first, last - push, pop, concat, reverse - slice (with negative indices), contains, indexOf - repeat, range (with step support) - flatten, unique, zip All functions include proper UTF-8 handling, bounds checking, and size limits to prevent memory exhaustion. Total: 94 tests passing.
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.