Certificat ZK #3
Probă: comutativitatea adunării pe Nat — chitanță succintă RISC Zero (program lean_check, RTX 4090)
✅ verificat matematic: chitanța dovedește că nucleul Lean (nanoda, în zkVM) a acceptat o demonstrație
Certificatul nu e legat de o provocare: dovedește că există o demonstrație a enunțurilor de mai jos, iar comparația cu problema o faci tu. Certificatele făcute cu comparatorul sigilat (jurnal v2) dovedesc și că enunțurile sunt exact ale unei provocări.
Enunțuri demonstrate (demonstrațiile rămân secrete)
- Eq.symm
theorem Eq.symm.{u} : forall {α : Sort u} {a b : α}, Eq a b → Eq b a := _ - congrArg
theorem congrArg.{u v} : forall {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), Eq a₁ a₂ → Eq (f a₁) (f a₂) := _ - Nat.zero_add
theorem Nat.zero_add (n : Nat) : Eq (HAdd.hAdd (OfNat.ofNat 0) n) n := _
- Nat.succ_add
theorem Nat.succ_add (n m : Nat) : Eq (HAdd.hAdd (Nat.succ n) m) (Nat.succ (HAdd.hAdd n m)) := _
- Nat.add_comm
theorem Nat.add_comm (n m : Nat) : Eq (HAdd.hAdd n m) (HAdd.hAdd m n) := _
- add_comm'
theorem add_comm' (n m : Nat) : Eq (HAdd.hAdd n m) (HAdd.hAdd m n) := _
- Deținător
- u_XI6mv-HHRwyD
Deținătorul e contul care a postat chitanța. Chitanța în sine nu e încă legată de un cont sau de o tranzacție: dovedește că există o demonstrație, nu cui îi aparține. - Înscris la (UTC)
- 2026-09-17T13:57:40.322020Z
- Id-ul de imagine al programului (lean_check)
- b80838fed027ffe2c75c05c45e46d8f2a3385fcb2ac4564084a732a53a4ef99f
- Politica de axiome (axiomele pe care verificatorul avea voie să le accepte)
- Classical.choice, Lean.trustCompiler, Quot.sound, propext
- ⚠ Politica acestui certificat permite și Lean.trustCompiler, axioma din spatele native_decide: ea presupune corect tot compilatorul Lean, nu doar nucleul. Certificatele noi nu o mai permit.
- SHA-256 al exportului (secret)
- b4279761d83e88a2737beead8ed1bc6d742498310eaeb46f502dab2a8c8c08bd · 53 declarații verificate
- chitanță
- succinct · sha256 9d7abf96499c5c46e9c3a3f3a5aba27220be2b340c5dc87753720fc0b8eb1bc9 · Descarcă chitanța
- Hash-ul intrării
- 4d48736c3bf88e5994e55f5a401f21ea2198ef5ab7d0f05dc13955522a46f33d · #3
Verifică singur
Construiește verificatorul din zk/lean_check/verifier (Rust), apoi rulează-l pe chitanță cu id-ul de imagine. Id-ul de imagine e hash-ul programului fix; oricine reconstruiește zk/lean_check obține același id.
lean_check_verifier receipt.bin b80838fed027ffe2c75c05c45e46d8f2a3385fcb2ac4564084a732a53a4ef99f