TK-HvAc / docs /Runtime_Implementation.md

Implement TK-HvAc C++/Vulkan resolver and literal HVAC coupling

3bebe93 verified 3 days ago

13.1 kB

# Native implementation, version 0.2.0

Tom Klootwijk | NL200678942 | 10-07-1990

TK-HvAc now has a compiled C++20 host and an executed integer Vulkan compute resolver. It constructs a finite packet from supplied answers, stores overlapping novelty bits, and returns those answers through bounded header traversal and versioned page residency. It performs no candidate search during resolution.

The demonstrated coverage includes 128 synthetic jobs and three independently verified ETC mainnet jobs. The latter use the already-published proofs for blocks 11,700,000–11,700,002. Importing these known answers demonstrates a real finite coverage packet. An exact signed-threshold relation additionally covers changed targets for the same rule/epoch/seal. It does not construct answers for unseen seal hashes or prove a universal Etchash transport action.

## Implemented path

```text
offline supplied answers
  -> optional independent Etchash light verification
  -> complete rule/epoch/seal/target key
  -> C++ novelty overlap constructor and CRC-protected page files
  -> stable ECS key/page/version/header binding
  -> disk read into bounded LRU resident slot
  -> host-visible coherent Vulkan staging allocation
  -> software log-polar chart permutation and Morton texel placement
  -> device-local optimal-tiled R32_UINT image
  -> integer texelFetch, cross-word extraction, reference XOR and next-header hop
  -> nonce/mix result, with a fence before resource reuse
```

The concrete ECS is a set of C++ typed binding tables. It keeps stable job identity, page identity/version, bit view, header links and replaceable physical slot/generation separate. It implements the coupling needed by this resolver; it is not a general ECS framework.

