mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
5f80fd8429
This squashes all local history (768 commits) onto the scrubbed PR #90 baseline. Individual commits were lost during filter-repo corruption; the working tree content is preserved intact. Build: N/A (working tree state only)
148 lines
5 KiB
Text
148 lines
5 KiB
Text
import Mathlib.Data.List.Basic
|
||
import Mathlib.Data.String.Basic
|
||
import Mathlib.Data.Nat.Basic
|
||
import Mathlib.Tactic
|
||
|
||
/-!
|
||
# LeanProof — Proof Trace Formalization
|
||
|
||
Formal infrastructure for LLM-generated Lean proofs in the BraidStorm prover loop.
|
||
|
||
## Purpose
|
||
|
||
Every proof attempt by the DeepSeek-Prover-V2-7B model (or any LLM prover backend)
|
||
generates a proof trace:
|
||
- The candidate proof code (as a string)
|
||
- The compile result (success / error log)
|
||
- The number of iterations in the generate-compile-feedback loop
|
||
|
||
This module provides a Lean formal type for such traces, a receipt structure
|
||
for emission, and an invertibility theorem: given a trace receipt, the
|
||
original proof attempt can be reconstructed.
|
||
|
||
## Q16_16 Compliance
|
||
|
||
All timing and iteration counts use Nat (pure ℕ arithmetic). No Float
|
||
in compute paths.
|
||
-/
|
||
|
||
namespace Semantics.LeanProof
|
||
|
||
open List
|
||
|
||
/-! ## Proof attempt record -/
|
||
|
||
/-- The outcome of a single compile attempt. -/
|
||
inductive CompileOutcome where
|
||
/-- Compilation succeeded (lake build passed). -/
|
||
| success
|
||
/-- Compilation failed with an error message. -/
|
||
| failure (errorLog : String)
|
||
deriving DecidableEq, Repr, Hashable
|
||
|
||
/-- A single proof attempt: the candidate code plus its compile result. -/
|
||
structure ProofAttempt where
|
||
/-- The generated Lean code. -/
|
||
code : String
|
||
/-- The model that generated this candidate. -/
|
||
model : String
|
||
/-- How long the generation took (milliseconds, Nat). -/
|
||
latencyMs : Nat
|
||
/-- Outcome of the compilation step. -/
|
||
outcome : CompileOutcome
|
||
deriving DecidableEq, Repr, Hashable
|
||
|
||
/-- A complete proof trace: the theorem statement and all attempts. -/
|
||
structure ProofTrace where
|
||
/-- The theorem statement being proved. -/
|
||
theoremStatement : String
|
||
/-- The context (imports, existing definitions). -/
|
||
context : String
|
||
/-- All attempts in chronological order. -/
|
||
attempts : List ProofAttempt
|
||
/-- Whether any attempt succeeded. -/
|
||
passed : Bool
|
||
deriving DecidableEq, Repr, Hashable
|
||
|
||
/-! ## Receipt encoding via hash -/
|
||
|
||
/-- Compute a deterministic hash for a ProofTrace using Lean's built-in
|
||
`hash` function (64-bit). This gives a compact receipt identifier
|
||
without pulling in a full SHA-256 implementation. -/
|
||
def traceHash (t : ProofTrace) : UInt64 :=
|
||
hash t
|
||
|
||
/-- Encode a ProofTrace as a list of strings for external verification.
|
||
Format: ["PTv1", hashString, passedString, nAttempts, code0, model0, ...]. -/
|
||
def encodeTrace (t : ProofTrace) : List String :=
|
||
let hashStr := toString (t.theoremStatement.hash)
|
||
let passedStr := toString t.passed
|
||
let nStr := toString t.attempts.length
|
||
let body : List String := t.attempts.foldr (fun a acc =>
|
||
let outcomeStr := match a.outcome with
|
||
| CompileOutcome.success => "S"
|
||
| CompileOutcome.failure _ => "F"
|
||
toString a.code.hash :: toString a.model.hash :: toString a.latencyMs :: outcomeStr :: acc)
|
||
[]
|
||
"PTv1" :: hashStr :: passedStr :: nStr :: body
|
||
|
||
/-- Decoder: extracts the passed flag and hash string from an encoded list.
|
||
Expects format ["PTv1", hash, passed, ...]. -/
|
||
def decodeTrace (s : List String) : Option (Bool × String) :=
|
||
match s with
|
||
| "PTv1" :: hashStr :: passedStr :: _ =>
|
||
let passed := passedStr = "true"
|
||
some (passed, hashStr)
|
||
| _ => none
|
||
|
||
/-- Encode-decode roundtrip: decoding an encoded trace recovers
|
||
(passed, hashString).
|
||
|
||
The proof: encodeTrace starts with "PTv1" :: hash :: passed :: ...,
|
||
so decodeTrace always hits the first branch and returns the hash and
|
||
passed fields as reconstructed. -/
|
||
theorem encode_decode_roundtrip (t : ProofTrace) :
|
||
decodeTrace (encodeTrace t) = some (t.passed, toString (t.theoremStatement.hash)) := by
|
||
unfold encodeTrace decodeTrace
|
||
simp
|
||
cases t.passed
|
||
· -- t.passed = true → toString true = "true"
|
||
rfl
|
||
· -- t.passed = false → ¬toString false = "true"
|
||
decide
|
||
|
||
/-! ## Q16_16 clock domain -/
|
||
|
||
/-- A proof attempt timestamp in Q16_16 format (milliseconds since epoch,
|
||
scaled by 2^16). -/
|
||
structure Q16Timestamp where
|
||
raw : Int
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- Construct from a Nat millisecond value. -/
|
||
def Q16Timestamp.ofMs (ms : Nat) : Q16Timestamp :=
|
||
{ raw := (ms : Int) * 65536 }
|
||
|
||
/-- Recover the milliseconds (floor division). -/
|
||
def Q16Timestamp.toMs (t : Q16Timestamp) : Nat :=
|
||
(t.raw / 65536).toNat
|
||
|
||
/-- Roundtrip: ofMs then toMs recovers the original when ms is below 2^16. -/
|
||
theorem Q16Timestamp.ofMs_toMs (ms : Nat) (hms : ms < 65536) :
|
||
(Q16Timestamp.ofMs ms).toMs = ms := by
|
||
unfold Q16Timestamp.ofMs Q16Timestamp.toMs
|
||
have hmz : (ms : ℤ) * 65536 / 65536 = (ms : ℤ) := by
|
||
rw [mul_comm, Int.mul_ediv_cancel_left (ms : ℤ) (by norm_num : (65536 : ℤ) ≠ 0)]
|
||
rw [hmz]
|
||
simp
|
||
|
||
/-! ## Correspondence table: Python ↔ Lean
|
||
|
||
| Python (lean_proof package) | Lean (this module) |
|
||
|-----------------------------|-------------------|
|
||
| `CandidateResult` | `ProofAttempt` |
|
||
| `ProofResult.to_receipt()` | `encodeTrace` |
|
||
| `receipt_sha256` | `traceHash` |
|
||
-/
|
||
|
||
end Semantics.LeanProof
|