mirror of
https://github.com/hanzoai/proofs.git
synced 2026-10-30 18:23:34 +00:00
zeekayandHanzo Dev
3626b96b68
Every library is a default target, so any one of these failing takes the whole build down. What each was: Compute/Billing.lean, Gateway/RateLimit.lean, CRDT/Anchor.lean — `simp [f] at h` already turns the guard into a conjunction, so the `split at h` after it had nothing left to split. Destructure the conjunction and state the reduced goal for omega. In `rate_limited` the simp closed the goal, so the line after it ran on none. Compute/ConfidentialCompute.lean — `a == b = true` does not parse: `==` and `=` are both precedence 50 and non-associative. State the propositional equality, which is the stronger claim anyway. Compute/PoAI.lean — `reward_bounded` was false as stated. qualityScore is unbounded in the type, so `rate ≤ 1000` alone does not bound computeUnits * rate * quality / 1000000 by computeUnits; quality = 10^9 breaks it. Added the range hypothesis on qualityScore that the 1000000 divisor normalizes against, and proved it. `canonical_root` was false of an arbitrary AISupply — nothing stops a record from teleporting more than was minted — so the bridge invariant it needs is now stated as `wellFormed`. `low_quality_no_mining` closed at the simp. Compute/Swarm.lean, KMS/Secrets.lean — trailing `omega` after a simp that had already closed the goal. AccessPolicy also needed `deriving Repr`, which SecretMeta's own Repr derivation requires of it. CRDT/Privacy.lean — `seal ` is a Lean command token, so a structure field named `seal` cannot parse. Backend fields take the names the Go interface uses (encrypt / decrypt) and the envelope layer is wrap / unwrap. `wrong_tag` needed the tag inequality in the direction the guard tests it, and both message theorems needed mapM' so the goal did not unfold into List.mapM.loop. Gateway/Auth.lean — checkAuth calls the axiomatized verifyToken, so it has no code to compile: noncomputable. Platform/SBOM.lean — simp had already pushed the negation inward, leaving push_neg nothing to do, and `List.all_cons` left a goal in ∀-form that the Bool-form hypothesis does not close. Three statements compiled while asserting nothing, and now carry a claim: enclave_isolation and attestation_constant_size stated `True`, and derived_key_isolation returned its own hypothesis. Isolation is now non-interference over a host view — two attested tasks differing only in enclave payload look identical from outside — and derived_key_isolation derives the master's confinement from hsm_boundary, which until now no theorem used. lake build exits 0. vacuity.py: 0 vacuous declarations, down from 2, and no theorem rests on sorryAx. Co-authored-by: Hanzo Dev <[email protected]>
79 lines
2.8 KiB
Lean4
79 lines
2.8 KiB
Lean4
/-
|
|
On-Chain Anchor
|
|
|
|
The anchor precompile stores Merkle roots at (app, height).
|
|
Heights are monotonic — once height N is anchored, anything ≤ N
|
|
is rejected. This gives off-chain CRDT state a tamper-evident
|
|
durability backstop: if the root a user computes locally differs
|
|
from the root on-chain, the server's state diverged.
|
|
|
|
Maps to:
|
|
- lux/precompile/anchor/contract.go (Submit, Get, GetLatest)
|
|
- hanzo/base/crdt/anchor.go (Anchorer interface, RPCAnchorer)
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace CRDT.Anchor
|
|
|
|
abbrev App := Nat
|
|
abbrev Height := Nat
|
|
abbrev Root := Nat
|
|
|
|
/-- The on-chain store. `roots` maps (app, height) to the anchored
|
|
Merkle root; `latest` tracks the highest height per app. -/
|
|
structure Store where
|
|
roots : App → Height → Option Root
|
|
latest : App → Height
|
|
|
|
/-- Submit an anchor. Succeeds only when the new height exceeds the
|
|
current latest for that app. This is the monotonicity invariant
|
|
that prevents retroactive root substitution. -/
|
|
def submit (s : Store) (app : App) (h : Height) (root : Root) : Option Store :=
|
|
if h > s.latest app then
|
|
some {
|
|
roots := fun a ht => if a = app ∧ ht = h then some root else s.roots a ht,
|
|
latest := fun a => if a = app then h else s.latest a,
|
|
}
|
|
else none
|
|
|
|
def get (s : Store) (app : App) (h : Height) : Option Root := s.roots app h
|
|
|
|
/-- A successful submit advances the latest height. -/
|
|
theorem submit_bumps (s s' : Store) (app : App) (h : Height) (root : Root)
|
|
(ok : submit s app h root = some s') :
|
|
s'.latest app = h ∧ h > s.latest app := by
|
|
simp [submit] at ok
|
|
obtain ⟨hlt, rfl⟩ := ok
|
|
exact ⟨by simp, hlt⟩
|
|
|
|
/-- Heights at or below the current latest are rejected.
|
|
An attacker cannot rewrite an earlier root without a chain reorg. -/
|
|
theorem old_rejected (s : Store) (app : App) (h : Height) (root : Root)
|
|
(low : h ≤ s.latest app) :
|
|
submit s app h root = none := by
|
|
simp [submit, Nat.not_lt.mpr low]
|
|
|
|
/-- The root is retrievable immediately after submitting it.
|
|
This is the read-your-writes guarantee: a user who submits an
|
|
anchor can verify it was recorded in the same block. -/
|
|
theorem read_after_write (s s' : Store) (app : App) (h : Height) (root : Root)
|
|
(ok : submit s app h root = some s') :
|
|
get s' app h = some root := by
|
|
simp [submit] at ok
|
|
obtain ⟨-, rfl⟩ := ok
|
|
simp [get]
|
|
|
|
/-- Submitting for one app does not affect another app's anchors.
|
|
Each app's data is fully isolated even though they share a
|
|
precompile address. -/
|
|
theorem apps_isolated (s s' : Store) (a₁ a₂ : App) (h₁ h₂ : Height) (root : Root)
|
|
(ne : a₁ ≠ a₂) (ok : submit s a₁ h₁ root = some s') :
|
|
get s' a₂ h₂ = get s a₂ h₂ := by
|
|
simp [submit] at ok
|
|
obtain ⟨-, rfl⟩ := ok
|
|
simp [get, ne, Ne.symm ne]
|
|
|
|
end CRDT.Anchor
|