The image-fetch semantics follow [Khronos Vulkan texture operations](https://docs.vulkan.org/spec/latest/chapters/textures.html). Image transitions, shader/host barriers and completion fences follow the access-dependency model described by [Khronos synchronization examples](https://docs.vulkan.org/guide/latest/synchronization_examples.html). Native image tiling is driver-controlled. No measurement here establishes physical texture-cache residency or cache saturation.

## Finite transport ABI

Every transport integer is unsigned LE32, except raw key bytes and the explicitly documented LE64 epoch/nonce. CRC32 is the standard reflected polynomial `0b11101101101110001000001100100000`, with all-ones initial state and final complement. It detects corruption; it is not an authentication signature.

| Object | Actual layout |
| --- | --- |
| Full job key | rule identity, 32 bytes; epoch LE64, 8 bytes; seal hash, 32 bytes; target BE256, 32 bytes |
| Answer | nonce LE64 followed by the 32 mix-digest bytes; 10 LE32 words total |
| Header | identity, page, version, view, bit offset, bit count, next header, interpretation tag; 32 bytes |
| Index | `TKHI` magic, schema `0b10`, page count, job count, domain-label byte length, ASCII domain, sorted `(key,page,version,entry,minimum_target_BE256,relation_tag)` records, CRC32 |
| Page | `TKHP` magic, schema, ID, version, XOR reference, logical bit count, word count, header count, headers, packed words, CRC32 |
| Query | entry header, expected resident generation, expected page version, reserved; 16 bytes |
| GPU result | status, hop count, output-word count, reserved, 10 answer words, 2 padding words; 64 bytes |

The domains are `fixture-integer-v1` and `etchash-import-v1`. A domain label is provenance metadata, not proof that an arbitrary hand-authored input is valid. The supplied Etchash import tool independently verifies every input proof before writing the answer list. Untrusted answers must undergo equivalent verification.

Byte lengths and array counts are checked before decoding. Page bits are low-bit-first within LE32 words, with zero padding. The overlap constructor reuses the longest equal suffix/prefix of the residual words; it stores the remaining novelty bits. The shared XOR reference is a declared finite parameter, not a general compression theorem.

For three imported proofs, 960 answer bits become 906 shared payload bits. The complete packet contains **1,188 page bytes plus 497 index bytes**, before the separate provenance/reference documents. Metadata is included in these figures. This sample does not achieve a whole-packet half-size reduction.

Logical source addresses and arithmetic constants are authored in binary. Decimal byte/count metrics are human-readable measurements. GLSL's literal grammar requires the build tool to lower binary authoring tokens to accepted integer literals. The selected SPIR-V shader contains no floating-point type.

## Cryptex chart and integer phase

[integer_profile.json](../runtime/integer_profile.json) supplies finite Q16.16 codes for `kappa=phi^pi` and `eta=phi^ln(pi^-1)`. The [generator](../tools/generate_integer_profile.py) checks selected codes at two Decimal precisions and emits binary C++ constants. It uses a documented finite pi approximation at build time.

For a page's logical word index `i`, the chosen chart is:

```text
theta = i & 0b11111
q     = i >> 0b101
a     = (chart_stride*i + chart_offset) & 0b1111111111
texel = MortonDecode(a)
```

`chart_stride` is odd and derived from the kappa code; `chart_offset` is derived from the eta code. This is an explicit finite bijective address profile, selected by this implementation. It does not assert a unique byte-layout theorem from irrational constants. The host and shader use the same generated parameters. It is a discrete angular/radial address chart; it is not an evaluated continuous logarithm of every query vector.

The C++ phase adapter separately maps signed integer planar vectors to unsigned 32-bit full-turn CORDIC codes using shift/add operations and generated integer angle constants. It retains 30 guard bits internally, handles all quadrants and tags the zero vector undefined. Its declared phase-error budget is 128 ticks per full turn. Independent 80-digit Decimal tests over 5,234 vectors observed at most 6 ticks of error. This is finite test evidence, not a universal correct-rounding certificate. The adapter does not claim to recover arbitrary eigenvectors from a hash.

The Q16.16 geometry adapter supplies integer-root enclosures for sphere and box distances, and interval min/max CSG membership bounds. It does not yet serialize arbitrary CSG/differential programs or implement the complete Klein/kinematic raymarcher.

## Residency and synchronization

The C++ LRU pager owns a bounded number of slots. Every replacement increments the slot generation. Queries carry their expected generation and page version; stale inputs are rejected before a texture read. Headers use page-local dense indices with checked bit windows and a finite traversal bound. A cycle cannot produce a successful unbounded traversal.

Each image upload transitions to transfer-destination, copies the staged words, then transitions to shader-read-only. A fence completes the upload before the slot is published for dispatch. A dispatch writes its output buffer, applies a shader-write-to-host-read dependency and completes a fence before host reads or reuse. The baseline intentionally uses one synchronous queue. Asynchronous disk prefetch, copy/compute overlap, nonuniform descriptor indexing and large-budget VRAM saturation remain future engineering work. This baseline has no OS-specific pinned-ring guarantee.

`OutsideCoverage` is distinct from a residency miss. A key outside the stored identity and target-range coverage produces no answer. A resident-page miss loads the already-constructed page and resumes decoding. No header or decoder invokes a hidden nonce-search loop.

## Build and run

Dependencies: a C++20 compiler, Vulkan headers, glslang, Python 3, and a Vulkan 1.1 device supporting sampled `R32_UINT` images. The tested Windows build uses LLVM-MinGW 20261104, glslang 16.6.0 and Vulkan-Headers 1.4.321. Build tools are external dependencies; they are not copied into this model repository. See [build provenance](../reports/BUILD_PROVENANCE.json).

From the repository root, with local tool paths supplied explicitly:

```powershell
python tools/build_runtime.py --compiler <clang++> --glslang <glslang> --vulkan-include <include-directory> --build-dir build
python tools/test_runtime.py --executable build/tk-hvac.exe --shader build/resolve.spv --work <new-test-directory>
build/tk-hvac.exe resolve --corpus examples/verified_etc/corpus --queries examples/verified_etc/queries.bits --backend vulkan --shader build/resolve.spv --slots 0b1
```

The placeholders name paths on the executing machine. A CMake build description is also supplied under `runtime/`; the recorded acceptance run used the Python build tool.

To independently regenerate the real-proof import, install PyCryptodome in the selected Python environment and run:

```powershell
python tools/import_etchash_answers.py --blocks sources/ETC_Mainnet_11700000_11700002.json --output <new-import-directory> --cache-dir <verification-cache-directory>
build/tk-hvac.exe build --input <new-import-directory>/answers.bits --domain etchash-import-v1 --output <new-corpus-directory> --jobs-per-page 0b1
```

No network call is made by this importer. It constructs the ETC epoch-195 verification cache and regenerates the dataset items needed to verify the supplied nonces. This cost belongs to import/verification, not runtime lookup. The [independent verifier](../reference/etchash_light.py) first passes the [core-geth Hashimoto test vector](https://github.com/etclabscore/core-geth/blob/master/consensus/ethash/algorithm_test.go), and applies [ECIP-1099](https://ecips.ethereumclassic.org/ECIPs/ecip-1099) for epoch/seed identity. Source block JSON was fetched read-only from Blockscout's Ethereum Classic RPC endpoint; every full header hash, mix digest and target result was recomputed.

## A proved target-interval transport relation

For a fixed rule identity, epoch and seal, import a verified answer `(nonce,mix)` and its exact final result `R=HashimotoResult(nonce)`. The target coordinate has the declared signed field

```text
f_R(T) = R - T
covered(T) iff f_R(T) <= 0
answer(T) = the same verified nonce/mix
```

As a real one-dimensional defining program, `f_R` is the negative-inside signed distance of the half-line `[R,+infinity)`. Admitted target queries are finite unsigned 256-bit integers. The runtime computes its membership by lexicographic comparison of equal-width big-endian bytes, without floating point or an overflowing 256-bit subtraction. The boundary is accepted, matching the consensus target predicate.

This is a concrete reusable relation: the defining parameter `R` and its associated proof are stored once, while target queries select the same answer. The index uses a stable `(rule,epoch,seal)` prefix table and stores the minimum verified threshold for that group. It does not enumerate new nonces or run Hashimoto during lookup. A tag distinguishes this relation from an exact-key-only fixture.

The implication follows directly: `HashimotoResult(nonce)=R` and `R<=T` imply that the same proof satisfies the queried target. For an increase `delta>=0`, target transport `T -> T+delta` within the admitted domain preserves that answer. This is a partial monotone solution relation, not an asserted group action on all Etchash jobs. A changed seal can change the whole hash computation and has no such established transport here.

The acceptance run checks three different verified seals, each at `T=R`, `T=R+1` and the maximum target, plus rejection at `T=R-1`. These nine transported-target queries and the original-job lookups produce identical CPU/GPU answers through page replacement.

## Evidence and remaining scope

[RUNTIME_VALIDATION.json](../reports/RUNTIME_VALIDATION.json) records the native checks, actual GPU, repeated covered queries and eviction counts. [The import receipt](../examples/verified_etc/verification.json) records the three exact jobs and independently recomputed proofs. The synthetic packet tests exercise non-word-aligned views, cross-word reads, malformed input, CRC rejection, cycle termination, relocation, fresh-process replay and stale generations.

The real-proof test repeatedly resolves three distinct covered keys through a single resident slot and compares CPU/GPU output bytes. Changing rule, epoch or seal returns `OutsideCoverage`. A target below the verified proof result also returns `OutsideCoverage`; target equality and larger targets resolve through the exact threshold relation below. A geometric resemblance alone cannot authorize another changed job.

The principal remaining mathematical requirement is a solution-preserving transport/construction rule for unseen Etchash jobs. The engineering work still includes arbitrary typed field-program serialization, full kinematic calculus and traversal, asynchronous streaming, measured cache/bandwidth behavior, and calibrated physical material/HVAC adapters. No live mining throughput or unseen-job speedup is claimed.

	# Native implementation, version 0.2.0

	Tom Klootwijk \| NL200678942 \| 10-07-1990

	TK-HvAc now has a compiled C++20 host and an executed integer Vulkan compute resolver. It constructs a finite packet from supplied answers, stores overlapping novelty bits, and returns those answers through bounded header traversal and versioned page residency. It performs no candidate search during resolution.

	The demonstrated coverage includes 128 synthetic jobs and three independently verified ETC mainnet jobs. The latter use the already-published proofs for blocks 11,700,000–11,700,002. Importing these known answers demonstrates a real finite coverage packet. An exact signed-threshold relation additionally covers changed targets for the same rule/epoch/seal. It does not construct answers for unseen seal hashes or prove a universal Etchash transport action.

	## Implemented path

	```text
	offline supplied answers
	-> optional independent Etchash light verification
	-> complete rule/epoch/seal/target key
	-> C++ novelty overlap constructor and CRC-protected page files
	-> stable ECS key/page/version/header binding
	-> disk read into bounded LRU resident slot
	-> host-visible coherent Vulkan staging allocation
	-> software log-polar chart permutation and Morton texel placement
	-> device-local optimal-tiled R32_UINT image
	-> integer texelFetch, cross-word extraction, reference XOR and next-header hop
	-> nonce/mix result, with a fence before resource reuse
	```

	The concrete ECS is a set of C++ typed binding tables. It keeps stable job identity, page identity/version, bit view, header links and replaceable physical slot/generation separate. It implements the coupling needed by this resolver; it is not a general ECS framework.

	The image-fetch semantics follow [Khronos Vulkan texture operations](https://docs.vulkan.org/spec/latest/chapters/textures.html). Image transitions, shader/host barriers and completion fences follow the access-dependency model described by [Khronos synchronization examples](https://docs.vulkan.org/guide/latest/synchronization_examples.html). Native image tiling is driver-controlled. No measurement here establishes physical texture-cache residency or cache saturation.

	## Finite transport ABI

	Every transport integer is unsigned LE32, except raw key bytes and the explicitly documented LE64 epoch/nonce. CRC32 is the standard reflected polynomial `0b11101101101110001000001100100000`, with all-ones initial state and final complement. It detects corruption; it is not an authentication signature.

	\| Object \| Actual layout \|
	\| --- \| --- \|
	\| Full job key \| rule identity, 32 bytes; epoch LE64, 8 bytes; seal hash, 32 bytes; target BE256, 32 bytes \|
	\| Answer \| nonce LE64 followed by the 32 mix-digest bytes; 10 LE32 words total \|
	\| Header \| identity, page, version, view, bit offset, bit count, next header, interpretation tag; 32 bytes \|
	\| Index \| `TKHI` magic, schema `0b10`, page count, job count, domain-label byte length, ASCII domain, sorted `(key,page,version,entry,minimum_target_BE256,relation_tag)` records, CRC32 \|
	\| Page \| `TKHP` magic, schema, ID, version, XOR reference, logical bit count, word count, header count, headers, packed words, CRC32 \|
	\| Query \| entry header, expected resident generation, expected page version, reserved; 16 bytes \|
	\| GPU result \| status, hop count, output-word count, reserved, 10 answer words, 2 padding words; 64 bytes \|

	The domains are `fixture-integer-v1` and `etchash-import-v1`. A domain label is provenance metadata, not proof that an arbitrary hand-authored input is valid. The supplied Etchash import tool independently verifies every input proof before writing the answer list. Untrusted answers must undergo equivalent verification.

	Byte lengths and array counts are checked before decoding. Page bits are low-bit-first within LE32 words, with zero padding. The overlap constructor reuses the longest equal suffix/prefix of the residual words; it stores the remaining novelty bits. The shared XOR reference is a declared finite parameter, not a general compression theorem.

	For three imported proofs, 960 answer bits become 906 shared payload bits. The complete packet contains 1,188 page bytes plus 497 index bytes, before the separate provenance/reference documents. Metadata is included in these figures. This sample does not achieve a whole-packet half-size reduction.

	Logical source addresses and arithmetic constants are authored in binary. Decimal byte/count metrics are human-readable measurements. GLSL's literal grammar requires the build tool to lower binary authoring tokens to accepted integer literals. The selected SPIR-V shader contains no floating-point type.

	## Cryptex chart and integer phase

	[integer_profile.json](../runtime/integer_profile.json) supplies finite Q16.16 codes for `kappa=phi^pi` and `eta=phi^ln(pi^-1)`. The [generator](../tools/generate_integer_profile.py) checks selected codes at two Decimal precisions and emits binary C++ constants. It uses a documented finite pi approximation at build time.

	For a page's logical word index `i`, the chosen chart is:

	```text
	theta = i & 0b11111
	q = i >> 0b101
	a = (chart_stride*i + chart_offset) & 0b1111111111
	texel = MortonDecode(a)
	```

	`chart_stride` is odd and derived from the kappa code; `chart_offset` is derived from the eta code. This is an explicit finite bijective address profile, selected by this implementation. It does not assert a unique byte-layout theorem from irrational constants. The host and shader use the same generated parameters. It is a discrete angular/radial address chart; it is not an evaluated continuous logarithm of every query vector.

	The C++ phase adapter separately maps signed integer planar vectors to unsigned 32-bit full-turn CORDIC codes using shift/add operations and generated integer angle constants. It retains 30 guard bits internally, handles all quadrants and tags the zero vector undefined. Its declared phase-error budget is 128 ticks per full turn. Independent 80-digit Decimal tests over 5,234 vectors observed at most 6 ticks of error. This is finite test evidence, not a universal correct-rounding certificate. The adapter does not claim to recover arbitrary eigenvectors from a hash.

	The Q16.16 geometry adapter supplies integer-root enclosures for sphere and box distances, and interval min/max CSG membership bounds. It does not yet serialize arbitrary CSG/differential programs or implement the complete Klein/kinematic raymarcher.

	## Residency and synchronization

	The C++ LRU pager owns a bounded number of slots. Every replacement increments the slot generation. Queries carry their expected generation and page version; stale inputs are rejected before a texture read. Headers use page-local dense indices with checked bit windows and a finite traversal bound. A cycle cannot produce a successful unbounded traversal.

	Each image upload transitions to transfer-destination, copies the staged words, then transitions to shader-read-only. A fence completes the upload before the slot is published for dispatch. A dispatch writes its output buffer, applies a shader-write-to-host-read dependency and completes a fence before host reads or reuse. The baseline intentionally uses one synchronous queue. Asynchronous disk prefetch, copy/compute overlap, nonuniform descriptor indexing and large-budget VRAM saturation remain future engineering work. This baseline has no OS-specific pinned-ring guarantee.

	`OutsideCoverage` is distinct from a residency miss. A key outside the stored identity and target-range coverage produces no answer. A resident-page miss loads the already-constructed page and resumes decoding. No header or decoder invokes a hidden nonce-search loop.

	## Build and run

	Dependencies: a C++20 compiler, Vulkan headers, glslang, Python 3, and a Vulkan 1.1 device supporting sampled `R32_UINT` images. The tested Windows build uses LLVM-MinGW 20261104, glslang 16.6.0 and Vulkan-Headers 1.4.321. Build tools are external dependencies; they are not copied into this model repository. See [build provenance](../reports/BUILD_PROVENANCE.json).

	From the repository root, with local tool paths supplied explicitly:

	```powershell
	python tools/build_runtime.py --compiler <clang++> --glslang <glslang> --vulkan-include <include-directory> --build-dir build
	python tools/test_runtime.py --executable build/tk-hvac.exe --shader build/resolve.spv --work <new-test-directory>
	build/tk-hvac.exe resolve --corpus examples/verified_etc/corpus --queries examples/verified_etc/queries.bits --backend vulkan --shader build/resolve.spv --slots 0b1
	```

	The placeholders name paths on the executing machine. A CMake build description is also supplied under `runtime/`; the recorded acceptance run used the Python build tool.

	To independently regenerate the real-proof import, install PyCryptodome in the selected Python environment and run:

	```powershell
	python tools/import_etchash_answers.py --blocks sources/ETC_Mainnet_11700000_11700002.json --output <new-import-directory> --cache-dir <verification-cache-directory>
	build/tk-hvac.exe build --input <new-import-directory>/answers.bits --domain etchash-import-v1 --output <new-corpus-directory> --jobs-per-page 0b1
	```

	No network call is made by this importer. It constructs the ETC epoch-195 verification cache and regenerates the dataset items needed to verify the supplied nonces. This cost belongs to import/verification, not runtime lookup. The [independent verifier](../reference/etchash_light.py) first passes the [core-geth Hashimoto test vector](https://github.com/etclabscore/core-geth/blob/master/consensus/ethash/algorithm_test.go), and applies [ECIP-1099](https://ecips.ethereumclassic.org/ECIPs/ecip-1099) for epoch/seed identity. Source block JSON was fetched read-only from Blockscout's Ethereum Classic RPC endpoint; every full header hash, mix digest and target result was recomputed.

	## A proved target-interval transport relation

	For a fixed rule identity, epoch and seal, import a verified answer `(nonce,mix)` and its exact final result `R=HashimotoResult(nonce)`. The target coordinate has the declared signed field

	```text
	f_R(T) = R - T
	covered(T) iff f_R(T) <= 0
	answer(T) = the same verified nonce/mix
	```

	As a real one-dimensional defining program, `f_R` is the negative-inside signed distance of the half-line `[R,+infinity)`. Admitted target queries are finite unsigned 256-bit integers. The runtime computes its membership by lexicographic comparison of equal-width big-endian bytes, without floating point or an overflowing 256-bit subtraction. The boundary is accepted, matching the consensus target predicate.

	This is a concrete reusable relation: the defining parameter `R` and its associated proof are stored once, while target queries select the same answer. The index uses a stable `(rule,epoch,seal)` prefix table and stores the minimum verified threshold for that group. It does not enumerate new nonces or run Hashimoto during lookup. A tag distinguishes this relation from an exact-key-only fixture.

	The implication follows directly: `HashimotoResult(nonce)=R` and `R<=T` imply that the same proof satisfies the queried target. For an increase `delta>=0`, target transport `T -> T+delta` within the admitted domain preserves that answer. This is a partial monotone solution relation, not an asserted group action on all Etchash jobs. A changed seal can change the whole hash computation and has no such established transport here.

	The acceptance run checks three different verified seals, each at `T=R`, `T=R+1` and the maximum target, plus rejection at `T=R-1`. These nine transported-target queries and the original-job lookups produce identical CPU/GPU answers through page replacement.

	## Evidence and remaining scope

	[RUNTIME_VALIDATION.json](../reports/RUNTIME_VALIDATION.json) records the native checks, actual GPU, repeated covered queries and eviction counts. [The import receipt](../examples/verified_etc/verification.json) records the three exact jobs and independently recomputed proofs. The synthetic packet tests exercise non-word-aligned views, cross-word reads, malformed input, CRC rejection, cycle termination, relocation, fresh-process replay and stale generations.

	The real-proof test repeatedly resolves three distinct covered keys through a single resident slot and compares CPU/GPU output bytes. Changing rule, epoch or seal returns `OutsideCoverage`. A target below the verified proof result also returns `OutsideCoverage`; target equality and larger targets resolve through the exact threshold relation below. A geometric resemblance alone cannot authorize another changed job.

	The principal remaining mathematical requirement is a solution-preserving transport/construction rule for unseen Etchash jobs. The engineering work still includes arbitrary typed field-program serialization, full kinematic calculus and traversal, asynchronous streaming, measured cache/bandwidth behavior, and calibrated physical material/HVAC adapters. No live mining throughput or unseen-job speedup is claimed.