Repository navigation
Conversation
…-0..EG-9 The operator's spec, committed byte-for-byte (sha256 7f825e1f1f6a3215...). Epic #4898 on 0.72.0; rows EG-0..EG-9 are #4899..#4908, minted with `pmat work add --epic 4898 --github-issue N`. Refs #4898 #4899 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Agent: apr-embed
…tooling - contracts/embeddinggemma2-forward-v1.yaml: local/global attention, gated GELU FFN, mean pool, projection, L2 normalise, truncation. Every obligation has an id; pv validate and pv lint report 0 errors, 0 warnings. - docs/audits/APR-EMBED-001/corpus: built by scripts/apr_embed_corpus.sh from the MIT book at a pinned commit; sha256 manifest; texts x 7 prompts + the document form, 5 lengths, batch-invariance set, retrieval micro-set, and train/held-out pairs split by chapter. - scripts/apr_embed_probe.sh + EG-0/probe-verbs.tsv: the 50-verb probe (a). Refs #4899 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
… guard, embedding ops
(a) Probe of 50 verbs on the UD-Q4_K_XL file, exit code and first line each.
(b) inspect + tensors on all 8 files; m9.md gives every M9 value with its
command (F16-on-oracle pending (c)).
(d) apr-cli-commands-v1.yaml: every command declares one verdict per model
kind (receipt / refuse / no-model), refusals name the verb to use. The
totality guard is two tests in the existing cli_commands target
(fragment 050, so ci / gate via workspace-test); mutation RED receipt in
d-totality-mutation.md.
(e) apr-model-capability-v1.yaml (+ mirror): eight embedding ops, all
gpu_supported false with a reason; CausalMask moves from `always` to
`by_kind.generative`. RequiredOp gains the eight variants; nothing
derives them yet (EG-1/EG-2).
D-1: epic E10 Embeddings on 0.72 (budget 6) and the 0.72 §1.5 row.
Refs #4899
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Agent: apr-embed
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
The new embeddinggemma2-forward-v1 contract tripped six tests in workspace-test: its ten `formal:` lines carried no declared symbol (the shrink-only formal_prose baseline rose 1464 -> 1473), its lean_theorem labels named theorems that do not exist, and contracts.nt plus the witness were not regenerated. - Rewrite every `formal:` with symbols the ontology declares. - Drop the lean_theorem labels; no Lean proof exists yet. - Regenerate contracts.nt (pv extract) and the witness (pv-sat). Verified: ont2b_sigma_gate 8, ont4b_shapes_gate 11, ont5_consistency_gate 5, ont8_evidence_gate 8, pvl_discharge_check 15, all passing. No baseline or allow-list was edited. Refs #4899 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
…ind from the file
- model_kind.rs: ModelKind {Generative, Embedding} by an exact, case-insensitive
match on gemma-embedding2; the gemma prefix match is not widened. A causal
embedding file is refused. per_layer_kv_heads reads the head_count_kv array per
layer (scalar broadcasts, wrong length refused); layer_attention_kinds reads
local/global from attn_q widths (I-9).
- contract_gate: gemma-embedding2 is refused on the generative path at gate
model_kind, naming `apr embed` (I-3), instead of the Gemma3 message.
- contracts/embeddinggemma2-load-v1.yaml: 5 obligations, 5 falsifiers.
FALSIFY-EG2L-004 observed RED before the gate change, GREEN after. Five planted
mutants in model_kind.rs (prefix match, causal guard, first-entry KV, kind flip,
length check) each turn a test RED. aprender-serve lib: model_kind + contract_gate
50 passed; clippy -D warnings clean; ont2b/ont4b/ont5/ont8/pvl_discharge green.
Refs #4900
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Agent: apr-embed
…er collapses an array GGUFConfig::from_gguf read attention.head_count_kv through a UInt32-only reader, so an array value fell through to num_heads silently (I-9). It now goes through model_kind::num_kv_heads_per_layer and model_kind::uniform_kv_heads: - absent key: num_heads, as before; scalar: unchanged - uniform array: its value (was num_heads) - non-uniform, wrong-length, zero or non-integer array: refused (InvalidShape) by name Behaviour change outside the embedding path: a GGUF with per-layer head counts (e.g. OpenELM, hybrid files with 0 KV heads on SSM layers) used to load with a guessed num_heads and kv = num_heads; it is now refused instead of run with fabricated head counts. Contract embeddinggemma2-load-v1: EG2L-INV-006 + FALSIFY-EG2L-006. RED observed before the change (uniform array gave 4, non-uniform loaded); two mutants killed (uniform check removed, array ignored). gguf lib suite 2375 passed; clippy -D warnings clean; pv validate 0 errors; ont2b/4b/5/8 + pvl discharge green. Refs #4900 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
…by kind `apr chat` on a gemma-embedding2 GGUF exited 0. The contract gate's model_kind refusal ran only inside the CUDA preload, and a failure there printed `will use CPU` and continued; the CPU path ran no gate, so an empty stdin ended the session cleanly. One refusal, `commands::model_kind_gate::refuse_non_generative`, now runs in `ChatSession::new` before any tokenizer or backend is built, and at the top of `build_serve_model`, which every GGUF serve route goes through. Both exit 6 (ModelLoadFailed) and name `apr embed` (I-3). A causal embedding file is refused by name. Generative files and headers that do not parse go on to the loaders unchanged. realizar gains `model_kind::gguf_model_kind`, which reads the kind from a parsed file. FALSIFY-EG2L-007 / EG2L-INV-007 in embeddinggemma2-load-v1. RED before wiring: chat exited 4 on the missing tokenizer, and serve was refused over missing metadata; neither named the kind. GREEN 5/5. apr-cli chat+serve 723 passed; model_kind 14/14; clippy -D warnings clean; fmt clean; pv validate 0 errors; ont2b/4b/5/8 and pvl discharge green. Refs #4900 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
…laries A gemma4 GGUF (tokenizer.ggml.model = gemma4, 262,144 tokens plus merges) fell to greedy longest-match, so its ids departed from llama.cpp's. This ports llama.cpp's gemma4 BPE session: specials first, space -> U+2581 with no prefix, [^\n]+|[\n]+ runs, merges keyed by text (lowest rank, leftmost on ties, stale pairs skipped), unknown symbols to <0xXX> byte tokens. - gguf/spm_bpe.rs + 12-row case table (FALSIFY-EG2L-008) - GGUFModel::encode tries SPM-style BPE, then byte-level BPE, then greedy - apr tokenize reports canonical for gemma4; tokenizer_parity.sh matches the new uncovered message - metadata.rs get_tensor_f32: the per-qtype arms become one block table + tensor_byte_range, behaviour unchanged. token.rs is include!d next to it, so its cognitive complexity (66) blocked any token.rs commit at the hook cargo test -p aprender-serve --lib -- gguf tensor encode token: 4124 passed, 0 failed. clippy -D warnings clean on aprender-serve and apr-cli. Refs #4900 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
…sional oracle The pinned llama.cpp refuses gemma-embedding2 (D-3 is a STOP), so this records the provisional measurement, not the gate receipt. Refs #4900 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
…gate embeddinggemma2-load-v1.yaml is a new contract; make readme-sync and make roadmap-aggregate keep FALSIFY-README-002 and the roadmap DRIFT guard green. Refs #4900 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
An embedding GGUF reaches `apr flow` with no LM head and per-layer attention widths. The decoder drawing assumed both, so flow now reads the model kind first and draws the embedding graph: token embedding, the per-layer input projection, the local and global blocks with their widths, the output projection and mean pooling. A decoder model takes the old path unchanged. Refs #4900 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: apr-embed
The EG-1 verb sweep ran `apr validate` on the six Unsloth EmbeddingGemma 2 files. It failed three of them: BF16 (219 tensors), Q8_0 and UD-Q6_K_XL (one tensor each, per_layer_model_proj.weight, which every file stores as BF16). The cause was that GgufReader::get_tensor_f32 sized ggml type 30 but had no arm for it, so it refused each tensor with "no dequantizer". BF16 is the top 16 bits of an F32, so it widens bit-exactly. F16 and BF16 now share one two-byte path (widen_half), and each keeps its own widening. A short data section is still refused by name, and the bounds check no longer adds without overflow checking. Widening scope: get_all_tensors_f32 (the GH-375 fallback of `apr import`, and `apr convert`) now reads BF16 too. Unlike the #3947 IQ decoders this widens and decodes nothing, so it invents no weight. A test pins it. Tests (reader_tests_ggml_sizes.rs): - BF16 widens bit-exactly, including -0.0, the smallest normal and infinity; the 0xEE tail is not read. - F16 keeps its own widening. 0x3C00 is 1.0 in F16 and 2^-7 in BF16, so a swapped widener fails. - Short BF16 data is refused. - The whole-model load returns the same exact values. Refs #4900 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…_bit_mask) clippy --profile test on aprender-core flagged the low-16-bit mask in the BF16 widening test; trailing_zeros() >= 16 is the same predicate (0 gives 32). Refs #4900 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The 14 verbs run on the six unsloth embeddinggemma-2 GGUF files, each cell scored on exit code 0 and a positive check of its output. Run 1 (85ac2d1) scored 75/84: 3 validate failures from BF16 tensors that aprender-core could not read (fixed in 2a42c3d) and 6 list checks that looked for a file name an hf:// single-file pull never prints. Run 2 (2a42c3d) scored 84/84 with the list/rm checks reading the cache path from the pull log, so rm can no longer pass vacuously. With the tokenizer parity receipt (1120/1120), this covers both halves of the EG-1 done_when. Refs #4900 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
`apr embed` now reads an EmbeddingGemma 2 GGUF file as well as a BERT APR file; the file's magic bytes pick the path. The GGUF path takes its tokenizer, sizes and mean pooling from the file, applies the model card's task prompts (`--task`, `--title`), and keeps a re-normalised Matryoshka prefix with `--dim 512|256|128`. Vectors are unit length. The forward is its own module: centred local window |i - j| <= W/2 on the sliding layers, partial NeoX RoPE with per-kind bases, q/k RMS norms, a weightless v norm, score scale 1.0, a GELU-gated FFN and the per-layer embedding inputs. The embeddinggemma2-forward contract goes to v1.1.0 with the scale and the centred window corrected. Weight shapes are read as [out, in], the order the GGUF reader holds them in, and a fixture test holds the fixture to that order: a fixture written the other way round had let a forward that read the other way round pass every unit test. A BERT APR file without `--vocab` now exits 5 (validation) instead of 2 (usage): the flag is optional because a GGUF file carries its own tokenizer. Parity against the oracle is provisional (the pinned llama.cpp refuses the architecture; moving the pin is D-3): see the EG-2 receipt. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ap regenerated) Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
EG2-INV-002 named the local half window with a floor glyph that Σ does not declare; it is now h, defined in the property. FALSIFY-EG2L-007 cited `falsify_eg2l_007_*`; the binding gate matches a bare name as a substring without trimming the star, so it resolved to nothing. It now cites the prefix, which is also the filter `cargo test` takes. FALSIFY-EG2L-008 cites the spm_bpe tests module instead of a trailing `::*`. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
pv-sat on the merged tree: the census id set now includes the embeddinggemma2 load and forward contracts. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ard tests Review of the EG-0..EG-2 branch found two contract statements that did not match the code. - apr-cli-commands-v1: `serve` declared `embedding: receipt`, but `apr serve run` refuses an embedding file with exit 6 and names `apr embed` (FALSIFY-EG2L-007). Under I-3 that cell is a refusal. It is now `refuse` with `use_instead: embed`; EG-3 (serve) flips it back when it lands. - embeddinggemma2-forward-v1: FALSIFY-EG2-001, 002, 007 and 008 named prose from the EG-0 pre-registration. EG-2 has a test for each, so each now cites it by name and the strict test-binding gate resolves it. 003, 004, 005, 006, 009 and 010 have no exact test yet and keep their prose. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ADME count and roadmap regenerated) - gguf/metadata.rs: main landed the same `dequantize_at` split for #4991 with an identical signature; main's version is taken, and the EG-2 row reader calls it unchanged. - serve/handler_gpu_completion.rs: both sides added a test after the zero-layer test; both are kept. The embedding refusal still runs before main's new hybrid check in `build_serve_model`. - The ONT witness is taken from main and regenerated in the next commit. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
pv-sat over the merged contracts/ tree. The contracts lib tests ran against this witness: 2292 passed, 0 failed. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
§13.11 rung 1 — quorum shadow verdict Shadow mode: this records a verdict and merges nothing. A refusal |
…ranch moved The branch edits extended_commands.rs and dispatch_analysis.rs, which 83 ledger rows cite by line, so the dogfood coverage gate (G2.1 freshness) was red. Every cited line was mapped through the branch diff and checked to carry the same text at its new number. Two rows already pointed at the wrong line on main and now cite the definition they describe: apr embed -> the Embed variant, apr dataset audio-inspect -> AudioInspect. check_dogfood_coverage.sh: PASS, self-test rc 0. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ed.rs Two guard-cargo rows were red on the PR head: - bashrs SEC/DET/IDEM (#3196): five SEC010 path-traversal findings in apr_embed_corpus.sh and apr_embed_probe.sh. Both now refuse an output path containing '..' (exit 2), and the probe refuses a verb that is not a plain name before it becomes a directory. check_bashrs_gate.sh: PASS, 551 files, 0 SEC/DET/IDEM errors. - include!d files formatted (#4151): matmul_fused.rs, touched by EG-2, was not rustfmt-clean. Formatted; include_fmt_ratchet.sh rc 0. Refs #4901 Agent: apr-embed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
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
APR-EMBED-001 rows EG-0, EG-1 and EG-2: EmbeddingGemma 2 loads as its own model kind and
apr embedruns it on GGUF.ModelKind::Embeddingby an exact match (thegemmaprefix match is not widened). Per-layer KV heads and the attention type are read from the file. SPM-style BPE tokenizer for gemma4 vocabularies. Generative verbs refuse the file by kind.apr embedtakes a GGUF and reads sizes from the file, with--task,--titleand--dim. The BERT path is unchanged.Evidence
docs/audits/APR-EMBED-001/EG-2/parity.md, cells ini8-cells.tsv. 840 cells (6 files x 7 prompts x 5 lengths x 4 dims) against a llama.cpp oracle. Result: PASS (provisional), because the pinned oracle build refuses this architecture (D-3). Every cell is above the 0.98 floor; the floor is not moved.aprender-contracts --lib2292 passed, 0 failed; the EG-2 aprender-serve and apr-cli subsets pass; clippy-D warningsis clean on both libs.Notes
Refs #4898
Refs #4900
Refs #4901
keep-open: #4898 stays open after this merges. It is the epic; rows EG-3 to EG-9 remain.
keep-open: #4900 stays open after this merges. The row closes after its receipt is reviewed on main.
keep-open: #4901 stays open after this merges. Its parity is provisional until an oracle build that accepts the architecture is pinned.
ont-delta: shape apr-cli-commands-v1 gains a per-command, per-kind verdict (EG-0 d); the release spec gains the 0.72 APR-EMBED-001 row; README contract count regenerated
🤖 Generated with Claude Code