mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
ede983168c
- PistSimulation.lean: proven goldenContractionEnergyDecrease (no sorry) 7 supporting lemmas, h_u'_nonneg + h_pt hypothesis, fold induction - Connectors.lean: restored zeroIsVoid theorem with Q16_16 proof - CanonSerialization.lean: removed dead theorem, documented blocker - FixedPointBridge.lean: eliminated Float from compute paths PIST predictions pipeline: - pist_matrix_builder.py: reproducible matrix-only builder (SHA256) - build_pist_matrices_278.py: generates PIST/Matrices278.lean - PIST/Classify.lean: classifyProxy/classifyExact stubs (v2 surface) - PIST/Matrices278.lean: 250-entry matrix HashMap - build_corpus278.py: reads predictions artifact, uses classify* - Pipeline contract documented in root AGENTS.md Cleanup: - Archived 5 orphan pist_* shims, 5 old route_repair variants - Quarantined PIST/Repair.lean (no external callers) - Created 4 opencode agents for remaining TODO items Build: PistSimulation 3309, Compiler 3313, Full 3571 (0 errors)
39 lines
1.6 KiB
Markdown
39 lines
1.6 KiB
Markdown
---
|
|
description: Rewrite FixedPointBridge.lean conversions using pure integer arithmetic (remove Float dependency). Use ONLY when asked to port FixedPointBridge or eliminate Float from compute paths.
|
|
mode: subagent
|
|
model: anthropic/claude-sonnet-4-6
|
|
permission:
|
|
edit: allow
|
|
bash: allow
|
|
read: allow
|
|
---
|
|
|
|
# Port FixedPointBridge
|
|
|
|
## Context
|
|
|
|
`Semantics/FixedPointBridge.lean:13` has:
|
|
```
|
|
TODO(lean-port): Rewrite conversions using pure integer arithmetic:
|
|
- toFloat / fromFloat are used only at the external boundary
|
|
- Internal compute should use ofNat / ofRatio / ofInt
|
|
```
|
|
|
|
Per root AGENTS.md: "Float (ofFloat) is forbidden in compute paths. Q16_16.ofNat and Q16_16.ofRatio are the canonical constructors."
|
|
|
|
## What to do
|
|
|
|
1. Read `Semantics/FixedPointBridge.lean` fully.
|
|
2. Identify every call to `ofFloat`, `toFloat`, or any Float-dependent conversion.
|
|
3. For each call, determine if it's:
|
|
- An external boundary (JSON parsing, sensor input) → mark with a comment noting it's boundary-only.
|
|
- An internal compute path → rewrite using `Q16_16.ofNat` / `Q16_16.ofRatio` / `Q16_16.ofInt`.
|
|
4. After rewriting, remove the `TODO(lean-port)` marker.
|
|
5. Run `lake build Compiler` and `lake build` to verify.
|
|
6. Run `grep -rn 'ofFloat\|toFloat' Semantics/ --include='*.lean' | grep -v lake-packages` to check for remaining Float usage.
|
|
|
|
## Constraints
|
|
|
|
- `ofFloat` is PERMITTED at the external boundary (JSON parsing, sensor input) but must be immediately bracketed with a comment.
|
|
- `ofFloat` is FORBIDDEN in internal compute paths.
|
|
- Do NOT change public API signatures unless necessary.
|