ubt 0.4.2

Unified Binary Tree implementation based on EIP-7864
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158

# UBT Integration Testing: Rust vs OCaml

This document describes the integration testing approach for comparing the Rust implementation against the OCaml extracted code from Rocq/Coq.

## Overview

The integration tests validate that structural tree operations (get, insert, delete) produce identical results in both implementations. Hash functions are explicitly excluded since:
- Rust uses Blake3
- OCaml extraction uses placeholder stubs

## Test Data Format

Test cases are defined in a simple text format:

```
# Comments start with #

TEST <test_name>
OP INSERT [stem_bytes] <subindex> [value_bytes]
OP DELETE [stem_bytes] <subindex>
QUERY [stem_bytes] <subindex>
EXPECT <None|Some([bytes])>
```

### Example

```
TEST single_insert_get
OP INSERT [1,2,3,4,5] 10 [42,43,44,45]
QUERY [1,2,3,4,5] 10
EXPECT Some([42,43,44,45,0,0,...])
```

## Results Format

Both Rust and OCaml output results in the same format:

```
# UBT <Language> Test Results

TEST <test_name>
RESULT stem=[bytes],subidx=<n> = <None|Some([bytes])>
```

## Running Tests

### Prerequisites

1. Rust toolchain
2. OCaml with `ocamlfind` and `str` library
3. Extracted OCaml code (`formal/extraction/extracted.ml`)

### Quick Run

```bash
./scripts/integration-test.sh
```

### Manual Steps

```bash
# 1. Export test data from Rust
UBT_TEST_DATA_PATH=target/test_data.txt \
UBT_RESULTS_PATH=target/rust_results.txt \
cargo test --test integration_export test_export_integration_data

# 2. Build OCaml runner
cd formal/extraction
ocamlfind ocamlopt -package str -linkpkg extracted.ml integration_runner.ml -o integration_runner

# 3. Run OCaml tests
./integration_runner < ../../target/test_data.txt > ../../target/ocaml_results.txt

# 4. Compare
diff target/rust_results.txt target/ocaml_results.txt
```

## Test Cases

| Test Name | Description |
|-----------|-------------|
| `empty_tree_get` | Get from empty tree returns None |
| `single_insert_get` | Insert then get same key |
| `get_different_stem` | Get non-existent stem returns None |
| `same_stem_different_subindex` | Different subindex returns None |
| `multiple_inserts_same_stem` | Multiple values in same subtree |
| `delete_removes_value` | Delete makes get return None |
| `insert_preserves_others` | Insert doesn't affect other keys |
| `overwrite_value` | Second insert overwrites first |
| `delete_nonexistent` | Delete non-existent doesn't affect others |
| `large_values` | Full 32-byte keys and values |

## Adding New Tests

1. Add test case to `tests/integration_export.rs` in `generate_test_cases()`
2. Run `./scripts/integration-test.sh` to verify

## CI Integration

Add to GitHub Actions workflow:

```yaml
integration-test:
  runs-on: ubuntu-latest
  steps:
    - uses: actions/checkout@v4
    - uses: dtolnay/rust-toolchain@stable
      with:
        toolchain: 1.85.0
    - uses: ocaml/setup-ocaml@v3
      with:
        ocaml-compiler: 5.1
    - run: opam install str
    - run: cd formal && make extract
    - run: ./scripts/integration-test.sh
```

## Limitations

1. **Hash Functions**: Not compared (different implementations)
2. **Root Hash**: Not compared (depends on hash function)
3. **Merkle Proofs**: Not compared (depends on hash function)
4. **Performance**: Not measured (focus is correctness)

## Architecture

```
                    +-------------------+
                    |  Test Generator   |
                    |  (Rust)           |
                    +--------+----------+
                             |
                             v
                    +-------------------+
                    |  test_data.txt    |
                    +--------+----------+
                             |
            +----------------+----------------+
            |                                 |
            v                                 v
    +---------------+                 +---------------+
    | Rust Runner   |                 | OCaml Runner  |
    | (tree.rs)     |                 | (Extracted)   |
    +-------+-------+                 +-------+-------+
            |                                 |
            v                                 v
    +---------------+                 +---------------+
    | rust_results  |                 | ocaml_results |
    +-------+-------+                 +-------+-------+
            |                                 |
            +----------------+----------------+
                             |
                             v
                    +-------------------+
                    |  Comparison       |
                    |  (diff)           |
                    +-------------------+
```