Skip to content

Commit 3303012

Browse files
noahgiftclaude
andcommitted
feat(crux-b-02): GGUF→safetensors output-layout + metadata-translation + PEFT target-module classifier (3 of 4 FALSIFY at PARTIAL_ALGORITHM_LEVEL)
Three pure classifiers in crates/apr-cli/src/commands/gguf_to_safetensors.rs: 1. hf_required_files() + missing_hf_files(listing) — canonical trio {model.safetensors, config.json, tokenizer.json} that a converted directory must contain. Without these filenames, no downstream HF byte-level load can begin. 2. translate_gguf_metadata(gguf_kv) -> HfLlamaConfig — pure mapping from GGUF llama.* keys onto the HF config.json fields. Missing keys return Err(MissingKey) rather than silently defaulting, which would let from_pretrained succeed with the wrong layer count and produce garbage. 3. peft_target_modules_resolve(tensor_names, target_modules) — substring-match check that every PEFT target (q_proj, v_proj, ...) resolves to at least one tensor. Mirrors PEFT's own name-matching rule. Unresolved targets are flagged before the attach call. Contract crux-B-02-v1.yaml v1.0.0-draft -> v1.1.0 (draft -> partial): - FALSIFY-001 (required files present): PARTIAL_ALGORITHM_LEVEL (5 tests) - FALSIFY-002 (dequant numerical bound): NOT_DISCHARGED (needs Q4_K_M harness) - FALSIFY-003 (transformers loads output): PARTIAL_ALGORITHM_LEVEL (8 tests) - FALSIFY-004 (PEFT LoRA attaches): PARTIAL_ALGORITHM_LEVEL (5 tests) 18 / 18 tests pass. pv validate: 0 errors, 0 warnings. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
1 parent d853e91 commit 3303012

3 files changed

Lines changed: 429 additions & 2 deletions

File tree

contracts/crux-B-02-v1.yaml

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,11 @@
66

77
metadata:
88
id: CRUX-B-02
9-
version: "1.0.0-draft"
9+
version: "1.1.0"
1010
created: "2026-04-18"
1111
author: PAIML Engineering
1212
registry: true
13-
status: draft
13+
status: partial
1414
parent_contracts:
1515
- crux-competitive-research-ux-v1
1616
category: "B — Inspection & Debugging"
@@ -80,6 +80,23 @@ falsification_tests:
8080
[ -f "$TMP/$f" ] || { echo "missing $f"; exit 1; }
8181
done
8282
if_fails: "converted directory is missing required HuggingFace files"
83+
evidence_discharged_by:
84+
classifier_path: crates/apr-cli/src/commands/gguf_to_safetensors.rs
85+
sub_claim: |
86+
Algorithm-level necessary condition: `hf_required_files()` is the
87+
canonical trio HF transformers expects, and `missing_hf_files`
88+
reports the exact subset absent from any candidate directory
89+
listing. Without these filenames present, no downstream byte-
90+
level load work can succeed.
91+
tests:
92+
- required_files_set_is_canonical
93+
- missing_files_empty_on_complete_output
94+
- missing_files_flags_each_omission
95+
- missing_files_flags_all_when_empty
96+
- required_files_set_is_deterministic
97+
scope: output-directory file-layout (pure set)
98+
discharge_status: PARTIAL_ALGORITHM_LEVEL
99+
full_discharge_blocked_on: end-to-end `apr convert --format safetensors` fixture harness
83100

84101
- id: FALSIFY-CRUX-B-02-002
85102
rule: dequant numerical bound
@@ -112,6 +129,28 @@ falsification_tests:
112129
assert m is not None
113130
"
114131
if_fails: "transformers cannot load the converted safetensors directory"
132+
evidence_discharged_by:
133+
classifier_path: crates/apr-cli/src/commands/gguf_to_safetensors.rs
134+
sub_claim: |
135+
Algorithm-level necessary condition: `translate_gguf_metadata`
136+
produces a well-typed `HfLlamaConfig` with the four required
137+
fields (architectures, hidden_size, num_hidden_layers,
138+
num_attention_heads) and serializes round-trip clean through
139+
serde_json. Missing keys return Err rather than silently
140+
defaulting, which would hide upstream bugs and let
141+
`from_pretrained` succeed with the wrong layer count.
142+
tests:
143+
- translate_full_metadata_succeeds
144+
- translate_missing_architecture_errors
145+
- translate_missing_hidden_size_errors
146+
- translate_missing_layer_count_errors
147+
- translate_missing_head_count_errors
148+
- translate_wrong_type_errors
149+
- translate_is_deterministic
150+
- translate_config_roundtrips_through_json
151+
scope: GGUF KV → HF config.json translator (pure function)
152+
discharge_status: PARTIAL_ALGORITHM_LEVEL
153+
full_discharge_blocked_on: uv run transformers AutoModelForCausalLM.from_pretrained harness
115154

116155
- id: FALSIFY-CRUX-B-02-004
117156
rule: peft LoRA attaches without shape errors
@@ -127,6 +166,24 @@ falsification_tests:
127166
assert sum(p.numel() for p in m2.parameters() if p.requires_grad) > 0
128167
"
129168
if_fails: "PEFT LoRA attachment failed — converted output is not PEFT-ready"
169+
evidence_discharged_by:
170+
classifier_path: crates/apr-cli/src/commands/gguf_to_safetensors.rs
171+
sub_claim: |
172+
Algorithm-level necessary condition: `peft_target_modules_resolve`
173+
checks that every target module name (q_proj, v_proj, etc.)
174+
matches at least one tensor in the safetensors archive via
175+
substring containment, mirroring PEFT's own name-matching rule.
176+
If every target resolves, `peft.get_peft_model` has the
177+
precondition it needs to attach LoRA adapters.
178+
tests:
179+
- peft_default_targets_resolve_on_llama_layout
180+
- peft_unknown_target_module_flagged
181+
- peft_empty_tensor_list_fails_all_targets
182+
- peft_empty_target_list_trivially_resolves
183+
- peft_resolution_is_deterministic
184+
scope: PEFT target-module resolver (pure function over tensor names)
185+
discharge_status: PARTIAL_ALGORITHM_LEVEL
186+
full_discharge_blocked_on: uv run peft get_peft_model attach harness
130187

131188
proof_obligations:
132189
- type: invariant
@@ -143,6 +200,19 @@ verification_summary:
143200
proven: 0
144201
tested: 0
145202
status: spec-complete
203+
discharge_ledger:
204+
- falsify_id: FALSIFY-CRUX-B-02-001
205+
discharge_status: PARTIAL_ALGORITHM_LEVEL
206+
blocked_on: end-to-end apr convert --format safetensors fixture harness
207+
- falsify_id: FALSIFY-CRUX-B-02-002
208+
discharge_status: NOT_DISCHARGED
209+
blocked_on: Q4_K_M dequant numerical harness vs reference f32
210+
- falsify_id: FALSIFY-CRUX-B-02-003
211+
discharge_status: PARTIAL_ALGORITHM_LEVEL
212+
blocked_on: uv run transformers AutoModelForCausalLM.from_pretrained harness
213+
- falsify_id: FALSIFY-CRUX-B-02-004
214+
discharge_status: PARTIAL_ALGORITHM_LEVEL
215+
blocked_on: uv run peft get_peft_model attach harness
146216

147217
pmat_work_tracking:
148218
# Managed by master contract §12. If intake_status == "missing", a ticket

0 commit comments

Comments
 (0)