Status: current companion/correction to Part One after repository refresh
Date: 29 August 2026
Purpose: reconcile the exploratory architecture with commit 73209342c232, and clarify the intended role of Lean 4/F* in the implementation.
A subsequent audit first reported that several Lean modules cited in Part One
were absent. That conclusion came from a stale local checkout and is withdrawn.
After fast-forwarding the repository to 73209342c232, Codex confirmed that
the current Lean tree includes:
SPARQL/IndexedEvalRefinement.lean;SPARQL/AlgebraRefinement.lean;These are landed implementation and proof infrastructure. They are not only F* lineage or proposed ports.
The following vocabulary remains useful:
LANDED
present and building in the checkout being developed
LINEAGE
existing implementation/design in F*, another branch,
or earlier Factoidal work that may be ported/reused
PROPOSED
new block-engine design
No proposed component should be presented as landed only because an analogous
component exists elsewhere. The Cottas and SPARQL modules cited above now
belong in LANDED.
The dated repository baseline is
20260829-blockengine-baseline.md.
The following architecture is explicitly not the goal:
Lean
semantics
proofs
│
▼
Rust/C database
actual computation
The Factoidal approach is stronger.
Lean 4, continuing the earlier F* approach, should be an authoritative executable implementation language for assurance-critical data processing.
The intended architecture is closer to:
INPUT
│
▼
executable Lean/F*
parse / validate / normalize
│
▼
executable Lean/F*
RDF / SPARQL
│
▼
executable Lean/F*
physical planning / PushIR
│
▼
executable Lean/F*
RDF block operations
│
┌────────┴────────┐
│ │
▼ ▼
PostgreSQL TiKV
adapter adapter
│ │
└────────┬────────┘
▼
RESULT
│
▼
evidence / lineage /
attestation
Proofs are one consequence of choosing Lean.
Other consequences are equally important:
This is the larger Factoidal value proposition.
Codex found a useful complication: the current Lean tree contains partial defs, including Storage/DeltaLog.replay, and the older repository guidance understated their number.
So we should not use:
Lean = verified
as a category.
Instead distinguish at least:
A. Total Lean definition
executable, accepted by Lean's termination/productivity checks
B. Total Lean definition + proved contract
e.g. scanFast x = scanSpec x
C. Lean partial def
executable but with a weaker termination/trust story
D. Lean definition with assumptions / axioms / foreign primitives
assurance explicitly conditional on those boundaries
E. Separately implemented optimized code
related by proof, differential testing, or merely an interface contract
These distinctions should eventually be visible in Factoidal evidence records.
A physical operator might therefore report:
implementation:
language: lean4
definition: Storage.Block.scan
totality: total
refinement: blockScan_eq_semanticScan
while another says:
implementation:
language: native
semanticReference: Storage.Block.intersect
evidence: differential
This prevents “written in Lean” from becoming a misleading green badge.
Codex verified the native C and current WebAssembly paths.
It also directly tested the installed Lean toolchain's LLVM backend and found that it was built without -DLLVM=ON; invoking lean -b hit Lean's explicit assertion requiring an LLVM-enabled build.
Therefore Part One's language should be corrected from:
Lean → C / LLVM / WASM
to:
CURRENT:
Lean → generated/native C path
Lean → WASM path
PLANNED/OPTIONAL:
Lean → LLVM backend
LLVM should not be an initial project dependency.
It is an optimization/toolchain experiment.
A useful principle follows:
The block-engine architecture must not depend on LLVM being available.
If LLVM later produces materially better vector code or easier SIMD integration, enable and benchmark it.
Part One proposed a common Rust/C rdf-block-kernel.
That prematurely placed the computational center outside Lean.
The revised preference is:
Lean source
│
executable algorithms
│
proved contracts
│
▼
Lean-generated native core
│
narrow stable ABI
╱ ╲
╱ ╲
PostgreSQL shim TiKV shim
The backend adapters may necessarily contain C, Rust or backend-native glue.
Their job should initially be small:
receive bytes
pin/copy buffers where necessary
call Lean-generated core
translate return/error representation
interact with backend APIs
They should not independently reimplement:
block decoding
block pruning
revision visibility
PushIR semantics
sorted intersection
SPARQL expression fragments
unless benchmarks force that decision.
This makes the default executable implementation the formal implementation.
Only measured hot spots should be candidates for separately implemented native kernels.
There will probably be operations for which platform-specific code wins significantly:
SIMD uint64 intersection
bit unpacking
Roaring primitives
CRC/hashing
memory mapping
zero-copy backend buffers
But the architecture should approach these incrementally.
For example:
Lean:
intersectSpec
Lean:
intersectScalar
theorem:
intersectScalar = intersectSpec
later:
native:
intersectAVX2
The final step introduces an explicit new assurance obligation.
Possible evidence strengths include:
machine-checked refinement
strongest
compiled from the same Lean definition
strong, subject to compiler/toolchain trust
differentially tested against Lean
useful but weaker
reproducibly benchmarked/tested
weaker
external implementation only
explicit trust boundary
The optimized implementation should never silently inherit proofs about a different function.
The common-framework idea still stands.
It should not be described as:
PostgreSQL → small/local
TiKV → real/clustered
PostgreSQL can itself be deployed in substantial HA configurations.
The important distinction is narrower.
TiKV natively supplies a distributed transactional keyspace whose ranges are automatically partitioned across a cluster.
Stock PostgreSQL does not provide that same abstraction across arbitrary PostgreSQL nodes.
So:
BlockBackend
│
┌────────┴────────┐
│ │
PostgreSQL TiKV
│ │
single / HA / distributed
replicated KV cluster
Later we might add:
PostgresShardBackend
but this should not be faked in version 1.
The planner should depend on capabilities such as:
snapshotReads
atomicMultiKeyWrite
orderedRangeAccess
remotePushExecution
automaticPartitioning
rather than on assumptions encoded in backend names.
The new system should avoid having:
Postgres physical RDF model
and:
TiKV physical RDF model
where possible.
Instead define a canonical RDF block model:
Block
BlockMetadata
Manifest
Delta
RevisionVisibility
and provide two persistence realizations.
For example:
Logical RDF dataset D
│
┌──────────────┴──────────────┐
│ │
Manifest Mpg Manifest Mkv
│ │
PostgreSQL TiKV
Mpg and Mkv might differ in block boundaries or physical placement while still satisfying:
denotes(Mpg) = D
denotes(Mkv) = D
This is important for both portability and assurance.
The backend is not the identity of the data.
Codex should not have to choose between:
QLever-like uint blocks
and:
compiled SPARQL mini-language
We want both.
They operate at different levels.
Blocks answer:
How do we represent and scan large RDF relations efficiently?
Characteristics:
global integer term IDs
multiple sorted permutations
prefix elision
column/vector representation
compressed integer streams
min/max metadata
block statistics
selective decode
lazy block access
PushIR answers:
Once a block is located, what bounded computation can execute beside it?
Examples:
filter ID
check revision visibility
select columns
count
intersect sorted IDs
semi-join
aggregate locally
Conceptually:
SPARQL
│
▼
Physical Plan
│
├──────── coordinator operators
│
└──────── PushIR fragment
│
▼
RDF blocks
Neither replaces the other.
PushIR is especially suitable for the Factoidal methodology because it can be tiny.
Version 0 might contain only:
ScanRange
LoadColumn
EqId
LtId
And
Or
Not
VisibleAt
Select
Project
Count
Min
Max
Emit
Its syntax, validator and evaluator can all be Lean definitions.
Then:
compilePush : PhysicalFragment → Option PushProgram
is also executable Lean.
The key theorem family is:
compilePush f = some p
→
evalPush p data
=
evalFragment f data
where equality is stated using the appropriate RDF/SPARQL bag/order semantics.
An expression or physical fragment that cannot be compiled simply remains above the pushdown boundary.
Thus:
compiler returns none
means:
execute normally
not:
query unsupported
That is a useful safe-fallback rule.
RonDB's interpreted-code machinery was the inspiration, not the required shape.
A particularly attractive alternative for Factoidal is for PushIR to be an algebra of block primitives.
For example:
Scan GPOS g=17 p=42
VisibleAt 103
Eq O 9001
Project S
Count
might compile directly into calls among a small fixed family of Lean functions.
A serialized program is still useful for:
But we do not need to invent registers, stacks or general-purpose bytecode unless that becomes useful.
The first vertical should not begin with clever bitpacking.
Something like:
structure Block where
permutation : Permutation
prefix : ...
rows : Array PhysicalRow
or a simple columnar equivalent is enough to establish semantics.
Then prove things such as:
blockRows (encode rows) = rows
scanBlock pattern block
=
semanticFilter pattern (blockRows block)
Only after the semantic boundary works should we introduce:
delta encoding
frame-of-reference
bit packing
RLE
Roaring
adaptive codecs
Each codec should preserve a common block denotation.
That turns compression into another data transformation with an explicit correctness contract.
Codex suggested the first implementation unit as:
TermId
tagged GraphId
one immutable block
one permutation
one scan
one refinement theorem
That is a good starting vertical.
I would add one requirement:
the scan theorem should connect all the way to an existing RDF/SPARQL semantic notion, rather than merely proving two new block-engine functions agree.
So the first useful vertical is:
RDF terms
│
▼
TermId encoding
│
▼
one sorted block
│
▼
physical bounded scan
│
▼
decode result
│
▼
existing semantic triple-pattern result
with a theorem connecting the endpoints.
That gives the project its characteristic shape immediately.
Cottas-style separate dictionaries are useful for columnar artifacts, but a general SPARQL engine benefits from IDs that survive movement across positions.
For:
?s :parent ?o .
?o :name ?name .
the first pattern's object immediately becomes the second pattern's subject join value.
So the default model should be:
TermId : RDFTerm → 64-bit physical ID
with exact RDF-term identity represented consistently wherever the term can legally occur.
Graph scope can be separate:
GraphId =
DefaultGraph
| NamedGraph TermId
or an equivalent tagged representation.
This should remain a semantic design question until proved adequate; do not prematurely burn tag bits into the public identity contract.
The existing SPARQL formalization has already exposed cases where an implementation equality relation is not literally structural RDF-term equality.
The contract must also name its RDF version. The RDF 1.2 Concepts definition of literal term equality treats language tags case-insensitively and keeps lexical forms exact. This differs from RDF 1.1 for tag case. The current Lean relations split in a different place:
Literal.eqb folds language-tag case, as RDF 1.2 requires, and also
canonicalizes rdf:XMLLiteral lexical forms, which is too coarse for RDF 1.2
term identity;Literal.termEq compares all stored fields, which keeps XML lexical forms
exact but treats tag case as significant.Thus neither relation should be adopted as the public RDF 1.2 dictionary contract without a small repair. Define and prove one version-explicit term identity relation before allocating stable IDs.
Therefore the physical dictionary should have a simple contract:
same TermId
⇔
same RDF term
for whatever precise RDF-term equality Factoidal chooses.
Other notions should be separately derived:
JoinKey
ValueKey
NumericValue
CollationKey
if particular SPARQL operations require them.
Do not make physical identity depend on an optimization-oriented equality predicate.
Substantially more than storage code.
The existing SPARQL tree should remain the semantic root.
Useful existing categories include:
RDF term model
query/pattern AST
expression AST
solution mappings
expression evaluation
BGP semantics
join/filter/union/minus/etc.
query evaluation machinery
test infrastructure
W3C conformance fixtures
The new project should add a physical-evaluation vertical beneath those semantics rather than create a second SPARQL implementation.
The refreshed tree gives a more specific reuse path:
existing Lean SPARQL semantics
│
├── AlgebraRefinement
├── IndexedEvalRefinement
│
▼
existing Lean Cottas physical reasoning
│
├── on-disk planning
├── selective scans
├── reader/writer machinery
└── access-path and pruning logic
│
▼
new generalized Block layer
│
├── PostgreSQL persistence
└── TiKV persistence
This makes the first work a generalization and refactoring of landed Lean physical techniques. It is not a new port from F*.
Conceptually:
SPARQL semantic evaluator
▲
│ refinement
│
physical block evaluator
IndexedEvalRefinement already proves exact list equality for the indexed BGP
evaluator and hash join. Use its proof shape as the first block-scan standard.
The Lean Cottas work is the primary physical starting point. It already contains the reader/writer, on-disk planner, selective scans, access-path selection, pruning, limits, counts, dictionaries, and offset-index machinery.
The older F* Cottas work remains useful as lineage, differential input, and a source for behavior that has not yet moved. It contains physical-algorithm reasoning such as:
candidate-group pruning
dictionary-based exclusion
offset jumps
selective column decode
exact-count shortcuts
safe fallback
ordered intersection
The refactoring direction is now:
landed Lean Cottas algorithm and theorem
│
▼
general Lean Block algorithm and theorem
│
├── Cottas realization
│
├── PostgreSQL block realization
│
└── TiKV block realization
The current Cottas store uses separate subject, predicate, object, and graph ID domains. It also has Cottas-specific row-group and file contracts. The common Block layer still needs one version-explicit term identity contract, one block denotation, and backend-neutral laws. Generalize the proved mechanisms without making the current Cottas representation the public storage contract.
The refreshed tree has five total Lean HDT modules: container, container theorems, dictionary, triples, and store. The store reads a static HDT object and performs pure searches after the I/O boundary. Use it for:
binary encoding patterns
succinct representations
byte-level proof experience
test infrastructure
HDT remains particularly useful as prior art for:
compact dictionary IDs
compressed adjacency-style relations
static RDF packaging
while the new engine has stronger requirements around:
named graphs
transactions
updates
revisions
distributed storage
A reasonable progression is:
Phase PG0
Lean block engine runs in ordinary process
PostgreSQL stores manifests and block bytes
Phase PG1
small PostgreSQL extension calls Lean-generated native library
Phase PG2
custom PostgreSQL scan/executor integration
Phase PG3
only if justified:
deeper access-method/planner integration
Do not make PostgreSQL planner integration a prerequisite for proving the RDF physical model.
Early PostgreSQL is valuable precisely because it gives us mature:
transactions
WAL
snapshots
recovery
replication
operations tooling
without requiring us to solve distributed systems first.
Likewise:
Phase KV0
TiKV stores canonical blocks
coordinator retrieves and executes them
Phase KV1
send bounded PushIR fragments toward data
Phase KV2
execute Lean-generated block core from a thin TiKV-side adapter
Phase KV3
specialized region-aware joins/aggregates
Whether the final integration is:
TiKV plugin
maintained TiKV fork
sidecar colocated with TiKV
FFI into Lean-generated native library
is an implementation question.
The semantic contract must not depend on that choice.
For one query execution the eventual evidence chain might be:
source bytes
│
▼
RDF parse
│
▼
canonical logical dataset D
│
▼
term dictionary
│
▼
block manifest M
│
▼
snapshot/revision V
│
▼
SPARQL query Q
│
▼
logical plan L
│
▼
physical plan P
│
▼
PushIR fragments X1...Xn
│
▼
block executions
│
▼
result R
Possible checked statements include:
parse(source) = D
manifestDenotes(M, D)
physicalPlanDenotes(P) = logicalPlanDenotes(L)
compilePush(F) = X
→ evalPush(X) = evalPhysicalFragment(F)
resultOf(P, M, V) = R
And the execution record can bind those semantic facts to:
source hashes
Lean source/build identity
compiler/toolchain identity
backend snapshot
program hashes
block hashes
result hash
This is where the block engine connects to Factoidal's broader provenance/attestation work.
Even if an algorithm is written and proved in Lean, executing compiled machine code introduces a toolchain boundary.
So a mature assurance statement should distinguish:
kernel-checked theorem about source definition
from:
claim that this executable implements that source definition
The latter relies initially on the Lean compiler, C compiler/linker, runtime and build process.
Possible future strengthening includes:
reproducible builds
signed source→binary provenance
NPM/GitHub build provenance
trusted-cloud build attestation
multiple backend compilations
cross-checking WASM/native results
This is not a defect in the Lean strategy.
It is precisely the kind of boundary Factoidal should make visible rather than pretending does not exist.
Every substantial physical transformation can become a Factoidal operation:
dictionary build
block build
re-encode
compact
apply delta
publish manifest
execute query
For example:
DatasetSnapshot D17
│
│ build-block-index
▼
BlockManifest M31
│
│ apply Delta Δ4
▼
BlockManifest M32
│
│ compact
▼
BlockManifest M33
The same DAG has:
computation view
provenance view
assurance view
rather than requiring a separate database audit-log ontology.
This follows the broader Factoidal direction in which operations record immutable inputs/outputs, semantics and evidence rather than merely logging that some program ran.
Suppose:
base B
delta Δ
becomes:
new base B'
Then the relevant claim is not simply:
compaction completed
but:
denote(B, Δ, revision r)
=
denote(B', revision r)
for the appropriate revision domain.
Likewise:
CodecA block
↓ re-encode
CodecB block
should preserve block denotation.
This makes ordinary database maintenance part of the same formally described data-processing chain.
That is exactly where a Lean/F* approach has more to offer than “the query planner has been proved correct”.
One of the strongest ideas from the existing Factoidal storage work should become a central rule:
optimization cannot establish safety
↓
use slower path
not:
optimization cannot establish safety
↓
guess
Examples:
unknown block summary
→ read block
PushIR compilation failure
→ coordinator execution
unknown cardinality
→ conservative plan
missing native optimization
→ Lean scalar implementation
unusable offset/index metadata
→ full scan
This gives an attractive operational property:
Disabling optimization should reduce performance, not correctness or semantic coverage.
The precise tree can evolve, but conceptually:
L4Factoidal/
RDF/
... existing semantic model ...
SPARQL/
... existing semantics ...
Physical/
Model.lean
Plan.lean
Eval.lean
Lower.lean
Refinement.lean
PushIR/
Syntax.lean
Validate.lean
Eval.lean
Compile.lean
Refinement.lean
Storage/
TermId.lean
Block/
Model.lean
Denotation.lean
Scan.lean
Prune.lean
Join.lean
CodecSimple.lean
Manifest.lean
Delta.lean
Compact.lean
Backend/
Contract.lean
Capabilities.lean
Backend-specific integration code should sit outside the semantic core where practical.
The first coding milestone should be small enough to land quickly but meaningful enough to establish the architecture.
Select RDF 1.2 term identity explicitly. Repair the language-tag and
rdf:XMLLiteral split described in section 15. Prove the decision procedure
sound and complete for the chosen relation.
Define logical/physical ID relation.
Do not optimize tagging prematurely.
Represent default versus named graph unambiguously.
Refactor one landed Cottas access shape into a backend-neutral block. Use one simple permutation, probably one where a bound predicate produces a useful sorted relation.
No compression required initially.
Define what logical quads the block represents.
For example:
fixed predicate
optional subject/object bounds
Prove the scan returns exactly the result required by the existing RDF/SPARQL triple-pattern semantics for the supported fragment.
Compile that implementation through the existing Lean native/C path.
Persist/read that identical block as opaque bytes plus metadata.
semantic evaluator result
=
in-memory block result
=
PostgreSQL-persisted block result
This is already a small but real end-to-end assurance story.
After the first vertical works:
simple block
↓
compressed block
and prove:
decode (encode b) = b
or an appropriately abstract equivalent.
Benchmark several codecs.
Do not assume QLever's exact choices are optimal for:
mutable quads
revision metadata
PostgreSQL
TiKV
The transferable QLever insight is primarily:
exploit sorted RDF integer structure aggressively.
The precise codec remains empirical.
Once block semantics are stable:
PushIR v0:
bound ID comparisons
revision visibility
projection
COUNT
Compile only the corresponding SPARQL/physical fragments.
Run it first with the Lean evaluator.
Then invoke the same generated implementation through PostgreSQL.
Then through TiKV.
This gives a much cleaner progression than simultaneously designing:
compression
distributed execution
complex joins
VM
optimizer
before anything is vertically connected.
Only after the common semantic/block/backend boundary is established should the project become aggressive:
QLever-style compressed blocks
block-overlap pruning
vectorized merge joins
late materialization
SIMD intersection
galloping search
specialized RDF statistics
star-pattern indexes
materialized graph patterns
worst-case-optimal joins
region-aware distributed execution
continuous delta compaction
revision-native queries
At that stage PostgreSQL and TiKV can tell us different things.
PostgreSQL gives a strong single-system baseline and exceptional operational maturity.
TiKV gives the opportunity to investigate truly distributed RDF execution.
It would be easy to overclaim.
A result should not simply carry:
verified: true
Instead report something like:
semantic:
Lean theorem-backed
block representation:
Lean theorem-backed
physical planner:
Lean executable
selected refinements proved: [...]
PushIR:
Lean compiler + evaluator
refinement theorem: [...]
storage:
PostgreSQL transactional snapshot
external-system assumption
native executable:
compiled from Lean source
build provenance: ...
result:
sha256:...
If later an AVX routine is substituted:
SIMD intersection:
external native optimization
differential test suite: ...
The assurance frontier remains visible.
The refreshed repository is the starting point. On commit 73209342c232,
Codex reports that the full Lean build passed all 719 jobs under Lean 4.33.1.
Native C and WASM paths exist. LLVM support is absent from the installed
toolchain.
It also created:
docs/20260829-blockengine-baseline.md
skills/blockengine/SKILL.md
as the local durable handoff and working method.
Those should now be treated as the coding agent's repository-local source of truth about current implementation state.
The exploratory architecture documents remain design input, not a substitute for checking the tree.
The project should carry these rules explicitly.
Lean/F* is not merely where proofs live.
It is where assurance-critical algorithms should be implemented when practical.
Optimized paths refine simpler executable paths.
Failure to justify an optimization falls back to a slower semantically complete path.
PostgreSQL and TiKV persist representations of RDF state; neither defines RDF or SPARQL semantics.
Blocks, manifests, dictionaries, deltas and compaction all have explicit denotations.
PushIR is a small, typed, bounded execution language compiled from physical SPARQL fragments.
Total Lean, partial Lean, proved refinements, compiled code, external adapters and attestations are not conflated.
The same logical dataset/query executed through PostgreSQL and TiKV should be capable of producing the same logical result identity despite different physical execution.
Do not begin with TiKV.
Do not begin with PostgreSQL.
Do not begin with a bytecode VM.
Begin by generalizing one landed Lean Cottas access shape:
RDF 1.2 term identity contract
TermId
GraphId
Block
Block.denotes
one permutation
one scan
one theorem relating that scan to existing RDF/SPARQL semantics
Make it executable.
Benchmark it enough to ensure the representation is not pathological.
Then persist that exact object in PostgreSQL without changing its semantics.
That establishes the vertical seam everything else depends on:
SPARQL semantics
↓
physical RDF representation
↓
executable Lean algorithm
↓
database persistence
↓
same logical result
Once that is real, both the QLever-inspired performance work and the TiKV distributed work have somewhere sound to attach.
The eventual system should be describable as:
FACTOIDAL
│
RDF / SPARQL semantics
│
executable Lean
│
physical compiler
│
┌───────────┴───────────┐
│ │
coordinator plan PushIR
│ │
└───────────┬───────────┘
│
Lean block engine
│
compressed blocks
╱ ╲
╱ ╲
PostgreSQL TiKV
│ │
transaction / distributed
durability transaction /
replication
╲ ╱
╲ ╱
execution
│
▼
RESULT
│
▼
Factoidal evidence DAG
The distinctive proposition is not simply:
“an RDF engine written in Lean.”
Nor is it:
“a verified SPARQL implementation on a fast database.”
It is:
an RDF/SPARQL data-processing system in which logical semantics, executable algorithms, physical representation, query compilation, persistence transformations, optimized execution and provenance can be connected through an explicit chain of machine-checkable contracts and evidence.
PostgreSQL and TiKV give us powerful storage machinery.
QLever gives us important evidence about how far specialized RDF physical structures can be pushed.
Lean/F* gives us the opportunity to make the route from source data to result unusually inspectable and unusually defensible.
That should remain the organizing principle of the project.