Skip to content

Commit 32b5df2

Browse files
StevenDBennettStevenDBennett
committed
v1.0.0: dyadic — Six-Axiom 2-Adic Operator Calculus
0 parents  commit 32b5df2

12 files changed

Lines changed: 3906 additions & 0 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
name: CI
2+
3+
on:
4+
push:
5+
branches: [ main ]
6+
pull_request:
7+
branches: [ main ]
8+
9+
jobs:
10+
gcc:
11+
strategy:
12+
matrix:
13+
proof: [light, heavy]
14+
runs-on: ubuntu-latest
15+
steps:
16+
- uses: actions/checkout@v4
17+
- run: sudo apt-get update && sudo apt-get install -y g++-14
18+
- name: Compile standalone headers (light proofs)
19+
if: matrix.proof == 'light'
20+
run: |
21+
printf '#include "dyadic.h"\n' | g++-14 -std=c++20 -O2 -x c++ - -c -o /dev/null -Wall -Wextra -Wpedantic -Werror
22+
printf '#include "dyadic_verify.h"\n' | g++-14 -std=c++20 -O2 -x c++ - -c -o /dev/null -Wall -Wextra -Wpedantic -Werror
23+
- name: Compile standalone headers (heavy proofs)
24+
if: matrix.proof == 'heavy'
25+
run: |
26+
printf '#include "dyadic.h"\n' | g++-14 -std=c++20 -O2 -x c++ - -c -o /dev/null -Wall -Wextra -Wpedantic -Werror -DDYADIC_HEAVY_PROOFS -fconstexpr-ops-limit=200000000
27+
printf '#include "dyadic_verify.h"\n' | g++-14 -std=c++20 -O2 -x c++ - -c -o /dev/null -Wall -Wextra -Wpedantic -Werror -DDYADIC_HEAVY_PROOFS -fconstexpr-ops-limit=200000000
28+
- name: Build and test
29+
run: |
30+
cmake -B build -DDYADIC_BUILD_TESTS=ON -DDYADIC_HEAVY_PROOFS=${{ matrix.proof == 'heavy' && 'ON' || 'OFF' }}
31+
cmake --build build
32+
ctest --test-dir build --output-on-failure
33+
34+
clang:
35+
runs-on: ubuntu-latest
36+
steps:
37+
- uses: actions/checkout@v4
38+
- run: sudo apt-get update && sudo apt-get install -y clang++-18
39+
- name: Compile standalone headers
40+
run: |
41+
printf '#include "dyadic.h"\n' | clang++-18 -std=c++20 -O2 -x c++ - -c -o /dev/null -Wall -Wextra -Wpedantic -Werror -fconstexpr-steps=50000000
42+
printf '#include "dyadic_verify.h"\n' | clang++-18 -std=c++20 -O2 -x c++ - -c -o /dev/null -Wall -Wextra -Wpedantic -Werror -fconstexpr-steps=50000000
43+
- name: Build and test
44+
run: |
45+
cmake -B build -DCMAKE_CXX_COMPILER=clang++-18 -DDYADIC_BUILD_TESTS=ON
46+
cmake --build build
47+
ctest --test-dir build --output-on-failure
48+
49+
sanitize:
50+
runs-on: ubuntu-latest
51+
steps:
52+
- uses: actions/checkout@v4
53+
- run: sudo apt-get update && sudo apt-get install -y g++-14
54+
- name: Build with ASan+UBSan
55+
run: |
56+
cmake -B build -DCMAKE_CXX_COMPILER=g++-14 -DDYADIC_BUILD_TESTS=ON
57+
cmake --build build --target test_verify_san
58+
- name: Run sanitized tests
59+
run: ./build/test_verify_san
60+
61+
msvc:
62+
runs-on: windows-latest
63+
steps:
64+
- uses: actions/checkout@v4
65+
- name: Setup MSVC dev environment
66+
uses: ilammy/msvc-dev-cmd@v1
67+
- name: Compile standalone headers
68+
shell: pwsh
69+
run: |
70+
Add-Content -Path "test_header.cpp" -Value '#include "dyadic.h"'
71+
cl /std:c++20 /EHsc /c /W4 /WX /D_SILENCE_ALL_CXX20_DEPRECATION_WARNINGS test_header.cpp
72+
Add-Content -Path "test_verify.cpp" -Value '#include "dyadic_verify.h"'
73+
cl /std:c++20 /EHsc /c /W4 /WX /D_SILENCE_ALL_CXX20_DEPRECATION_WARNINGS /constexpr:steps50000000 test_verify.cpp
74+
- name: Build and test with CMake
75+
shell: pwsh
76+
run: |
77+
cmake -B build -DDYADIC_BUILD_TESTS=ON
78+
cmake --build build --config Release
79+
ctest --test-dir build -C Release --output-on-failure --timeout 120

