Formal CHD/quant proofs, SentencePiece runtime, and native packaging - #6
Merged
Conversation
Keep fetch/stage outputs local so binding native/ dirs and dist/native are not published as prebuilts.
Prove cleared-denominator Nat/Int round and L1 bounds so Float claims can stay honest markers instead of axioms.
Point Core/LayerBound at Fixed Int theorems and keep Float L2 claims as True markers after aborting IEEE discharge.
Provide shared CHD hash-mod bounds used by builders and well-sized placement proofs.
Capture injective key-to-slot post-conditions and disjoint bucket merge so MPH success is checkable without the Rust search loop.
Executable findDisplace/assembleBucketed now carry wellFormed implications and stable bucket ordering aligned with the Rust builder.
Locate optional guardd CLI binaries so tests can exercise SHA-256 and related sidecars when present.
Clarify that simpleDigest is a Lean placeholder and prefer the Rust guardd_sha256 sidecar for real hashes.
Align PerfectHashTokenizer with CHD runtime vocabulary and fix vocab_size to depend on the tokenizer instance.
Export the new formal modules from ModelAssetGuard so lake builds and Tests can import them.
Cover Fixed/CHDBuild goldens, quantization_error_matrix correctness, and optional guardd_sha256 when built.
Replace simulated Lean CLI success paths with RustSidecar runners so missing binaries fail closed.
Expose sha256, perfect_hash, bitflip, and quant128 sidecars for Lean/CI and drop unused libc/winapi deps.
Stabilize length-then-id bucket sort and LambdaPlanCase so MPH tables match Lean assembleBucketed and satisfy clippy.
Implement stock-aligned encode paths with honest nbest/MT19937 limits and curated NFKC support rather than claiming full Unicode parity.
Wire SentencePiece/CHD modules into the cdylib API and mark guardd_verify_quant deprecated in favor of the 128-vector verifier.
Strengthen runtime L2 checks that remain authoritative while Lean Float claims stay obligation markers.
Improve deterministic corpus tooling used by the guardd_bitflip sidecar and integration tests.
Record proven CHD/Fixed theorems and honest MPH runtime limits so formal claims stay auditable.
Explain why Mathlib/IEEE refinement was refused and keep Float markers as non-axiom obligations.
State MT19937/nbest and NFKC limits clearly so support is not over-claimed versus stock SentencePiece.
Describe release-asset-first fetch, CI fallback, and that npm/PyPI do not ship embedded prebuilts yet.
Prefer GitHub release assets with CI artifact fallback and copy libraries into binding native/ dirs for local use.
Fail closed if Lean sources introduce axiom declarations contrary to the documented zero-axiom policy.
Align packaging helpers with per-OS guardd-native uploads and fetch/stage workflows.
Provide npm fetch-native/smoke scripts and document that binaries are staged locally, not published in the package.
Expose model-asset-guard-fetch-native via setuptools and mark integration tests so default pytest stays offline.
Prefer staged native/ then cargo target paths so local fetch/stage workflows work without embedding binaries.
Match Node search order for staged natives and keep optional HF/torch paths behind extras.
Upload per-OS guardd-native artifacts, run axiom checks, and keep formal/bundle jobs aligned with the new sidecars.
Document fetch/stage natives, formal modules, and repository URLs without claiming published prebuilt packages.
Expand curated normalize goldens and miniature models for offline encode/normalize cross-checks.
Provide a stable epsilon corpus for guardd 128-vector quantization checks.
Keep default pytest offline via markers while covering staged natives and SP normalize/encode paths.
Gate network/HF cases behind the integration marker and focus perfect-hash coverage on CHD round-trips.
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
guardd_verify_quant, stronger quant/bitflip paths.Test plan
lake build/ Lean Tests for CHD and Fixed goldenscargo test/cargo clippyinsrc/rust/guarddpytestdefault (offline) and optional-m integrationscripts/fetch_guardd_native+ Node/Python smoke against staged native