Adds 6 new sections addressing concrete drift patterns found by auditing
the Compiler surface:
1. ofFloat leakage — Compiler-surface modules (RRC.*, AVMIsa.*, ReceiptCore)
must have zero ofFloat calls in any compute path; undocumented magic
integers are a bug.
2. #eval witness contract — every #eval must carry a '-- expect:' comment
with a hand-computed expected value; treat divergence as a failing test.
3. Namespace/closing discipline — namespace X must close with 'end X'
as the last non-blank line; no file-level open leakage; BEq RRCShape
pitfall documented.
4. Lakefile/Compiler surface discipline — Compiler roots are frozen;
job-count decrease after a change is an error signal.
5. Schema and claim_boundary strings — versioned, named, must not be
renamed; table of current schemas added; vague strings forbidden.
6. Promotion gate invariant — promotion=not_promoted is a hard invariant;
Promotion.candidate in any new code requires user approval.
Also adds: axiom/unsafe/native_decide prohibition, canonical Python shim
BOUNDARY comment format (exact format, PARTIAL BOUNDARY for mixed files).
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Adds .devin/skills/lean-proof/SKILL.md enforcing:
- Double-check output after every lake build (re-read + verify #eval values)
- Sorries must be explained (why deferred, proof sketch, TODO_MAP tracking)
or eliminated — bare sorry not acceptable
- TODOs follow the same contract: named, sketched, tracked
- No tautological theorems — proof must guarantee something non-trivial
about a domain type; trivially-true wrappers are forbidden
- Proof must have a stated purpose answering "what does this guarantee?"
- Q16_16 fixed-point contract (no Float in compute paths)
- Namespace/import conventions for RRC and RRCLogogramProjection
- Reference file index for the Lean workspace
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Adds .devin/config.json with a UserPromptSubmit hook that fires on every
user message and injects the programming choice flow + post-interaction
checklist into the agent's context via add_context.
.devin/hooks/programming-choice-reminder.sh:
Emits a JSON add_context block with the 7-branch decision tree:
1. Admissibility/gating → Lean only
2. Receipt minting / top-level JSON → AVMIsa.Emit only
3. Alignment classification → Lean (RRC.Emit)
4. Raw input features → Python shim OK with constraints
5. Float in compute path → STOP, use Q16_16
6. Promotion in shim space → STOP, not_promoted until Lean gate passes
7. Pure I/O → Python fine, route receipts through AVMIsa.Emit
Plus the 4-step post-interaction checklist (AGENTS.md / build / commit / status)
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