‎CMakeLists.txt‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
cmake_minimum_required(VERSION 3.14)
2+
project(dyadic LANGUAGES CXX)
3+
4+
# Require C++20
5+
set(CMAKE_CXX_STANDARD 20)
6+
set(CMAKE_CXX_STANDARD_REQUIRED ON)
7+
8+
# Header-only interface library for IDE discovery
9+
add_library(dyadic INTERFACE)
10+
target_include_directories(dyadic INTERFACE ${CMAKE_CURRENT_SOURCE_DIR})
11+
target_compile_features(dyadic INTERFACE cxx_std_20)
12+
13+
# Option for exhaustive compile-time proofs
14+
option(DYADIC_HEAVY_PROOFS "Enable exhaustive (but expensive) compile-time proofs" OFF)
15+
if(DYADIC_HEAVY_PROOFS)
16+
target_compile_definitions(dyadic INTERFACE DYADIC_HEAVY_PROOFS)
17+
endif()
18+
19+
# Tests (only if not being included as a subdirectory)
20+
option(DYADIC_BUILD_TESTS "Build test executables" ON)
21+
if(DYADIC_BUILD_TESTS AND NOT PROJECT_IS_SUBMODULE)
22+
enable_testing()
23+
24+
function(add_dyadic_test name source)
25+
add_executable(${name} ${source})
26+
target_link_libraries(${name} PRIVATE dyadic)
27+
# Increase constexpr evaluation budget for compile-time proofs
28+
if(CMAKE_CXX_COMPILER_ID MATCHES "GNU")
29+
target_compile_options(${name} PRIVATE -fconstexpr-ops-limit=200000000)
30+
elseif(CMAKE_CXX_COMPILER_ID MATCHES "Clang")
31+
target_compile_options(${name} PRIVATE -fconstexpr-steps=50000000)
32+
elseif(CMAKE_CXX_COMPILER_ID MATCHES "MSVC")
33+
target_compile_options(${name} PRIVATE /constexpr:steps50000000)
34+
endif()
35+
add_test(NAME ${name} COMMAND ${name})
36+
endfunction()
37+
38+
add_dyadic_test(test_verify test/test_verify.cpp)
39+
add_dyadic_test(test_property test/test_property.cpp)
40+
add_dyadic_test(test_full test/test_full.cpp)
41+
42+
# Benchmark (not part of default CTest — run manually)
43+
add_executable(benchmark test/benchmark.cpp)
44+
target_link_libraries(benchmark PRIVATE dyadic)
45+
46+
# Sanitized build target (ASan + UBSan) — GCC/Clang only
47+
if(NOT CMAKE_CXX_COMPILER_ID MATCHES "MSVC")
48+
add_executable(test_verify_san test/test_verify.cpp)
49+
target_link_libraries(test_verify_san PRIVATE dyadic)
50+
target_compile_options(test_verify_san PRIVATE
51+
-fsanitize=address,undefined -O1)
52+
target_link_options(test_verify_san PRIVATE -fsanitize=address,undefined)
53+
if(CMAKE_CXX_COMPILER_ID MATCHES "GNU")
54+
target_compile_options(test_verify_san PRIVATE
55+
-fconstexpr-ops-limit=200000000 -fconstexpr-depth=1000000)
56+
elseif(CMAKE_CXX_COMPILER_ID MATCHES "Clang")
57+
target_compile_options(test_verify_san PRIVATE
58+
-fconstexpr-steps=50000000)
59+
endif()
60+
endif()
61+
endif()

