diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3cebaec..8f4671d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -11,23 +11,38 @@ jobs: fail-fast: false matrix: compiler: - - { cc: gcc, cxx: g++, flags: "" } - # libstdc++ 13 hides std::expected from Clang 18, so Clang builds against libc++ - - { cc: clang, cxx: clang++, flags: "-stdlib=libc++" } + - { cc: gcc, cxx: g++ } + # Clang 19 is the first Clang whose concepts level unlocks std::expected in libstdc++ 13 + - { cc: clang, cxx: clang++-19 } name: linux-${{ matrix.compiler.cc }} runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 - - name: Install libc++ + - name: Install Clang 19 if: matrix.compiler.cc == 'clang' - run: sudo apt-get update && sudo apt-get install -y libc++-18-dev libc++abi-18-dev + run: sudo apt-get update && sudo apt-get install -y clang-19 - name: Configure - run: cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=${{ matrix.compiler.cxx }} "-DCMAKE_CXX_FLAGS=${{ matrix.compiler.flags }}" + run: cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=${{ matrix.compiler.cxx }} - name: Build run: cmake --build build - name: Test run: ctest --test-dir build --output-on-failure + fuzz: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + - name: Install Clang 19 + run: sudo apt-get update && sudo apt-get install -y clang-19 libclang-rt-19-dev + - name: Build fuzzers + run: | + cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=RelWithDebInfo -DCMAKE_CXX_COMPILER=clang++-19 -DTHEOS_FUZZ=ON -DTHEOS_BUILD_TESTS=OFF + cmake --build build + - name: Fuzz the binary decoder (60 s) + run: ./build/fuzz/decode_fuzzer -max_total_time=60 -max_len=8192 fuzz/corpus/decode + - name: Fuzz the parser (60 s) + run: ./build/fuzz/parse_fuzzer -max_total_time=60 -max_len=8192 fuzz/corpus/parse + windows-mingw: runs-on: windows-latest defaults: diff --git a/.gitignore b/.gitignore index bcc19ab..beca4ac 100644 --- a/.gitignore +++ b/.gitignore @@ -48,3 +48,11 @@ Thumbs.db Desktop.ini $RECYCLE.BIN/ /build*/ +!/tests/golden/**/*.theos +!/fuzz/corpus/**/*.theos + +# libFuzzer artifacts +crash-* +leak-* +timeout-* +oom-* diff --git a/CLAUDE.md b/CLAUDE.md index ed55ac9..a459b23 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -7,8 +7,9 @@ - **Run Binary:** `./build/theosc` ## Coding Standards & C++20 Style Guide -- **Language Standard:** Strict C++23 (`std::expected`, `std::span`, `std::unique_ptr`, `constexpr`, concepts). GCC 13+ / Clang 18+ / MinGW-w64 GCC 13+. +- **Language Standard:** Strict C++23 (`std::expected`, `std::span`, `std::unique_ptr`, `constexpr`, concepts). GCC 13+ / Clang 19+ / MinGW-w64 GCC 13+ (Clang 18 cannot see `std::expected` in libstdc++ 13). - **Memory Safety:** Avoid raw `new`/`delete`. Use smart pointers and deterministic resource acquisition (RAII). -- **Binary Packing:** All disk structs must use `#pragma pack(push, 1)` to prevent compiler padding misalignment when reading/writing raw binary streams. +- **Binary Format:** `.theos` is read and written field by field with explicit little-endian encoding and bounds checks (`src/core/binary.cpp`); never `reinterpret_cast` file bytes into structs. Spec: `docs/spec/theos-v2.md`. +- **Golden Files:** `THEOS_UPDATE_GOLDEN=1 ./build/tests/theos_tests "[golden]"` regenerates `tests/golden/**` outputs; review the diff before committing. - **Error Handling:** Use `std::expected` or exceptions with explicit error categories for file I/O and syntax parsing failures. Never leave parsing streams unchecked. - **Const Correctness:** Make member functions `const` wherever state is unmodified. \ No newline at end of file diff --git a/CMakeLists.txt b/CMakeLists.txt index eeba1db..2e4d48b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -16,8 +16,16 @@ if(MINGW) add_link_options(-static -static-libstdc++ -static-libgcc) endif() +# Fuzz builds instrument everything so the fuzzers see coverage inside the library +option(THEOS_FUZZ "Build libFuzzer targets (Clang only)" OFF) +if(THEOS_FUZZ) + add_compile_options(-fsanitize=fuzzer-no-link,address,undefined -fno-sanitize-recover=all) + add_link_options(-fsanitize=address,undefined) +endif() + add_library(theos_core STATIC src/core/ast.cpp + src/core/binary.cpp src/core/canon.cpp src/core/diagnostic.cpp src/core/driver.cpp @@ -33,6 +41,10 @@ target_link_libraries(theos_core PRIVATE theos_warnings) add_executable(theosc src/cli/main.cpp) target_link_libraries(theosc PRIVATE theos_core theos_warnings) +if(THEOS_FUZZ) + add_subdirectory(fuzz) +endif() + option(THEOS_BUILD_TESTS "Build the test suite" ON) if(THEOS_BUILD_TESTS) enable_testing() diff --git a/README.md b/README.md index 31e252f..4d5a281 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,8 @@ Theos bridges this gap. It provides a deterministic pipeline to turn human-reada ## Pipeline ``` -.theo source ─► Lexer ─► Parser ─► AST ─► Validator ─► Mermaid exporter +.theo source ─► Lexer ─► Parser ─► AST ─► Validator ─┬─► Mermaid exporter + └─► .theos binary (encode / decode) ``` Each claim in a `.theo` file carries natural-language text and a formula: @@ -45,11 +46,27 @@ The full language is specified in [docs/spec/language.md](docs/spec/language.md) --- +## The `.theos` Binary Format + +`theosc build` compiles a checked argument into a `.theos` file, specified in +[docs/spec/theos-v2.md](docs/spec/theos-v2.md): + +- PNG-style signature (`89 54 48 45 4F 0D 0A 1A`) that detects text-mode corruption +- Tagged, CRC-32-protected chunks; unknown ancillary chunks are skipped, unknown critical chunks rejected +- Fixed-width little-endian records referencing each other by index, for O(1) access +- One deduplicated string table and one expression table with shared sub-formulas +- A reader that bounds-checks every offset and index, fuzzed with libFuzzer in CI + +--- + ## CLI Usage ```sh -theosc check examples/aquinas_first_way.theo -theosc export examples/resurrection.theo --format mermaid -o resurrection.mmd +theosc check examples/aquinas_first_way.theo +theosc export examples/resurrection.theo --format mermaid -o resurrection.mmd +theosc build examples/resurrection.theo -o resurrection.theos +theosc inspect resurrection.theos # decoded argument +theosc inspect resurrection.theos --chunks # chunk table and hex view ``` Diagnostics go to stderr as `file:line:col: error: message` with the source line underneath; @@ -62,10 +79,11 @@ exit code 0 = success, 1 = invalid input, 2 = usage error. ```text theos-engine/ ├── include/theos/ # Public headers -├── src/core/ # Core library (lexer, parser, validator, exporter) +├── src/core/ # Core library (lexer, parser, validator, exporter, binary format) ├── src/cli/ # theosc command-line tool -├── docs/spec/ # Language specification +├── docs/spec/ # Language and binary format specifications ├── examples/ # Sample .theo arguments +├── fuzz/ # libFuzzer targets and seed corpora └── tests/ # Catch2 unit tests and golden files ``` @@ -73,7 +91,7 @@ theos-engine/ ## Building from Source -Requires CMake 3.20+ and a C++23 compiler (GCC 13+, Clang 18+, or MinGW-w64 GCC 13+ via MSYS2). +Requires CMake 3.20+ and a C++23 compiler (GCC 13+, Clang 19+, or MinGW-w64 GCC 13+ via MSYS2). Tests use Catch2, fetched automatically by CMake. ```sh @@ -83,6 +101,9 @@ ctest --test-dir build --output-on-failure ./build/theosc ``` +Fuzzing (Clang 19+): `cmake -B build-fuzz -DCMAKE_CXX_COMPILER=clang++-19 -DTHEOS_FUZZ=ON -DTHEOS_BUILD_TESTS=OFF`, +then `./build-fuzz/fuzz/decode_fuzzer fuzz/corpus/decode`. + On Windows, run the same commands from an MSYS2 UCRT64 shell (add `-G "MinGW Makefiles"` or `-G Ninja` if needed). See [ROADMAP.md](ROADMAP.md) for where the project is going. Licensed under the [MIT License](LICENSE). diff --git a/ROADMAP.md b/ROADMAP.md index 0d0e62e..ce6daa2 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -259,4 +259,5 @@ Answers to the original open questions (2026-10-24) and decisions made while bui | Phase | Status | |-------|--------| | 0 Foundation | done | -| 1 Language v2 | done — formulas are fully parsed already (needed to find where they end); the v1 binary format was removed here rather than in M2.2 because it was tied to the old AST; syntax errors stop at the first error, static-rule errors are all reported; Clang builds use libc++ because libstdc++ 13 hides `std::expected` from Clang 18 | +| 1 Language v2 | done — formulas are fully parsed already (needed to find where they end); the v1 binary format was removed here rather than in M2.2 because it was tied to the old AST; syntax errors stop at the first error, static-rule errors are all reported; Clang CI uses Clang 19, the first Clang that can use `std::expected` from libstdc++ 13 | +| 2 Binary v2 | done — formulas, proofs and objections are serialized here (M3.4 folded in, since the AST already carries them); padding must be zero so every single-byte corruption is detected (verified by flipping every byte); nesting depth is capped in parser (256) and decoder (512) | diff --git a/context.md b/context.md deleted file mode 100644 index 0322d38..0000000 --- a/context.md +++ /dev/null @@ -1,44 +0,0 @@ -> **Superseded.** This describes a planned layout that was never implemented and disagrees with the code. It is replaced by the `.theos` v2 specification in Phase 2 of [ROADMAP.md](ROADMAP.md). - -# .theos File Format Specification v1.0 - -## 1. Overview -The `.theos` file format is a binary container designed to store logical theological arguments, premises, deductions, conclusions, and scriptural proof anchors. - -## 2. Low-Level Binary Layout -Every `.theos` file consists of four contiguous segments: - -### A. Header Block (Bytes 0–31) -- **Magic Number (4 bytes):** `0x54, 0x48, 0x45, 0x4F` ("THEO") -- **Version (2 bytes):** Major/Minor version (`0x0100` for v1.0) -- **Node Count (2 bytes):** Total number of logic nodes in the graph. -- **Axiom Count (2 bytes):** Total scriptural axiom references. -- **Offsets (20 bytes):** - - `axiom_table_offset` (4 bytes, `uint32_t`) - - `node_table_offset` (4 bytes, `uint32_t`) - - `string_heap_offset` (4 bytes, `uint32_t`) - - `reserved` (8 bytes) - -### B. Scripture Axiom Table -A packed array of 32-bit unsigned integers representing scriptural references without string overhead. -- **Bit-Packing Layout (`uint32_t`):** - - Bits 0–7 (8 bits): Book ID (1–66) - - Bits 8–16 (9 bits): Chapter ID (1–512) - - Bits 17–24 (8 bits): Start Verse (1–256) - - Bits 25–31 (7 bits): End Verse offset (0–127) - -### C. Graph Node Table -Fixed-width node records allowing $O(1)$ random access index lookup: -- `node_id` (`uint16_t`) -- `type` (`uint8_t`: 0x01 = Premise, 0x02 = Deduction, 0x03 = Conclusion) -- `dep_count` (`uint8_t`: number of incoming edges) -- `string_offset` (`uint32_t`: byte pointer into String Heap) -- `dep_node_ids` (`uint16_t[4]`: fixed array of parent dependency node IDs) -- `axiom_ids` (`uint16_t[2]`: attached scriptural axiom indices) - -### D. String Heap -Contiguous null-terminated UTF-8 character arrays referenced by string offsets. - -## 3. Validation Rules (DAG Graph Theory) -1. **Acyclic Constraint:** The logic graph must be a Directed Acyclic Graph. Cycles trigger a compilation abort. -2. **Orphan Check:** Every node of type `Conclusion` must resolve its dependency path back to at least one valid scriptural `Axiom`. \ No newline at end of file diff --git a/docs/spec/theos-v2.md b/docs/spec/theos-v2.md new file mode 100644 index 0000000..022e88e --- /dev/null +++ b/docs/spec/theos-v2.md @@ -0,0 +1,298 @@ +# The `.theos` Binary Format — Specification v2.0 + +A `.theos` file is a compiled, validated argument: every axiom, definition, +node, formula, proof and objection of a `.theo` source, stored so a reader can +verify it cheaply and index any record in O(1). + +Design goals, and the mechanism that serves each: + +| Goal | Mechanism | +|------|-----------| +| Detect transfer corruption | PNG-style signature with `\r\n` and `0x1A`, CRC-32 on the header and on every chunk | +| Evolve without breaking readers | Tagged chunks; unknown *ancillary* chunks are skipped, unknown *critical* chunks are rejected | +| O(1) access, memory-mappable | Fixed-width little-endian records, 4-byte aligned payloads, references by index | +| No duplicated data | One string table, one expression table with structurally shared sub-formulas | +| Safe on hostile input | Every offset and index is bounds-checked; expressions may only reference earlier expressions, so decoding cannot loop or recurse unboundedly | + +All integers are **little-endian**. `u8/u16/u32` are unsigned integers of 1, 2 +and 4 bytes. `NONE = 0xFFFFFFFF` marks an absent reference. + +--- + +## 1. File layout + +``` +offset 0 signature 8 bytes +offset 8 header 16 bytes +offset 24 chunk 0 + chunk 1 + ... +``` + +### 1.1 Signature + +``` +89 54 48 45 4F 0D 0A 1A +``` + +`0x89` catches 7-bit transfers, `T H E O` identifies the format, `0D 0A` +catches line-ending conversion in either direction, `1A` stops `type` on +Windows from printing the binary body. + +### 1.2 Header (16 bytes) + +| Offset | Type | Field | +|--------|------|-------| +| 8 | u16 | `version_major` = 2 | +| 10 | u16 | `version_minor` = 0 | +| 12 | u32 | `chunk_count` | +| 16 | u32 | `file_size` — total bytes, signature included | +| 20 | u32 | `header_crc` — CRC-32 of bytes 0–19 | + +A reader rejects a file whose major version it does not know. Minor versions +only add ancillary chunks or use reserved fields that were zero. + +### 1.3 Chunks + +``` ++0 tag 4 bytes ASCII ++4 length u32 payload length in bytes, padding excluded ++8 crc u32 CRC-32 of tag + payload ++12 payload length bytes + padding 0–3 zero bytes so the next chunk starts 4-byte aligned +``` + +The case of the first tag letter decides what an unknown chunk means, as in +PNG: **uppercase = critical** (a reader that does not know it must reject the +file), **lowercase = ancillary** (safe to skip). Each tag appears at most once. +Chunks may appear in any order; readers locate them by tag. + +CRC-32 is the IEEE 802.3 polynomial (`0xEDB88320` reflected), initial value +`0xFFFFFFFF`, final XOR `0xFFFFFFFF` — the same CRC as PNG and zlib. + +--- + +## 2. Chunks + +Required: `META`, `STRS`, `FORM`, `NODE`. The others may be omitted when empty. + +### 2.1 `STRS` — string table + +Concatenated UTF-8 strings, each terminated by `00`. A string reference is the +byte offset of the string's first byte. The payload starts with `00`, so +reference `0` is the empty string. Identical strings are stored once. + +### 2.2 `META` — document metadata + +| Type | Field | +|------|-------| +| u32 | `flags` — bit 0: argument file (has a title) | +| u32 | `title` (string) | +| u32 | `author` (string) | +| u32 | `source_file` (string) | +| u32 | `import_count` | +| u32 × import_count | import paths (strings) | + +### 2.3 `FORM` — expression table + +| Type | Field | +|------|-------| +| u32 | `expr_count` | +| u32 | `pool_count` | +| 16 bytes × expr_count | expression records | +| u32 × pool_count | argument pool (expression indices) | + +Expression record (16 bytes): + +| Offset | Type | Field | +|--------|------|-------| +| 0 | u8 | `kind` (table below) | +| 1 | u8 | `sort` — 0 individual, 1 property (binders only) | +| 2 | u16 | `argc` — Atom argument count | +| 4 | u32 | `name` (string) — Symbol name, Atom head, binder variable | +| 8 | u32 | `a` | +| 12 | u32 | `b` | + +| kind | Expression | `a` | `b` | +|------|------------|-----|-----| +| 0 | Symbol | — | — | +| 1 | Lambda | body | — | +| 2 | Atom | first pool index of the `argc` arguments | — | +| 3 | Eq | left symbol | right symbol | +| 4 | Bottom | — | — | +| 5 / 6 / 7 | Not / Box / Dia | operand | — | +| 8 / 9 / 10 / 11 | And / Or / Implies / Iff | left | right | +| 12 / 13 | Forall / Exists | body | — | + +Unused fields are 0. **Every child index must be smaller than the index of the +record that uses it**, so the table is a topologically sorted DAG: a reader +builds expressions in one forward pass. Writers share identical sub-formulas. + +### 2.4 `AXIM` — axioms + +| Type | Field | +|------|-------| +| u32 | `count` | +| 24 bytes × count | axiom records | + +| Offset | Type | Field | +|--------|------|-------| +| 0 | u8 | `kind` — 0 scripture, 1 source, 2 principle | +| 1 | u8 | `canon` — 0 protestant, 1 catholic, 2 orthodox, 3 quran (scripture only) | +| 2 | u16 | `book` (1-based within the canon; 0 for the Quran) | +| 4 | u16 | `chapter` | +| 6 | u16 | `verse` (0 = whole chapter) | +| 8 | u16 | `end_chapter` | +| 10 | u16 | `end_verse` | +| 12 | u32 | `id` (string) | +| 16 | u32 | `citation` (string) — reference text, work, or statement | +| 20 | u32 | `locator` (string) — source locator | + +### 2.5 `DEFN` — definitions + +| Type | Field | +|------|-------| +| u32 | `count` | +| u32 | `param_count` | +| 16 bytes × count | definition records: `id` (string), `body` (expr), `param_start`, `param_count` | +| 8 bytes × param_count | parameters: `name` (string), `sort` (u8), 3 zero bytes | + +### 2.6 `NODE` — nodes + +| Type | Field | +|------|-------| +| u32 | `count` | +| 32 bytes × count | node records | + +| Offset | Type | Field | +|--------|------|-------| +| 0 | u8 | `kind` — 0 premise, 1 deduction, 2 conclusion | +| 1 | u8 | `flags` — bit 0 imported, bit 1 has `by` rule, bit 2 has proof | +| 2 | u16 | reserved (0) | +| 4 | u32 | `id` (string) | +| 8 | u32 | `text` (string) | +| 12 | u32 | `formula` (expr) | +| 16 | u32 | `rule` (string, if flag bit 1) | +| 20 | u32 | `proof` (`PROF` item index of the proof root, if flag bit 2) | +| 24 | u32 | `edge_start` — first `EDGE` entry | +| 28 | u16 | `from_count` — node indices at `edge_start` | +| 30 | u16 | `grounds_count` — axiom indices following them | + +### 2.7 `EDGE` — edge pool + +| Type | Field | +|------|-------| +| u32 | `count` | +| u32 × count | node or axiom indices, as sliced by `NODE` records | + +### 2.8 `DIAL` — objections and replies + +| Type | Field | +|------|-------| +| u32 | `count` | +| 20 bytes × count | records | + +| Offset | Type | Field | +|--------|------|-------| +| 0 | u8 | `kind` — 0 objection, 1 reply | +| 1 | u8 | `target_kind` — 0 node, 1 objection/reply | +| 2 | u16 | reserved (0) | +| 4 | u32 | `id` (string) | +| 8 | u32 | `text` (string) | +| 12 | u32 | `formula` (expr or NONE) | +| 16 | u32 | `target` — index into `NODE` or `DIAL` | + +### 2.9 `PROF` — proofs + +| Type | Field | +|------|-------| +| u32 | `item_count` | +| u32 | `ref_count` | +| 24 bytes × item_count | proof items, pre-order | +| 12 bytes × ref_count | line references | + +Proof item: + +| Offset | Type | Field | +|--------|------|-------| +| 0 | u8 | `type` — 0 line, 1 subproof, 2 proof root | +| 1 | u8 | `flags` — bit 0 strict (`box`), bit 1 has fresh name | +| 2 | u16 | `ref_count` (lines) | +| 4 | u32 | line: `number`; subproof/root: number of direct children | +| 8 | u32 | line: `formula` (expr); subproof: `fresh` (string) | +| 12 | u32 | line: `rule` (string) | +| 16 | u32 | line: `ref_start` | +| 20 | u32 | reserved (0) | + +The children of a subproof or root are the items that follow it, each +followed by its own children. Reference record: `kind` (u8: 0 line, 1 range, +2 name), 3 zero bytes, `first` (u32: line number, or string for names), `last` +(u32). + +--- + +## 3. Reader obligations + +A conforming reader rejects the file (and must not read out of bounds) when: + +- the signature, header CRC, `file_size` or major version is wrong; +- a chunk header or payload extends past `file_size`, or its CRC is wrong; +- a tag repeats, a required chunk is missing, or an unknown critical chunk appears; +- any string reference does not point at the start of a NUL-terminated string + inside `STRS`; +- any expression, node, axiom, edge, proof or reference index is out of range, + or an expression references itself or a later expression; +- a record count implies a payload larger than the chunk. + +The reference reader is `src/core/binary.cpp`; `theosc inspect --chunks` +prints the chunk table of any file. + +--- + +## 4. Annotated example + +`theosc build tests/golden/binary/tiny.theo` (a modus ponens argument with one +scripture axiom) produces a 452-byte file. `theosc inspect --chunks` lists: + +``` +tag offset length crc status +META 00000018 20 0CAD82AC ok +STRS 00000038 73 FDC87A18 ok +FORM 00000090 56 EF2B231A ok +AXIM 000000D4 28 6AF8D58E ok +DEFN 000000FC 8 6A5B503F ok +NODE 00000110 100 6938B645 ok +EDGE 00000180 20 48AC2821 ok +DIAL 000001A0 4 40614F55 ok +PROF 000001B0 8 A545DE26 ok +``` + +Signature and header: + +``` +00000000 89 54 48 45 4F 0D 0A 1A signature +00000008 02 00 00 00 version 2.0 +0000000C 09 00 00 00 9 chunks +00000010 C4 01 00 00 file_size = 452 +00000014 F8 D4 E2 24 header_crc +``` + +The `FORM` chunk holds `A`, `B` and `A -> B` as three records; the +implication refers back to the two atoms by index: + +``` +00000090 46 4F 52 4D 38 00 00 00 1A 23 2B EF tag "FORM", length 56, crc +0000009C 03 00 00 00 00 00 00 00 3 expressions, empty argument pool +000000A4 02 00 00 00 34 00 00 00 00 00 00 00 00 00 00 00 #0 Atom "A" (string at 0x34) +000000B4 02 00 00 00 36 00 00 00 00 00 00 00 00 00 00 00 #1 Atom "B" (string at 0x36) +000000C4 0A 00 00 00 00 00 00 00 00 00 00 00 01 00 00 00 #2 Implies a = #0, b = #1 +``` + +The scripture axiom `John 1:1` is stored resolved: kind 0, canon 0 +(protestant), book 43, chapter 1, verse 1, end 1:1: + +``` +000000E0 01 00 00 00 1 axiom +000000E4 00 00 2B 00 01 00 01 00 01 00 01 00 kind, canon, book 0x2B = 43, 1:1-1:1 +000000F0 29 00 00 00 2B 00 00 00 00 00 00 00 id "J", citation "John 1:1", no locator +``` diff --git a/fuzz/CMakeLists.txt b/fuzz/CMakeLists.txt new file mode 100644 index 0000000..6adc65c --- /dev/null +++ b/fuzz/CMakeLists.txt @@ -0,0 +1,6 @@ +# Built with -DTHEOS_FUZZ=ON using Clang 19+; run e.g. ./build/fuzz/decode_fuzzer -max_total_time=60 fuzz/corpus/decode +foreach(target decode_fuzzer parse_fuzzer) + add_executable(${target} ${target}.cpp) + target_link_libraries(${target} PRIVATE theos_core theos_warnings) + target_link_options(${target} PRIVATE -fsanitize=fuzzer) +endforeach() diff --git a/fuzz/corpus/decode/tiny.theos b/fuzz/corpus/decode/tiny.theos new file mode 100644 index 0000000..34e6f7e Binary files /dev/null and b/fuzz/corpus/decode/tiny.theos differ diff --git a/fuzz/corpus/parse/aquinas_first_way.theo b/fuzz/corpus/parse/aquinas_first_way.theo new file mode 100644 index 0000000..b375bcf --- /dev/null +++ b/fuzz/corpus/parse/aquinas_first_way.theo @@ -0,0 +1,43 @@ +// The First Way (argument from motion), Summa Theologiae I, q.2, a.3. +// The regress premise is stated explicitly so the inference is deductively valid. + +argument "The First Way: Argument from Motion" by "Thomas Aquinas" + +axiom ST = source("Thomas Aquinas, Summa Theologiae", "I, q.2, a.3") +axiom Ps102 = scripture(protestant, "Psalms 102:25-27") +axiom Heb1 = scripture(protestant, "Hebrews 1:3") + +premise P1 grounded_by [ST] { + text: "Some things in the world are in motion." + formula: exists x. Moved(x) +} + +premise P2 grounded_by [ST] { + text: "Whatever is moved is moved by something other than itself." + formula: forall x. Moved(x) -> exists y. (Moves(y, x) & y != x) +} + +premise P3 grounded_by [ST] { + text: "An infinite regress of movers is impossible." + formula: ~Regress +} + +premise P4 grounded_by [ST] { + text: "If something is moved, every moved thing has another mover, and every mover is itself moved, then there is an infinite regress of movers." + formula: (exists x. Moved(x)) & (forall x. Moved(x) -> exists y. (Moves(y, x) & y != x)) & (forall x. forall y. Moved(x) & Moves(y, x) -> Moved(y)) -> Regress +} + +premise P5 grounded_by [ST, Ps102, Heb1] { + text: "A first mover, itself unmoved, is what everyone understands to be God." + formula: forall y. (~Moved(y) & exists x. Moves(y, x)) -> God(y) +} + +deduction D1 from [P1, P2, P3, P4] { + text: "Therefore there is a first mover, moved by no other." + formula: exists y. (~Moved(y) & exists x. Moves(y, x)) +} + +conclusion C1 from [D1, P5] { + text: "Therefore God exists." + formula: exists y. God(y) +} diff --git a/fuzz/corpus/parse/full_document.theo b/fuzz/corpus/parse/full_document.theo new file mode 100644 index 0000000..e705514 --- /dev/null +++ b/fuzz/corpus/parse/full_document.theo @@ -0,0 +1,39 @@ +argument "Golden" by "Tests" + +import "lib/shared" + +axiom S = scripture(catholic, "Wisdom 13:1-9") +axiom W = source("Aristotle, Physics", "VIII.5") +axiom N = principle("Nothing comes from nothing.") + +define Contingent(x) := <>~Exists(x) +define G(x) := forall F:prop. Positive(F) -> F(x) + +premise P1 grounded_by [S, W] { + text: "Some things are contingent." + formula: ∃x. Contingent(x) +} + +premise P2 grounded_by [N] { + text: "Contingent things need a cause." + formula: forall x. Contingent(x) -> exists y. (Causes(y, x) & x != y) +} + +conclusion C1 from [P1, P2] { + text: "Something causes something." + formula: exists x y. Causes(y, x) + proof { + 1. exists x. Contingent(x) premise P1 + { [a] + 2. Contingent(a) assume + 3. Contingent(a) -> exists y. (Causes(y, a) & a != y) forall_e P2 + } + box { + 4. []A reit 1 + } + 5. exists x y. Causes(y, x) exists_e 1, 2-4 + } +} + +objection O1 against P2 { text: "Causation might be an illusion." } +reply R1 to O1 { text: "Then so is the objection's motivation." formula: ~Illusion } diff --git a/fuzz/corpus/parse/resurrection.theo b/fuzz/corpus/parse/resurrection.theo new file mode 100644 index 0000000..8b5174e --- /dev/null +++ b/fuzz/corpus/parse/resurrection.theo @@ -0,0 +1,42 @@ +// A minimal-facts argument for the resurrection. The inference to the best +// explanation is made an explicit premise (P4), which is where debate belongs. + +argument "Historical Case for the Resurrection" by "Theos Examples" + +axiom Cor15 = scripture(protestant, "1 Corinthians 15:3-8") +axiom Mk16 = scripture(protestant, "Mark 16:1-8") +axiom Lk24 = scripture(protestant, "Luke 24:36-43") +axiom IBE = principle("The hypothesis that best explains the established facts is probably true.") + +premise P1 grounded_by [Cor15] { + text: "Jesus died by crucifixion and was buried." + formula: Died +} + +premise P2 grounded_by [Mk16] { + text: "The tomb was found empty shortly after." + formula: EmptyTomb +} + +premise P3 grounded_by [Cor15, Lk24] { + text: "Individuals and groups experienced appearances of Jesus alive." + formula: Appearances +} + +premise P4 grounded_by [IBE] { + text: "If Jesus died, the tomb was empty and he appeared alive, the best explanation is that God raised him." + formula: Died & EmptyTomb & Appearances -> Raised +} + +conclusion C1 from [P1, P2, P3, P4] { + text: "God raised Jesus from the dead." + formula: Raised +} + +objection O1 against P4 { + text: "Grief hallucinations explain the appearances without a resurrection." +} + +reply R1 to O1 { + text: "Hallucinations are private; they do not explain group appearances or the empty tomb." +} diff --git a/fuzz/decode_fuzzer.cpp b/fuzz/decode_fuzzer.cpp new file mode 100644 index 0000000..5a398b2 --- /dev/null +++ b/fuzz/decode_fuzzer.cpp @@ -0,0 +1,11 @@ +// libFuzzer target: decoding arbitrary bytes must either succeed or throw FormatError, never crash +#include "theos/binary.hpp" + +extern "C" int LLVMFuzzerTestOneInput(const uint8_t* data, size_t size) { + try { + auto doc = Theos::Binary::decode(std::as_bytes(std::span(data, size))); + (void)Theos::AST::dump(doc); + } catch (const Theos::Binary::FormatError&) { + } + return 0; +} diff --git a/fuzz/parse_fuzzer.cpp b/fuzz/parse_fuzzer.cpp new file mode 100644 index 0000000..b23d3e9 --- /dev/null +++ b/fuzz/parse_fuzzer.cpp @@ -0,0 +1,9 @@ +// libFuzzer target: checking arbitrary source text must report diagnostics, never crash +#include "theos/driver.hpp" +#include + +extern "C" int LLVMFuzzerTestOneInput(const uint8_t* data, size_t size) { + auto result = Theos::Driver::check_source(std::string(reinterpret_cast(data), size), "fuzz.theo"); + (void)Theos::Driver::render_diagnostics(result); + return 0; +} diff --git a/include/theos/binary.hpp b/include/theos/binary.hpp new file mode 100644 index 0000000..bf5cd5e --- /dev/null +++ b/include/theos/binary.hpp @@ -0,0 +1,44 @@ +#pragma once + +#include "theos/ast.hpp" +#include +#include +#include +#include +#include + +// The .theos v2 binary format (docs/spec/theos-v2.md) +namespace Theos::Binary { + +constexpr uint16_t VERSION_MAJOR = 2; +constexpr uint16_t VERSION_MINOR = 0; + +// Malformed or corrupted input; the message names what is wrong and where +struct FormatError : std::runtime_error { + using std::runtime_error::runtime_error; +}; + +std::vector encode(const AST::Document& doc); +AST::Document decode(std::span bytes); + +struct ChunkInfo { + std::string tag; + uint32_t offset = 0; // of the chunk header + uint32_t length = 0; // payload bytes + uint32_t crc = 0; // stored + bool crc_ok = false; +}; + +struct FileInfo { + uint16_t version_major = 0; + uint16_t version_minor = 0; + uint32_t file_size = 0; + std::vector chunks; +}; + +// Verifies signature and header, then lists chunks without decoding them (chunk CRCs are reported, not enforced) +FileInfo describe(std::span bytes); + +uint32_t crc32(std::span bytes); + +} // namespace Theos::Binary diff --git a/src/cli/main.cpp b/src/cli/main.cpp index 8357c58..8d151fc 100644 --- a/src/cli/main.cpp +++ b/src/cli/main.cpp @@ -1,5 +1,9 @@ +#include "theos/binary.hpp" #include "theos/driver.hpp" #include "theos/exporter.hpp" +#include +#include +#include #include #include #include @@ -14,14 +18,17 @@ constexpr const char* usage = "theosc - the Theos argument compiler\n" "\n" "Usage:\n" - " theosc check \n" - " theosc export --format mermaid [-o ]\n"; + " theosc check \n" + " theosc export --format mermaid [-o ]\n" + " theosc build [-o ]\n" + " theosc inspect [--chunks]\n"; struct Args { std::string command; std::string input; std::string format; std::string output; + bool chunks = false; }; std::optional parse_args(int argc, char* argv[]) { @@ -32,6 +39,7 @@ std::optional parse_args(int argc, char* argv[]) { const std::string arg = argv[i]; if (arg == "--format" && i + 1 < argc) a.format = argv[++i]; else if (arg == "-o" && i + 1 < argc) a.output = argv[++i]; + else if (arg == "--chunks") a.chunks = true; else if (a.input.empty() && !arg.starts_with("-")) a.input = arg; else return std::nullopt; } @@ -39,18 +47,79 @@ std::optional parse_args(int argc, char* argv[]) { return a; } -void write_output(const std::string& path, const std::string& content) { +std::vector read_bytes(const std::string& path) { + std::ifstream in(path, std::ios::binary); + if (!in) throw std::runtime_error("cannot open '" + path + "'"); + std::vector chars{std::istreambuf_iterator(in), {}}; + std::vector bytes(chars.size()); + std::memcpy(bytes.data(), chars.data(), chars.size()); + return bytes; +} + +void write_bytes(const std::string& path, std::span bytes) { + std::ofstream out(path, std::ios::binary); + if (!out) throw std::runtime_error("cannot write '" + path + "'"); + out.write(reinterpret_cast(bytes.data()), static_cast(bytes.size())); +} + +void write_text(const std::string& path, const std::string& content) { if (path.empty()) { std::cout << content; return; } - std::ofstream out(path, std::ios::binary); - if (!out) throw std::runtime_error("cannot write '" + path + "'"); - out << content; + write_bytes(path, std::as_bytes(std::span(content))); +} + +std::string hex(uint32_t v, int width) { + char buf[16]; + std::snprintf(buf, sizeof buf, "%0*X", width, v); + return buf; +} + +std::string hex_dump(std::span bytes, uint32_t base) { + std::string out; + for (size_t row = 0; row < bytes.size(); row += 16) { + out += " " + hex(static_cast(base + row), 8) + " "; + std::string ascii; + for (size_t i = row; i < row + 16; ++i) { + if (i < bytes.size()) { + const auto b = static_cast(bytes[i]); + out += hex(b, 2) + " "; + ascii += (b >= 0x20 && b < 0x7F) ? static_cast(b) : '.'; + } else { + out += " "; + } + } + out += " " + ascii + "\n"; + } + return out; +} + +int inspect(const Args& args) { + const auto bytes = read_bytes(args.input); + if (!args.chunks) { + std::cout << Theos::AST::dump(Theos::Binary::decode(bytes)); + return 0; + } + const auto info = Theos::Binary::describe(bytes); + std::cout << ".theos v" << info.version_major << "." << info.version_minor << ", " << info.file_size << " bytes, " + << info.chunks.size() << " chunks\n\n"; + std::cout << hex_dump(std::span(bytes).first(24), 0) << "\n"; + std::cout << " tag offset length crc status\n"; + for (const auto& c : info.chunks) { + std::cout << " " << c.tag << " " << hex(c.offset, 8) << " " << std::to_string(c.length) << std::string(8 - std::min(8, std::to_string(c.length).size()), ' ') + << hex(c.crc, 8) << " " << (c.crc_ok ? "ok" : "CORRUPT") << "\n"; + } + for (const auto& c : info.chunks) { + std::cout << "\n " << c.tag << "\n" << hex_dump(std::span(bytes).subspan(c.offset, 12 + std::min(c.length, 64)), c.offset); + if (c.length > 64) std::cout << " ... " << (c.length - 64) << " more bytes\n"; + } + return 0; } int run(const Args& args) { - if (args.command != "check" && args.command != "export") return EXIT_USAGE; + if (args.command == "inspect") return inspect(args); + if (args.command != "check" && args.command != "export" && args.command != "build") return EXIT_USAGE; if (args.command == "export" && args.format != "mermaid") return EXIT_USAGE; auto result = Theos::Driver::check_file(args.input); @@ -61,7 +130,14 @@ int run(const Args& args) { std::cerr << args.input << ": ok\n"; return 0; } - write_output(args.output, Theos::Exporter::to_mermaid(*result.doc)); + if (args.command == "build") { + const std::string out = args.output.empty() + ? std::filesystem::path(args.input).replace_extension(".theos").string() + : args.output; + write_bytes(out, Theos::Binary::encode(*result.doc)); + return 0; + } + write_text(args.output, Theos::Exporter::to_mermaid(*result.doc)); return 0; } diff --git a/src/core/binary.cpp b/src/core/binary.cpp new file mode 100644 index 0000000..21340ac --- /dev/null +++ b/src/core/binary.cpp @@ -0,0 +1,773 @@ +#include "theos/binary.hpp" +#include "theos/canon.hpp" +#include +#include +#include +#include +#include + +namespace Theos::Binary { + +namespace { + +constexpr std::array signature = { + std::byte{0x89}, std::byte{'T'}, std::byte{'H'}, std::byte{'E'}, + std::byte{'O'}, std::byte{0x0D}, std::byte{0x0A}, std::byte{0x1A}, +}; +constexpr size_t HEADER_END = 24; +constexpr size_t CHUNK_HEADER = 12; +constexpr uint32_t NONE = 0xFFFFFFFF; +// Deeper structures are rejected so recursive consumers (printing, checking) cannot exhaust the stack +constexpr size_t MAX_DEPTH = 512; + +constexpr size_t EXPR_RECORD = 16; +constexpr size_t AXIOM_RECORD = 24; +constexpr size_t DEF_RECORD = 16; +constexpr size_t PARAM_RECORD = 8; +constexpr size_t NODE_RECORD = 32; +constexpr size_t DIAL_RECORD = 20; +constexpr size_t PROOF_ITEM = 24; +constexpr size_t PROOF_REF = 12; + +constexpr std::array required_chunks = {"META", "STRS", "FORM", "NODE"}; +constexpr std::array known_chunks = {"META", "STRS", "FORM", "AXIM", "DEFN", "NODE", "EDGE", "DIAL", "PROF"}; + +std::array make_crc_table() { + std::array table{}; + for (uint32_t i = 0; i < 256; ++i) { + uint32_t c = i; + for (int k = 0; k < 8; ++k) c = (c & 1) ? 0xEDB88320u ^ (c >> 1) : c >> 1; + table[i] = c; + } + return table; +} + +uint32_t crc_update(uint32_t crc, std::span bytes) { + static const auto table = make_crc_table(); + for (std::byte b : bytes) crc = table[(crc ^ static_cast(b)) & 0xFF] ^ (crc >> 8); + return crc; +} + +// ---------------------------------------------------------------- writing + +class Buffer { +public: + void u8(uint8_t v) { bytes_.push_back(std::byte{v}); } + void u16(uint16_t v) { + u8(static_cast(v)); + u8(static_cast(v >> 8)); + } + void u32(uint32_t v) { + u16(static_cast(v)); + u16(static_cast(v >> 16)); + } + void raw(std::span b) { bytes_.insert(bytes_.end(), b.begin(), b.end()); } + void pad4() { + while (bytes_.size() % 4) u8(0); + } + void patch_u32(size_t at, uint32_t v) { + for (int i = 0; i < 4; ++i) bytes_[at + static_cast(i)] = std::byte{static_cast(v >> (8 * i))}; + } + size_t size() const { return bytes_.size(); } + std::vector& bytes() { return bytes_; } + +private: + std::vector bytes_; +}; + +uint32_t checked_u32(size_t n, std::string_view what) { + if (n >= NONE) throw FormatError(std::string(what) + " too large for the .theos format"); + return static_cast(n); +} + +uint16_t checked_u16(size_t n, std::string_view what) { + if (n > 0xFFFF) throw FormatError(std::string(what) + " too large for the .theos format"); + return static_cast(n); +} + +class Encoder { +public: + explicit Encoder(const AST::Document& doc) : doc_(doc) { strings_.u8(0); } + + std::vector run() { + index_items(); + Buffer meta = encode_meta(); + Buffer axim = encode_axioms(); + Buffer defn = encode_definitions(); + Buffer node = encode_nodes(); + Buffer dial = encode_dialectics(); + // FORM, PROF, EDGE and STRS are filled while encoding the chunks above + Buffer form = finish_form(); + Buffer prof = finish_prof(); + Buffer edge = finish_edges(); + + std::vector> chunks = { + {"META", &meta}, {"STRS", &strings_}, {"FORM", &form}, {"AXIM", &axim}, {"DEFN", &defn}, + {"NODE", &node}, {"EDGE", &edge}, {"DIAL", &dial}, {"PROF", &prof}, + }; + + Buffer out; + out.raw(signature); + out.u16(VERSION_MAJOR); + out.u16(VERSION_MINOR); + out.u32(static_cast(chunks.size())); + out.u32(0); // file_size, patched below + out.u32(0); // header_crc, patched below + for (auto& [tag, buf] : chunks) { + std::vector tagged; + for (char c : tag) tagged.push_back(std::byte{static_cast(c)}); + tagged.insert(tagged.end(), buf->bytes().begin(), buf->bytes().end()); + out.raw(std::span(tagged).first(4)); + out.u32(checked_u32(buf->size(), "chunk")); + out.u32(crc32(tagged)); + out.raw(buf->bytes()); + out.pad4(); + } + out.patch_u32(16, checked_u32(out.size(), "file")); + out.patch_u32(20, crc32(std::span(out.bytes()).first(20))); + return std::move(out.bytes()); + } + +private: + void index_items() { + for (size_t i = 0; i < doc_.axioms.size(); ++i) axiom_index_[doc_.axioms[i].id] = static_cast(i); + for (size_t i = 0; i < doc_.nodes.size(); ++i) node_index_[doc_.nodes[i].id] = static_cast(i); + for (size_t i = 0; i < doc_.dialectics.size(); ++i) dial_index_[doc_.dialectics[i].id] = static_cast(i); + } + + uint32_t str(const std::string& s) { + if (s.empty()) return 0; + auto it = string_offsets_.find(s); + if (it != string_offsets_.end()) return it->second; + const uint32_t offset = checked_u32(strings_.size(), "string table"); + for (char c : s) strings_.u8(static_cast(c)); + strings_.u8(0); + string_offsets_.emplace(s, offset); + return offset; + } + + static uint32_t lookup(const std::unordered_map& map, const std::string& name) { + auto it = map.find(name); + if (it == map.end()) throw FormatError("cannot encode reference to unknown item '" + name + "'; validate first"); + return it->second; + } + + // Structurally identical expressions get one record; children are always encoded first + uint32_t expr(const Expr& e) { + std::vector children; + for (const auto& arg : e.args) children.push_back(expr(*arg)); + + uint32_t a = 0, b = 0; + uint16_t argc = 0; + if (e.kind == ExprKind::Atom) { + argc = checked_u16(children.size(), "atom arguments"); + a = checked_u32(pool_.size(), "argument pool"); + pool_.insert(pool_.end(), children.begin(), children.end()); + } else { + if (!children.empty()) a = children[0]; + if (children.size() > 1) b = children[1]; + } + const uint32_t name = str(e.name); + const uint8_t sort = is_binder(e.kind) && e.sort == Sort::Prop ? 1 : 0; + + auto key = std::make_tuple(static_cast(e.kind), sort, name, children); + auto it = expr_index_.find(key); + if (it != expr_index_.end()) { + if (e.kind == ExprKind::Atom) pool_.resize(a); // discard the duplicate argument run + return it->second; + } + const uint32_t index = checked_u32(expr_count_++, "expression table"); + exprs_.u8(static_cast(e.kind)); + exprs_.u8(sort); + exprs_.u16(argc); + exprs_.u32(name); + exprs_.u32(a); + exprs_.u32(b); + expr_index_.emplace(std::move(key), index); + return index; + } + + Buffer encode_meta() { + Buffer b; + b.u32(doc_.title ? 1 : 0); + b.u32(doc_.title ? str(*doc_.title) : 0); + b.u32(str(doc_.author)); + b.u32(str(doc_.file)); + b.u32(checked_u32(doc_.imports.size(), "imports")); + for (const auto& imp : doc_.imports) b.u32(str(imp.path)); + return b; + } + + Buffer encode_axioms() { + Buffer b; + b.u32(checked_u32(doc_.axioms.size(), "axioms")); + for (const auto& ax : doc_.axioms) { + const bool scripture = ax.kind == AST::AxiomKind::Scripture; + b.u8(static_cast(ax.kind)); + b.u8(scripture ? static_cast(ax.scripture.canon) : 0); + b.u16(scripture ? ax.scripture.book : 0); + b.u16(scripture ? ax.scripture.chapter : 0); + b.u16(scripture ? ax.scripture.verse : 0); + b.u16(scripture ? ax.scripture.end_chapter : 0); + b.u16(scripture ? ax.scripture.end_verse : 0); + b.u32(str(ax.id)); + b.u32(str(ax.citation)); + b.u32(str(ax.locator)); + } + return b; + } + + Buffer encode_definitions() { + Buffer defs, params; + uint32_t param_count = 0; + for (const auto& def : doc_.definitions) { + defs.u32(str(def.id)); + defs.u32(expr(*def.body)); + defs.u32(param_count); + defs.u32(checked_u32(def.params.size(), "parameters")); + for (const auto& p : def.params) { + params.u32(str(p.name)); + params.u8(p.sort == Sort::Prop ? 1 : 0); + params.u8(0); + params.u16(0); + ++param_count; + } + } + Buffer b; + b.u32(checked_u32(doc_.definitions.size(), "definitions")); + b.u32(param_count); + b.raw(defs.bytes()); + b.raw(params.bytes()); + return b; + } + + Buffer encode_nodes() { + Buffer b; + b.u32(checked_u32(doc_.nodes.size(), "nodes")); + for (const auto& n : doc_.nodes) { + const uint8_t flags = (n.imported ? 1 : 0) | (n.rule ? 2 : 0) | (n.proof ? 4 : 0); + const uint32_t formula = expr(*n.formula); + const uint32_t proof = n.proof ? encode_proof(*n.proof) : 0; + const uint32_t edge_start = checked_u32(edges_.size(), "edge pool"); + for (const auto& r : n.from) edges_.push_back(lookup(node_index_, r.name)); + for (const auto& r : n.grounded_by) edges_.push_back(lookup(axiom_index_, r.name)); + b.u8(static_cast(n.kind)); + b.u8(flags); + b.u16(0); + b.u32(str(n.id)); + b.u32(str(n.text)); + b.u32(formula); + b.u32(n.rule ? str(n.rule->name) : 0); + b.u32(proof); + b.u32(edge_start); + b.u16(checked_u16(n.from.size(), "'from' list")); + b.u16(checked_u16(n.grounded_by.size(), "'grounded_by' list")); + } + return b; + } + + Buffer encode_dialectics() { + Buffer b; + b.u32(checked_u32(doc_.dialectics.size(), "objections and replies")); + for (const auto& d : doc_.dialectics) { + const bool objection = d.kind == AST::DialecticKind::Objection; + b.u8(objection ? 0 : 1); + b.u8(objection ? 0 : 1); + b.u16(0); + b.u32(str(d.id)); + b.u32(str(d.text)); + b.u32(d.formula ? expr(*d.formula) : NONE); + b.u32(objection ? lookup(node_index_, d.target.name) : lookup(dial_index_, d.target.name)); + } + return b; + } + + uint32_t encode_proof(const AST::Proof& proof) { + const uint32_t root = checked_u32(proof_count_, "proof items"); + proof_item(2, 0, checked_u32(proof.items.size(), "proof"), 0, 0, 0, 0); + encode_items(proof.items); + return root; + } + + void encode_items(const std::vector& items) { + for (const auto& item : items) { + if (const auto* line = std::get_if(&item)) { + const uint32_t formula = expr(*line->formula); + const uint32_t ref_start = checked_u32(ref_count_, "proof references"); + for (const auto& r : line->refs) { + refs_.u8(static_cast(r.kind)); + refs_.u8(0); + refs_.u16(0); + refs_.u32(r.kind == AST::ProofRef::Kind::Name ? str(r.name) : r.first); + refs_.u32(r.last); + ++ref_count_; + } + proof_item(0, 0, line->number, formula, str(line->rule.name), ref_start, + checked_u16(line->refs.size(), "line references")); + } else { + const auto& sub = std::get(item); + const uint8_t flags = (sub.strict ? 1 : 0) | (sub.fresh ? 2 : 0); + proof_item(1, flags, checked_u32(sub.items.size(), "subproof"), sub.fresh ? str(sub.fresh->name) : 0, 0, 0, 0); + encode_items(sub.items); + } + } + } + + void proof_item(uint8_t type, uint8_t flags, uint32_t a, uint32_t b, uint32_t c, uint32_t d, uint16_t ref_count) { + proofs_.u8(type); + proofs_.u8(flags); + proofs_.u16(ref_count); + proofs_.u32(a); + proofs_.u32(b); + proofs_.u32(c); + proofs_.u32(d); + proofs_.u32(0); + ++proof_count_; + } + + Buffer finish_form() { + Buffer b; + b.u32(checked_u32(expr_count_, "expression table")); + b.u32(checked_u32(pool_.size(), "argument pool")); + b.raw(exprs_.bytes()); + for (uint32_t i : pool_) b.u32(i); + return b; + } + + Buffer finish_prof() { + Buffer b; + b.u32(checked_u32(proof_count_, "proof items")); + b.u32(checked_u32(ref_count_, "proof references")); + b.raw(proofs_.bytes()); + b.raw(refs_.bytes()); + return b; + } + + Buffer finish_edges() { + Buffer b; + b.u32(checked_u32(edges_.size(), "edge pool")); + for (uint32_t e : edges_) b.u32(e); + return b; + } + + const AST::Document& doc_; + Buffer strings_; + std::unordered_map string_offsets_; + std::unordered_map axiom_index_, node_index_, dial_index_; + + Buffer exprs_; + size_t expr_count_ = 0; + std::vector pool_; + std::map>, uint32_t> expr_index_; + + Buffer proofs_, refs_; + size_t proof_count_ = 0, ref_count_ = 0; + std::vector edges_; +}; + +// ---------------------------------------------------------------- reading + +// Bounds-checked little-endian view over one chunk payload (or the whole file) +class View { +public: + View(std::span bytes, std::string name) : bytes_(bytes), name_(std::move(name)) {} + + uint8_t u8(size_t at) const { return static_cast(byte(at)); } + uint16_t u16(size_t at) const { return static_cast(u8(at) | (u8(at + 1) << 8)); } + uint32_t u32(size_t at) const { return static_cast(u16(at)) | (static_cast(u16(at + 2)) << 16); } + size_t size() const { return bytes_.size(); } + std::span bytes() const { return bytes_; } + const std::string& name() const { return name_; } + + // Throws unless [offset, offset + count * record) lies inside the view + void require(size_t offset, size_t count, size_t record, std::string_view what) const { + if (offset > bytes_.size() || (record && count > (bytes_.size() - offset) / record)) { + throw FormatError(name_ + ": " + std::string(what) + " extends past the end of the chunk"); + } + } + +private: + std::byte byte(size_t at) const { + if (at >= bytes_.size()) throw FormatError(name_ + ": read past end at offset " + std::to_string(at)); + return bytes_[at]; + } + + std::span bytes_; + std::string name_; +}; + +struct Chunk { + ChunkInfo info; + std::span payload; +}; + +std::vector read_chunks(std::span bytes, FileInfo& file, bool enforce_crc) { + if (bytes.size() < HEADER_END) throw FormatError("file too small to be a .theos file"); + if (!std::equal(signature.begin(), signature.end(), bytes.begin())) { + throw FormatError("bad signature: not a .theos file, or corrupted by a text-mode transfer"); + } + View header(bytes, "header"); + if (header.u32(20) != crc32(bytes.first(20))) throw FormatError("header CRC mismatch"); + file.version_major = header.u16(8); + file.version_minor = header.u16(10); + file.file_size = header.u32(16); + if (file.version_major != VERSION_MAJOR) { + throw FormatError("unsupported .theos version " + std::to_string(file.version_major) + "." + std::to_string(file.version_minor)); + } + if (file.file_size != bytes.size()) { + throw FormatError("file size mismatch: header says " + std::to_string(file.file_size) + " bytes, file has " + std::to_string(bytes.size())); + } + + const uint32_t chunk_count = header.u32(12); + std::vector chunks; + size_t pos = HEADER_END; + for (uint32_t i = 0; i < chunk_count; ++i) { + if (bytes.size() - pos < CHUNK_HEADER) throw FormatError("chunk " + std::to_string(i) + " header extends past end of file"); + View h(bytes.subspan(pos, CHUNK_HEADER), "chunk header"); + Chunk c; + for (size_t k = 0; k < 4; ++k) c.info.tag += static_cast(h.u8(k)); + c.info.offset = static_cast(pos); + c.info.length = h.u32(4); + c.info.crc = h.u32(8); + for (char ch : c.info.tag) { + if (!((ch >= 'A' && ch <= 'Z') || (ch >= 'a' && ch <= 'z'))) throw FormatError("invalid chunk tag at offset " + std::to_string(pos)); + } + if (c.info.length > bytes.size() - pos - CHUNK_HEADER) throw FormatError(c.info.tag + ": payload extends past end of file"); + c.payload = bytes.subspan(pos + CHUNK_HEADER, c.info.length); + c.info.crc_ok = crc_update(crc_update(0xFFFFFFFFu, bytes.subspan(pos, 4)), c.payload) == ~c.info.crc; + if (enforce_crc && !c.info.crc_ok) throw FormatError(c.info.tag + ": CRC mismatch (chunk corrupted)"); + for (const auto& prev : chunks) { + if (prev.info.tag == c.info.tag) throw FormatError(c.info.tag + ": chunk appears twice"); + } + file.chunks.push_back(c.info); + chunks.push_back(c); + pos += CHUNK_HEADER + c.info.length; + const size_t padding = (4 - pos % 4) % 4; + if (padding > bytes.size() - pos) throw FormatError(c.info.tag + ": padding extends past end of file"); + for (size_t k = 0; k < padding; ++k) { + if (bytes[pos + k] != std::byte{0}) throw FormatError(c.info.tag + ": non-zero padding"); + } + pos += padding; + } + if (pos != bytes.size()) throw FormatError("trailing bytes after the last chunk"); + return chunks; +} + +class Decoder { +public: + explicit Decoder(std::span bytes) { + FileInfo info; + for (auto& c : read_chunks(bytes, info, true)) { + const bool known = std::ranges::find(known_chunks, c.info.tag) != known_chunks.end(); + if (!known) { + if (c.info.tag[0] >= 'A' && c.info.tag[0] <= 'Z') throw FormatError(c.info.tag + ": unknown critical chunk"); + continue; // ancillary: safe to skip + } + chunks_.emplace(c.info.tag, View(c.payload, c.info.tag)); + } + for (auto tag : required_chunks) { + if (!chunks_.contains(std::string(tag))) throw FormatError("missing required chunk " + std::string(tag)); + } + } + + AST::Document run() { + AST::Document doc; + decode_form(); + decode_meta(doc); + const auto axioms = optional_count("AXIM"); + const auto nodes = view("NODE").u32(0); + const auto dials = optional_count("DIAL"); + decode_axioms(doc, axioms); + decode_definitions(doc); + decode_nodes(doc, nodes); + decode_dialectics(doc, dials); + return doc; + } + +private: + const View& view(const std::string& tag) const { return chunks_.at(tag); } + + uint32_t optional_count(const std::string& tag) const { + auto it = chunks_.find(tag); + return it == chunks_.end() ? 0 : it->second.u32(0); + } + + std::string str(uint32_t offset) const { + const View& s = view("STRS"); + if (offset >= s.size()) throw FormatError("STRS: string reference " + std::to_string(offset) + " out of range"); + if (offset > 0 && s.u8(offset - 1) != 0) throw FormatError("STRS: string reference " + std::to_string(offset) + " points inside a string"); + const auto bytes = s.bytes().subspan(offset); + const auto end = std::ranges::find(bytes, std::byte{0}); + if (end == bytes.end()) throw FormatError("STRS: unterminated string at " + std::to_string(offset)); + std::string out; + for (auto it = bytes.begin(); it != end; ++it) out += static_cast(*it); + return out; + } + + static uint32_t index(uint32_t i, size_t limit, const std::string& what) { + if (i >= limit) throw FormatError(what + " index " + std::to_string(i) + " out of range (" + std::to_string(limit) + ")"); + return i; + } + + ExprPtr expr_at(uint32_t i, const std::string& what) const { return exprs_[index(i, exprs_.size(), what + ": expression")]; } + + void decode_form() { + const View& v = view("FORM"); + const uint32_t count = v.u32(0); + const uint32_t pool_count = v.u32(4); + v.require(8, count, EXPR_RECORD, "expression records"); + const size_t pool_at = 8 + size_t{count} * EXPR_RECORD; + v.require(pool_at, pool_count, 4, "argument pool"); + + exprs_.reserve(count); + std::vector depth; + depth.reserve(count); + for (uint32_t i = 0; i < count; ++i) { + const size_t at = 8 + size_t{i} * EXPR_RECORD; + const uint8_t kind = v.u8(at); + const Sort sort = v.u8(at + 1) ? Sort::Prop : Sort::Ind; + const uint16_t argc = v.u16(at + 2); + const std::string name = str(v.u32(at + 4)); + const uint32_t a = v.u32(at + 8); + const uint32_t b = v.u32(at + 12); + // Children must precede their parent: indices are checked against i, not count + size_t d = 1; + auto child = [&](uint32_t c) { + index(c, i, "FORM: child of expression " + std::to_string(i)); + d = std::max(d, depth[c] + 1u); + return exprs_[c]; + }; + + switch (static_cast(kind)) { + case ExprKind::Symbol: exprs_.push_back(make_symbol(name)); break; + case ExprKind::Lambda: exprs_.push_back(make_binder(ExprKind::Lambda, name, sort, child(a))); break; + case ExprKind::Atom: { + if (a > pool_count || argc > pool_count - a) throw FormatError("FORM: atom arguments out of range"); + std::vector args; + for (uint32_t k = 0; k < argc; ++k) args.push_back(child(v.u32(pool_at + 4 * (size_t{a} + k)))); + exprs_.push_back(make_atom(name, std::move(args))); + break; + } + case ExprKind::Eq: { + auto l = child(a), r = child(b); + if (l->kind != ExprKind::Symbol || r->kind != ExprKind::Symbol) throw FormatError("FORM: identity must relate symbols"); + exprs_.push_back(make_eq(l, r)); + break; + } + case ExprKind::Bottom: exprs_.push_back(make_bottom()); break; + case ExprKind::Not: + case ExprKind::Box: + case ExprKind::Dia: exprs_.push_back(make_unary(static_cast(kind), child(a))); break; + case ExprKind::And: + case ExprKind::Or: + case ExprKind::Implies: + case ExprKind::Iff: exprs_.push_back(make_binary(static_cast(kind), child(a), child(b))); break; + case ExprKind::Forall: + case ExprKind::Exists: exprs_.push_back(make_binder(static_cast(kind), name, sort, child(a))); break; + default: throw FormatError("FORM: unknown expression kind " + std::to_string(kind)); + } + if (d > MAX_DEPTH) throw FormatError("FORM: expression nested deeper than " + std::to_string(MAX_DEPTH)); + depth.push_back(static_cast(d)); + } + } + + void decode_meta(AST::Document& doc) const { + const View& v = view("META"); + const uint32_t flags = v.u32(0); + if (flags & 1) doc.title = str(v.u32(4)); + doc.author = str(v.u32(8)); + doc.file = str(v.u32(12)); + const uint32_t imports = v.u32(16); + v.require(20, imports, 4, "imports"); + for (uint32_t i = 0; i < imports; ++i) doc.imports.push_back({str(v.u32(20 + 4 * size_t{i})), {}}); + } + + void decode_axioms(AST::Document& doc, uint32_t count) const { + if (!count) return; + const View& v = view("AXIM"); + v.require(4, count, AXIOM_RECORD, "axiom records"); + for (uint32_t i = 0; i < count; ++i) { + const size_t at = 4 + size_t{i} * AXIOM_RECORD; + AST::Axiom ax; + const uint8_t kind = v.u8(at); + if (kind > 2) throw FormatError("AXIM: unknown axiom kind " + std::to_string(kind)); + ax.kind = static_cast(kind); + ax.id = str(v.u32(at + 12)); + ax.citation = str(v.u32(at + 16)); + ax.locator = str(v.u32(at + 20)); + if (ax.kind == AST::AxiomKind::Scripture) { + const uint8_t canon = v.u8(at + 1); + if (canon > 3) throw FormatError("AXIM: unknown canon " + std::to_string(canon)); + ax.scripture.canon = static_cast(canon); + ax.scripture.book = v.u16(at + 2); + ax.scripture.chapter = v.u16(at + 4); + ax.scripture.verse = v.u16(at + 6); + ax.scripture.end_chapter = v.u16(at + 8); + ax.scripture.end_verse = v.u16(at + 10); + ax.canon = std::string(Scripture::name(ax.scripture.canon)); + } + doc.axioms.push_back(std::move(ax)); + } + } + + void decode_definitions(AST::Document& doc) const { + auto it = chunks_.find("DEFN"); + if (it == chunks_.end()) return; + const View& v = it->second; + const uint32_t count = v.u32(0); + const uint32_t params = v.u32(4); + v.require(8, count, DEF_RECORD, "definition records"); + const size_t params_at = 8 + size_t{count} * DEF_RECORD; + v.require(params_at, params, PARAM_RECORD, "parameters"); + for (uint32_t i = 0; i < count; ++i) { + const size_t at = 8 + size_t{i} * DEF_RECORD; + AST::Definition def; + def.id = str(v.u32(at)); + def.body = expr_at(v.u32(at + 4), "DEFN"); + const uint32_t start = v.u32(at + 8); + const uint32_t n = v.u32(at + 12); + if (start > params || n > params - start) throw FormatError("DEFN: parameters out of range"); + for (uint32_t k = 0; k < n; ++k) { + const size_t p = params_at + (size_t{start} + k) * PARAM_RECORD; + def.params.push_back({str(v.u32(p)), v.u8(p + 4) ? Sort::Prop : Sort::Ind, {}}); + } + doc.definitions.push_back(std::move(def)); + } + } + + void decode_nodes(AST::Document& doc, uint32_t count) const { + const View& v = view("NODE"); + v.require(4, count, NODE_RECORD, "node records"); + const View* edges = chunks_.contains("EDGE") ? &view("EDGE") : nullptr; + const uint32_t edge_count = edges ? edges->u32(0) : 0; + if (edges) edges->require(4, edge_count, 4, "edges"); + + std::vector node_ids; + for (uint32_t i = 0; i < count; ++i) node_ids.push_back(str(v.u32(4 + size_t{i} * NODE_RECORD + 4))); + + for (uint32_t i = 0; i < count; ++i) { + const size_t at = 4 + size_t{i} * NODE_RECORD; + AST::Node n; + const uint8_t kind = v.u8(at); + if (kind > 2) throw FormatError("NODE: unknown node kind " + std::to_string(kind)); + n.kind = static_cast(kind); + const uint8_t flags = v.u8(at + 1); + n.imported = flags & 1; + n.id = node_ids[i]; + n.text = str(v.u32(at + 8)); + n.formula = expr_at(v.u32(at + 12), "NODE"); + if (flags & 2) n.rule = AST::Ref{str(v.u32(at + 16)), {}}; + if (flags & 4) n.proof = decode_proof(v.u32(at + 20)); + const uint32_t start = v.u32(at + 24); + const uint32_t from = v.u16(at + 28); + const uint32_t grounds = v.u16(at + 30); + if (start > edge_count || from + grounds > edge_count - start) throw FormatError("NODE: edges out of range"); + for (uint32_t k = 0; k < from; ++k) { + n.from.push_back({node_ids[index(edges->u32(4 + 4 * (size_t{start} + k)), count, "EDGE: node")], {}}); + } + for (uint32_t k = 0; k < grounds; ++k) { + const uint32_t ax = index(edges->u32(4 + 4 * (size_t{start} + from + k)), doc.axioms.size(), "EDGE: axiom"); + n.grounded_by.push_back({doc.axioms[ax].id, {}}); + } + doc.nodes.push_back(std::move(n)); + } + } + + void decode_dialectics(AST::Document& doc, uint32_t count) const { + if (!count) return; + const View& v = view("DIAL"); + v.require(4, count, DIAL_RECORD, "objection records"); + std::vector ids; + for (uint32_t i = 0; i < count; ++i) ids.push_back(str(v.u32(4 + size_t{i} * DIAL_RECORD + 4))); + for (uint32_t i = 0; i < count; ++i) { + const size_t at = 4 + size_t{i} * DIAL_RECORD; + AST::Dialectic d; + d.kind = v.u8(at) ? AST::DialecticKind::Reply : AST::DialecticKind::Objection; + d.id = ids[i]; + d.text = str(v.u32(at + 8)); + const uint32_t formula = v.u32(at + 12); + if (formula != NONE) d.formula = expr_at(formula, "DIAL"); + const uint32_t target = v.u32(at + 16); + d.target.name = v.u8(at + 1) ? ids[index(target, count, "DIAL: target")] + : doc.nodes[index(target, doc.nodes.size(), "DIAL: target node")].id; + doc.dialectics.push_back(std::move(d)); + } + } + + AST::Proof decode_proof(uint32_t root) const { + const View& v = view("PROF"); + const uint32_t items = v.u32(0); + const uint32_t refs = v.u32(4); + v.require(8, items, PROOF_ITEM, "proof items"); + v.require(8 + size_t{items} * PROOF_ITEM, refs, PROOF_REF, "proof references"); + index(root, items, "NODE: proof"); + if (v.u8(8 + size_t{root} * PROOF_ITEM) != 2) throw FormatError("PROF: node proof does not point at a proof root"); + + uint32_t next = root + 1; + AST::Proof proof; + proof.items = decode_children(v, items, refs, v.u32(8 + size_t{root} * PROOF_ITEM + 4), next, 1); + return proof; + } + + std::vector decode_children(const View& v, uint32_t items, uint32_t refs, uint32_t count, uint32_t& next, + size_t depth) const { + if (depth > MAX_DEPTH) throw FormatError("PROF: subproofs nested deeper than " + std::to_string(MAX_DEPTH)); + std::vector out; + for (uint32_t c = 0; c < count; ++c) { + const size_t at = 8 + size_t{index(next++, items, "PROF: item")} * PROOF_ITEM; + const uint8_t type = v.u8(at); + if (type == 0) { + AST::ProofLine line; + line.number = v.u32(at + 4); + line.formula = expr_at(v.u32(at + 8), "PROF"); + line.rule.name = str(v.u32(at + 12)); + const uint32_t start = v.u32(at + 16); + const uint32_t n = v.u16(at + 2); + if (start > refs || n > refs - start) throw FormatError("PROF: references out of range"); + for (uint32_t k = 0; k < n; ++k) { + const size_t r = 8 + size_t{items} * PROOF_ITEM + (size_t{start} + k) * PROOF_REF; + AST::ProofRef ref; + const uint8_t kind = v.u8(r); + if (kind > 2) throw FormatError("PROF: unknown reference kind"); + ref.kind = static_cast(kind); + if (ref.kind == AST::ProofRef::Kind::Name) ref.name = str(v.u32(r + 4)); + else ref.first = v.u32(r + 4); + ref.last = v.u32(r + 8); + line.refs.push_back(std::move(ref)); + } + out.emplace_back(std::move(line)); + } else if (type == 1) { + AST::Subproof sub; + const uint8_t flags = v.u8(at + 1); + sub.strict = flags & 1; + if (flags & 2) sub.fresh = AST::Ref{str(v.u32(at + 8)), {}}; + const uint32_t children = v.u32(at + 4); + if (children > items - next) throw FormatError("PROF: subproof child count out of range"); + sub.items = decode_children(v, items, refs, children, next, depth + 1); + out.emplace_back(std::move(sub)); + } else { + throw FormatError("PROF: unexpected item type " + std::to_string(type)); + } + } + return out; + } + + std::map chunks_; + std::vector exprs_; +}; + +} // namespace + +uint32_t crc32(std::span bytes) { return ~crc_update(0xFFFFFFFFu, bytes); } + +std::vector encode(const AST::Document& doc) { return Encoder(doc).run(); } + +AST::Document decode(std::span bytes) { return Decoder(bytes).run(); } + +FileInfo describe(std::span bytes) { + FileInfo info; + read_chunks(bytes, info, false); + return info; +} + +} // namespace Theos::Binary diff --git a/src/core/parser.cpp b/src/core/parser.cpp index a9e94f6..d70359d 100644 --- a/src/core/parser.cpp +++ b/src/core/parser.cpp @@ -280,6 +280,7 @@ class Parser { } AST::ProofItem subproof() { + DepthGuard guard(*this); AST::Subproof sub; sub.span = peek().span; sub.strict = accept_keyword("box"); @@ -328,7 +329,10 @@ class Parser { // ---- formulas ---- - ExprPtr formula() { return iff(); } + ExprPtr formula() { + DepthGuard guard(*this); + return iff(); + } ExprPtr iff() { auto lhs = implies(); @@ -341,6 +345,7 @@ class Parser { } ExprPtr implies() { + DepthGuard guard(*this); auto lhs = disjunction(); if (at(Tok::Implies)) { advance(); @@ -378,6 +383,7 @@ class Parser { } ExprPtr unary() { + DepthGuard guard(*this); const Span start = peek().span; if (accept(Tok::Not)) { auto e = unary(); @@ -471,9 +477,24 @@ class Parser { return make_binder(ExprKind::Lambda, b.name, b.sort, body, join(start, body->span)); } + // Bounds recursion so hostile input cannot exhaust the stack + class DepthGuard { + public: + explicit DepthGuard(Parser& p) : p_(p) { + if (++p_.depth_ > MAX_DEPTH) p_.fail(p_.peek().span, "nesting too deep (limit " + std::to_string(MAX_DEPTH) + ")"); + } + ~DepthGuard() { --p_.depth_; } + + private: + Parser& p_; + }; + + static constexpr size_t MAX_DEPTH = 256; + std::vector toks_; std::string file_; size_t pos_ = 0; + size_t depth_ = 0; }; } // namespace diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index c16d3d8..b4a1c39 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -6,6 +6,7 @@ FetchContent_Declare(Catch2 FetchContent_MakeAvailable(Catch2) add_executable(theos_tests + test_binary.cpp test_canon.cpp test_exporter.cpp test_golden.cpp diff --git a/tests/golden/binary/tiny.out b/tests/golden/binary/tiny.out new file mode 100644 index 0000000..0c6560f --- /dev/null +++ b/tests/golden/binary/tiny.out @@ -0,0 +1,12 @@ +--- +argument "Tiny" by "Spec" +axiom J scripture protestant "John 1:1" +premise P1 grounded_by [J] + text: "A" + formula: A -> B +premise P2 grounded_by [J] + text: "B" + formula: A +conclusion C1 from [P1, P2] by imp_e + text: "C" + formula: B diff --git a/tests/golden/binary/tiny.theo b/tests/golden/binary/tiny.theo new file mode 100644 index 0000000..9bf8225 --- /dev/null +++ b/tests/golden/binary/tiny.theo @@ -0,0 +1,18 @@ +argument "Tiny" by "Spec" + +axiom J = scripture(protestant, "John 1:1") + +premise P1 grounded_by [J] { + text: "A" + formula: A -> B +} + +premise P2 grounded_by [J] { + text: "B" + formula: A +} + +conclusion C1 from [P1, P2] by imp_e { + text: "C" + formula: B +} diff --git a/tests/golden/binary/tiny.theos b/tests/golden/binary/tiny.theos new file mode 100644 index 0000000..34e6f7e Binary files /dev/null and b/tests/golden/binary/tiny.theos differ diff --git a/tests/test_binary.cpp b/tests/test_binary.cpp new file mode 100644 index 0000000..37faadf --- /dev/null +++ b/tests/test_binary.cpp @@ -0,0 +1,166 @@ +#include +#include +#include "theos/binary.hpp" +#include "theos/driver.hpp" +#include "theos/parser.hpp" +#include +#include +#include +#include + +using namespace Theos; +namespace fs = std::filesystem; + +namespace { + +AST::Document load(const fs::path& p) { + auto r = Driver::check_file(p.string()); + INFO(Driver::render_diagnostics(r)); + REQUIRE(r.ok()); + return *r.doc; +} + +std::vector valid_sources() { + std::vector out; + for (const auto& e : fs::directory_iterator(fs::path(THEOS_SOURCE_DIR) / "examples")) { + if (e.path().extension() == ".theo") out.push_back(e.path()); + } + out.push_back(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary/tiny.theo"); + return out; +} + +std::vector read_bytes(const fs::path& p) { + std::ifstream in(p, std::ios::binary); + std::vector chars{std::istreambuf_iterator(in), {}}; + std::vector bytes(chars.size()); + std::memcpy(bytes.data(), chars.data(), chars.size()); + return bytes; +} + +void put_u32(std::vector& b, size_t at, uint32_t v) { + for (size_t i = 0; i < 4; ++i) b[at + i] = std::byte{static_cast(v >> (8 * i))}; +} + +uint32_t get_u32(const std::vector& b, size_t at) { + uint32_t v = 0; + for (size_t i = 0; i < 4; ++i) v |= static_cast(b[at + i]) << (8 * i); + return v; +} + +// Appends a chunk with a valid CRC and fixes up the header so only the tag decides acceptance +std::vector with_extra_chunk(std::vector file, const std::string& tag) { + std::vector chunk; + for (char c : tag) chunk.push_back(std::byte{static_cast(c)}); + const std::vector payload = {std::byte{1}, std::byte{2}, std::byte{3}, std::byte{4}}; + std::vector tagged = chunk; + tagged.insert(tagged.end(), payload.begin(), payload.end()); + file.insert(file.end(), chunk.begin(), chunk.end()); + file.resize(file.size() + 8); + put_u32(file, file.size() - 8, 4); + put_u32(file, file.size() - 4, Binary::crc32(tagged)); + file.insert(file.end(), payload.begin(), payload.end()); + put_u32(file, 12, get_u32(file, 12) + 1); + put_u32(file, 16, static_cast(file.size())); + put_u32(file, 20, Binary::crc32(std::span(file).first(20))); + return file; +} + +} // namespace + +TEST_CASE("CRC-32 matches the IEEE reference value", "[binary]") { + const std::string check = "123456789"; + REQUIRE(Binary::crc32(std::as_bytes(std::span(check))) == 0xCBF43926u); +} + +TEST_CASE("Round trip preserves every document", "[binary]") { + for (const auto& path : valid_sources()) { + INFO(path.string()); + const auto doc = load(path); + const auto bytes = Binary::encode(doc); + const auto back = Binary::decode(bytes); + REQUIRE(AST::dump(back) == AST::dump(doc)); + REQUIRE(back.file == doc.file); + REQUIRE(Binary::encode(back) == bytes); + } +} + +TEST_CASE("Encoding is deterministic and shares sub-formulas", "[binary]") { + auto r = Driver::check_source(R"( +premise P1 { text: "a" formula: (A & B) -> (A & B) } +premise P2 { text: "b" formula: A & B } +)", "share.theo"); + REQUIRE(r.ok()); + const auto bytes = Binary::encode(*r.doc); + REQUIRE(bytes == Binary::encode(*r.doc)); + // A, B, A & B, and the implication: four records despite three occurrences of A & B + const auto info = Binary::describe(bytes); + for (const auto& c : info.chunks) { + if (c.tag == "FORM") REQUIRE(get_u32(bytes, c.offset + 12) == 4); + } +} + +TEST_CASE("Golden binaries are byte-for-byte stable", "[binary][golden]") { + const bool update = std::getenv("THEOS_UPDATE_GOLDEN") != nullptr; + for (const auto& e : fs::directory_iterator(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary")) { + if (e.path().extension() != ".theo") continue; + // Encode with a location-independent file name so golden bytes do not depend on the checkout path + auto r = Driver::check_file(e.path().string()); + REQUIRE(r.ok()); + r.doc->file = e.path().filename().string(); + const auto bytes = Binary::encode(*r.doc); + const auto golden = fs::path(e.path()).replace_extension(".theos"); + if (update) { + std::ofstream(golden, std::ios::binary).write(reinterpret_cast(bytes.data()), static_cast(bytes.size())); + continue; + } + INFO(golden.string()); + REQUIRE(read_bytes(golden) == bytes); + } +} + +TEST_CASE("Every single-byte corruption is detected", "[binary]") { + const auto bytes = Binary::encode(load(fs::path(THEOS_SOURCE_DIR) / "examples/resurrection.theo")); + for (size_t i = 0; i < bytes.size(); ++i) { + auto corrupt = bytes; + corrupt[i] ^= std::byte{0x20}; + INFO("byte " << i); + REQUIRE_THROWS_AS(Binary::decode(corrupt), Binary::FormatError); + } +} + +TEST_CASE("Every truncation is detected", "[binary]") { + const auto bytes = Binary::encode(load(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary/tiny.theo")); + for (size_t len = 0; len < bytes.size(); ++len) { + INFO("length " << len); + REQUIRE_THROWS_AS(Binary::decode(std::span(bytes).first(len)), Binary::FormatError); + } +} + +TEST_CASE("Text-mode line ending conversion is detected by the signature", "[binary]") { + auto bytes = Binary::encode(load(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary/tiny.theo")); + bytes.erase(bytes.begin() + 5); // \r\n -> \n + REQUIRE_THROWS_WITH(Binary::decode(bytes), "bad signature: not a .theos file, or corrupted by a text-mode transfer"); +} + +TEST_CASE("Unknown ancillary chunks are skipped, unknown critical chunks rejected", "[binary]") { + const auto doc = load(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary/tiny.theo"); + const auto bytes = Binary::encode(doc); + REQUIRE(AST::dump(Binary::decode(with_extra_chunk(bytes, "zNTE"))) == AST::dump(doc)); + REQUIRE_THROWS_WITH(Binary::decode(with_extra_chunk(bytes, "ZNTE")), "ZNTE: unknown critical chunk"); + REQUIRE_THROWS_WITH(Binary::decode(with_extra_chunk(bytes, "META")), "META: chunk appears twice"); +} + +TEST_CASE("Unsupported major version is rejected", "[binary]") { + auto bytes = Binary::encode(load(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary/tiny.theo")); + bytes[8] = std::byte{3}; + put_u32(bytes, 20, Binary::crc32(std::span(bytes).first(20))); + REQUIRE_THROWS_WITH(Binary::decode(bytes), "unsupported .theos version 3.0"); +} + +TEST_CASE("Deeply nested formulas are rejected by the parser", "[parser]") { + std::string deep(300, '('); + deep += "A" + std::string(300, ')'); + auto f = Parser::parse_formula(deep); + REQUIRE_FALSE(f); + REQUIRE(f.error().message.starts_with("nesting too deep")); +}