allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/.opencode/agents/port-fixedpoint-bridge.md
Brandon Schneider ede983168c feat(lean): complete goldenContractionEnergyDecrease proof + PIST predictions pipeline v2 
- 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)
2026-05-27 12:40:16 -05:00

1.6 KiB
Raw Blame History

description mode model permission
Rewrite FixedPointBridge.lean conversions using pure integer arithmetic (remove Float dependency). Use ONLY when asked to port FixedPointBridge or eliminate Float from compute paths. subagent anthropic/claude-sonnet-4-6
edit bash read
allow allow 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.