‎LICENSE‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MIT License
2+
3+
Copyright (c) 2025 Steven D Bennett
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
The above copyright notice and this permission notice shall be included in all
13+
copies or substantial portions of the Software.
14+
15+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+
SOFTWARE.

‎README.md‎

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
# dyadic — Six-Axiom 2-Adic Operator Calculus
2+
3+
Single-header C++20 library for arithmetic in ℤ₂[[t]]: carry chains, formal derivatives, forward differences, Witt vectors, basis conversions, power series composition and reversion.
4+
5+
```cpp
6+
#include "dyadic.h"
7+
#include <cstdio>
8+
using namespace dyadic;
9+
10+
int main() {
11+
Polynomial<4, uint64_t> p{{1, 2, 3, 4}};
12+
13+
// Formal derivative: D(P)(t) = dP/dt
14+
auto dp = formal_derivative(p); // {2, 6, 12, 0}
15+
for (auto c : dp) std::printf("%lu ", c);
16+
17+
// Forward difference: Δ(P)(t) = P(t+1) − P(t)
18+
auto fp = forward_difference(p); // {9, 18, 12, 0}
19+
20+
// Basis conversions (exact roundtrip)
21+
auto ff = change_basis<FallingFactorialBasis>(p);
22+
auto back = change_basis<MonomialBasis>(ff); // == p
23+
24+
// Evaluate P(5) = 1 + 2·5 + 3·25 + 4·125 = 586
25+
auto y = p.eval(5);
26+
27+
// Witt vector ring operations
28+
WittVector<3, uint64_t> a{{1, 2, 3}}, b{{4, 5, 6}};
29+
auto sum = a + b; // Witt addition (via ghost map)
30+
auto prod = a * b; // Witt multiplication
31+
32+
// Power series reversion (Lagrange inversion)
33+
Polynomial<6, uint64_t> P{{0, 1, 1}}; // t + t²
34+
auto Q = reversion(P);
35+
// Q = t − t² + 2t³ − 5t⁴ + 14t⁵ − 42t⁶ + …
36+
// (stored as unsigned ℤ₂ values: −1 ≡ 2⁶⁴−1, etc.)
37+
}
38+
```
39+
40+
## Requirements
41+
42+
- **C++20** compiler (GCC 12+, Clang 17+, MSVC 2022+)
43+
- No external dependencies
44+
- `detail::uint128_t` (software 128-bit pair) provides `uint64_t` word support without `unsigned __int128`
45+
- Clang needs `-fconstexpr-steps=50000000` for compile-time proofs; GCC needs `-fconstexpr-ops-limit=200000000`
46+
47+
## Features
48+
49+
| Area | What |
50+
|------|------|
51+
| **2-Adic Primitives** | `v2` (valuation), `modinv_odd`, `div_2k_adic`, `artin_schreier` (℘(x)=x²−x) |
52+
| **Polynomials** | `Polynomial<N,W,Basis>` with `eval`, `+`, `−`, `*`, basis conversion between Monomial / FallingFactorial / Taylor |
53+
| **Calculus** | `formal_derivative` (D), `forward_difference` (Δ), `taylor_shift`, `indefinite_sum` (Σ = Δ⁻¹) |
54+
| **Witt Vectors** | `WittVector<N,W>` with ghost map, Frobenius, Verschiebung, `+`, `*`, `adams_operation`, `teichmuller_lift` |
55+
| **Carry Chain** | Full-width carry propagation `C = (I−N)⁻¹` — converges in one pass |
56+
| **Compose / Reversion** | Power series composition P(Q(t)) and Lagrange inversion |
57+
| **Compile-Time Proofs** | 20+ `static_assert` proofs verifying ring axioms, basis roundtrips, D∘Δ=Δ∘D, ghost homomorphism, carry idempotence (see `dyadic_verify.h`) |
58+
59+
## More Examples
60+
61+
### Witt vector ring
62+
63+
```cpp
64+
WittVector<3, uint64_t> a{{1, 2, 3}}, b{{4, 5, 6}};
65+
66+
auto sum = a + b;
67+
auto prod = a * b;
68+
69+
// Frobenius and Verschiebung
70+
auto fa = a.frobenius();
71+
auto vb = b.verschiebung();
72+
// F(V(a)) == V(F(a)) — verified at compile time
73+
74+
// Adams operation ψⁿ
75+
auto psi = adams_operation(a, 3);
76+
77+
// Teichmüller lift: τ(x) = (x, 0, 0, …) (N is required)
78+
auto tau = teichmueller_lift<4>(uint64_t{7});
79+
// ghost_j(τ(ab)) = ghost_j(τ(a)) · ghost_j(τ(b)) — verified at compile time
80+
```
81+
82+
### Polynomial composition and reversion
83+
84+
```cpp
85+
Polynomial<6, uint64_t> P{{0, 1, 1}}; // P(t) = t + t²
86+
Polynomial<6, uint64_t> Q{{0, 1, 2}}; // Q(t) = t + 2t²
87+
88+
auto PQ = compose(P, Q); // P(Q(t)) — degree (N-1)*(M-1)+1 = 26
89+
auto R = reversion(P); // Lagrange inverse: P(R(t)) = t
90+
// R(t) = t − t² + 2t³ − 5t⁴ + 14t⁵ − 42t⁶ + …
91+
// (stored in ℤ₂: negative coefficients wrap modulo 2^W)
92+
```
93+
94+
### Compile-time verification
95+
96+
```cpp
97+
#include "dyadic_verify.h" // triggers all static_asserts at compile time
98+
// If it compiles, all 20+ proofs passed.
99+
```
100+
101+
Day-to-day compiles include a sampled subset. For the full exhaustive suite (256² cases, 8K+ multiplication cases), define `DYADIC_HEAVY_PROOFS`.
102+
103+
### Precision window checkers
104+
105+
```cpp
106+
Polynomial<6, uint8_t> p{{0, 0, 0, 0, 0, 255}};
107+
if (!check_taylor_roundtrip_precision(p))
108+
// T₅ = 5! · 255 = 30600 > 256 — high bits lost
109+
110+
WittVector<4, uint32_t> w{{1, 2, 3, 4}};
111+
if (!check_witt_recovery_precision(w))
112+
// Some rⱼ ≥ 2³²⁻ʲ — ghost recovery inexact
113+
```
114+
115+
## Build & Integrate
116+
117+
**As a single header** — copy `dyadic.h` into your project and `#include "dyadic.h"`.
118+
119+
**With CMake**:
120+
```bash
121+
cmake -B build -DDYADIC_BUILD_TESTS=ON
122+
cmake --build build
123+
ctest --test-dir build
124+
```
125+
126+
Optional: `-DDYADIC_HEAVY_PROOFS=ON` for exhaustive compile-time proofs.
127+
128+
**Via CI script**:
129+
```bash
130+
./ci_compile_check.sh
131+
```
132+
133+
## Tests
134+
135+
| File | What |
136+
|------|------|
137+
| `test_verify.cpp` | 20+ compile-time proofs + runtime verification across 9 (N,W) combos |
138+
| `test_property.cpp` | Randomized property-based tests: 7 invariants × 10 (N,W) combos |
139+
| `test_full.cpp` | 16 functional test groups covering the entire API surface |
140+
| `benchmark.cpp` | Runtime benchmarks for key operations (build manually: `g++ -O2 -std=c++20 -I.. benchmark.cpp`) |
141+
142+
All tests pass under GCC 14 and Clang 21 with ASan+UBSan. CI covers GCC (light + heavy proofs), Clang, and MSVC on Windows.
143+
144+
## Known Limitations
145+
146+
- **Taylor basis roundtrip**: `T_k = k! · FF_k` wraps when `FF_k ≥ 2^W / k!`. Use small coefficients for exact roundtrips. FallingFactorial basis has no such limitation.
147+
- **Witt precision window**: Recovery `r_j = (G_j − S_j) / 2^j` requires `r_j < 2^{W−j}`.
148+
- **`detail::uint128_t`** is a software 128-bit pair — no `unsigned __int128` required. `__int128` is used only as an optimization in `binom()`, guarded by feature-test macros.
149+
150+
## License
151+
152+
This project is made available under the terms of the MIT License.

0 commit comments

Comments
 (0)