رحلة المستخدم من
tx hashإلى.evmxproof، مكتوبة كأهداف قابلة للتحقق. كل مرحلة لها: مدخل محدد، مخرج محدد، شرط فشل صريح، ما لا تفعله.
evmx version # هوية الأداة + المحرك + canon_version
evmx tx <TX_HASH> # v0.1
evmx trace <TX_HASH> # v0.1
evmx diff <TX_HASH> # v0.3
evmx detect <TX_HASH> # v0.4 → PATTERN_CANDIDATE | NO_FINDING
evmx prove <TX_HASH> # v0.5 → .evmxproof
evmx verify <FILE.evmxproof> # v0.5
evmx fixture <record|list|check> # أدوات الـregistry (08)
قواعد ملزمة على المخرجات (D-15):
| القناة | المحتوى |
|---|---|
stdout |
نتيجة الأمر فقط. --format human (افتراضي) أو --format json |
stderr |
كل الـlogs بلا استثناء |
| exit code | 0 نجاح · 1 فشل منطقي (لا finding / verify فشل) · 2 خطأ استخدام · 3 خطأ شبكة/مزوّد · 4 خطأ داخلي |
evmx verify لا يكتب أي ملف ولا يفتح أي اتصال شبكة في الوضع الافتراضي.
┌──────────────────────────────────────┐
TX_HASH ───────────►│ STAGE 1 — ACQUISITION (evmx-rpc) │
└───────────────┬──────────────────────┘
│ RawSource[] (bytes + raw_hash)
┌───────────────▼──────────────────────┐
│ STAGE 2 — STRUCTURING (evmx-trace) │
└───────────────┬──────────────────────┘
│ ExecutionTree (+ AccessTimeline من v0.4)
┌───────────────▼──────────────────────┐
│ STAGE 3 — STATE (evmx-state) │
└───────────────┬──────────────────────┘
│ StateDiff + StateEvidence[]
┌───────────────▼──────────────────────┐
│ STAGE 4 — DETECTION (evmx-detectors)│
└───────────────┬──────────────────────┘
│ Claim + Evidence[] → PATTERN_CANDIDATE
┌───────────────▼──────────────────────┐
│ STAGE 5 — PROOF (evmx-proof) │
│ Witness → Replay → Compare │
└───────────────┬──────────────────────┘
│ Reproduction + Verification
┌───────────────▼──────────────────────┐
│ STAGE 6 — ARTIFACT (evmx-proof) │
└───────────────┬──────────────────────┘
│ .evmxproof (canonical bytes)
┌───────────────▼──────────────────────┐
│ STAGE 7 — VERIFY (evmx-proof) │
└──────────────────────────────────────┘
المدخل: tx_hash (0x + 64 hex، يُتحقق شكليًا قبل أي شبكة).
الاستدعاءات:
| # | الاستدعاء | متى |
|---|---|---|
| A1 | eth_getTransactionByHash |
دائمًا |
| A2 | eth_getTransactionReceipt |
دائمًا |
| A3 | eth_getBlockByNumber(blockNumber, false) |
دائمًا — نحتاج header للـenvelope |
| A4 | debug_traceTransaction(hash, {tracer:"callTracer", withLog:true}) |
من v0.1 |
| A5 | debug_traceTransaction(hash, {tracer:"prestateTracer", diffMode:true}) |
من v0.3 |
| A6 | debug_traceTransaction(hash, {disableMemory:true, ...}) — struct logs |
v0.4، بحد خطوات |
| A7 | eth_getStorageAt / eth_getBalance / eth_getTransactionCount عند N-1 وN |
v0.3 — cross-check |
| A8 | web3_clientVersion |
v0.5 |
| A9 | eth_getProof |
v0.5 — توثيق الـwitness |
المخرج: Vec<RawSource> حيث كل عنصر:
RawSource {
id: "S1".."Sn",
method, params_canonical,
bytes: Vec<u8>, // البايتات كما وصلت من الـtransport، بدون أي معالجة
raw_hash: B256, // keccak256(bytes) ← D-11
client: Option<String>, // من A8
provider_fingerprint: B256, // keccak256(host) — لا URL ولا مفتاح أبدًا
}
شروط الفشل الصريحة:
- المعاملة غير موجودة أو
blockNumber == null(pending) →E_TX_NOT_MINED، خروج1. - المزوّد لا يدعم
debug_*→E_PROVIDER_CAPABILITY، خروج3، مع ذكر البند الفاشل من checklist 01 §5. - استجابة أكبر من الحد المسموح →
E_RESPONSE_TOO_LARGE، خروج3. لا نحاول تحميلها في الذاكرة.
ما لا تفعله هذه المرحلة: لا تفسير، لا decode، لا استنتاج. مجرد جلب وتوثيق.
المدخل: RawSource الخاصة بـA4 (+ A6 من v0.4).
المخرج 1 — ExecutionTree: شجرة الـframes بترتيب التنفيذ (تفاصيل النموذج في 03 §4).
المخرج 2 — AccessTimeline (من v0.4): سلسلة مرتبة زمنيًا من الأحداث:
[ (seq, frame_id, kind, target) ]
kind ∈ { CALL_ENTER, CALL_EXIT, SLOAD, SSTORE, LOG, CREATE, SELFDESTRUCT }
هذه أهم بنية في المشروع. الـStage 4 كلها تعمل عليها. راجع RISK-01 في
PROJECT_MAP— الـtimeline لا يمكن اشتقاقه منcallTracerولا منprestateTracer؛ يحتاج producer منفصل.
الأهداف القابلة للتحقق:
- كل frame في الاستجابة الخام له عقدة واحدة في الشجرة، بنفس العدد والترتيب.
sum(children.gas_used) <= parent.gas_usedلكل عقدة غير جذرية.
تصحيح (2026-08-14، من بيانات mainnet حقيقية). الصيغة الأولى كانت «لكل عقدة» بلا استثناء، وهي خاطئة. في fixture
0003مجموع غاز أبناء الجذر = 425,827 بينما الجذر = 400,850 — الأبناء أكبر بـ24,977. الملاحظ (مُتحقَّق منه):root.gasUsed == receipt.gasUsedفي الـfixtures الثلاث، والانتهاك في الجذر حصرًا — كل العقد غير الجذرية تحقق الشرط. الفرضية (غير مُتحقَّق منها): الجذر يبلّغ محاسبة على مستوى المعاملة كاملة، وقد يدخل فيها ردّ الغاز والمحاسبة الابتدائية، بينما الأبناء يبلّغون استهلاكهم الخام. التفسير السببي لم يُثبَت، ولا يُبنى عليه منطق. المُلزِم هو الاستثناء الملاحَظ، لا سببه.لو بقي الشرط على صيغته الأولى كمعيار قبول، لكان أول ما يفعله المطوّر هو «إصلاح» parser سليم أو استبعاد fixture صحيحة من mainnet. هذه بالضبط فئة الأخطاء التي تُكتشف بالبيانات لا بالتفكير.
- إعادة بناء
ExecutionTreeمن نفسRawSourceتعطي شجرة متطابقة بايت-ببايت بعد الـcanonicalization.
فك الأسماء (v0.2): selector → signature من القاموس المحلي فقط.
النتيجة تُوسَم UNTRUSTED_LABEL وتظهر في العرض البشري فقط. ممنوع أن تدخل في أي evidence أو verdict (07 INV-6).
المدخل: A5 + A7 + الشجرة.
المخرج: StateDiff + قائمة StateEvidence، وكل عنصر يحمل مصدره:
StateEvidence {
target: Account(addr) | Storage(addr, slot) | Nonce(addr) | Balance(addr),
before, after,
source: RpcDerived | TraceDerived | ReplayDerived,
derivation: String, // كيف اشتُقّت بالضبط، مرجّعة لـ RawSource.id
}
| ما نريد إثباته | المصدر صاحب السلطة | السبب |
|---|---|---|
| قيمة storage/balance/nonce قبل وبعد | ReplayDerived ← ثم RpcDerived ← ثم TraceDerived |
الـreplay يعيد الاشتقاق من witness موثّق؛ الـRPC مقروء مباشرة؛ الـtracer تفسير للclient |
| ترتيب العمليات وتداخل الـframes | TraceDerived (AccessTimeline) وحده |
لا الـRPC ولا الـdiff يحملان زمنًا |
| حدوث/فشل call | TraceDerived |
مباشرة من الـtracer |
| تحويلات ERC-20 | TraceDerived + وسم UNTRUSTED_INTERPRETATION |
مطابقة Transfer topic ليست ضمانًا للسلوك |
ReplayDerivedغير مبنيّ حتى v0.5 (D-45): مدخلهrevm، وقِيس أن 7 من 17 مصدر شفرة نُفِّذت غائبة عن الأدلة. فالمبنيّ فيv0.3-bدرجتان من ثلاث —RpcDerivedفوقTraceDerived— ولا يُوصَف السلّم بالاكتمال قبل v0.5 (D-52).
قاعدة التعارض: لو مصدران أعطيا قيمتين مختلفتين لنفس الهدف → لا نختار. نُصدر EVIDENCE_CONFLICT، والـverdict النهائي INCONCLUSIVE. التعارض نفسه يُسجَّل في الـartifact كدليل.
الأهداف القابلة للتحقق:
-
لكل slot في
prestateTracer.pre، القيمة تطابقeth_getStorageAt(addr, slot, N−1).مصحَّح (
H-a·D-48). كان: «لكل slot فيpost… عند N». وهو يشترط مستحيلًا:getStorageAtعند N يعطي حالة نهاية البلوك، وpostيعطي الحالة بعد معاملتنا مباشرةً — وبينهما كل المعاملات التالية.ومقارنة
postلا تُسقَط بل تُقيَّد: تصحّ حين تكون معاملتنا آخر من يمسّ الـslot في بلوكها، وهو شرط يُفحَص لا يُفترض.وشرط صحة المقارنة الجديدة يُفحَص كذلك لكل (دليل، slot) بمسح المعاملات الأسبق، ولا يُعمَّم (
D-49). -
تغيّر الـbalance =
post - preيساوي المحسوب من قيم الـframes + رسوم الغاز + مكافآت الـcoinbase، أو يُعلَّمUNEXPLAINED_DELTAصراحة. -
الـnonce للـsender يزيد 1 بالضبط.
المدخل: ExecutionTree + AccessTimeline + StateDiff. لا شبكة، لا ملفات.
المخرج: Option<Claim> + Vec<Evidence>.
نمط reentrancy.classic مُعرَّف على الـtimeline كالآتي (النص الكامل في 03 §6):
∃ slot S, frame F_outer, F_inner :
F_inner ينتمي لسلالة F_outer
∧ address(F_inner) == address(F_outer) ∧ selector مطابق
∧ ∃ CALL خارجي C بين دخول F_outer ودخول F_inner
∧ SLOAD(S) قبل C داخل F_outer
∧ SSTORE(S) بعد خروج C داخل F_outer
∧ F_inner يقرأ S قبل أن يُكتب
المخرج دائمًا PATTERN_CANDIDATE. ممنوع على أي detector إصدار verdict أقوى. الترقية تحدث في Stage 5 فقط.
Claim + Evidence
│
▼
[1] بناء الـWitness ← القيم الدقيقة المقروءة عند block N-1 (accounts, storage, block hashes)
│
▼
[2] بناء الـEnvironment ← chain_id, block header كامل, hardfork, tx env (05 §5)
│
▼
[3] Replay (revm) ← تنفيذ من الـwitness فقط، بدون شبكة
│
▼
[4] Compare ← observed مقابل expected المشتق من الـclaim
│
▼
[5] Determinism check ← تشغيل [3] مرتين ⇒ نفس result_hash
│
▼
Reproduction { class, observed, expected, result_hash }
class = FAITHFULلو لم يُعدَّل أي شيء عن الحالة التاريخية.class = SYNTHETICلو استُخدم أي override (غاز، قيمة، حالة).SYNTHETICلا يمكن أن يصل لـPROOF_VERIFIEDفي v0.5.
Cross-check (v0.5، يصبح INV-8): الـAccessTimeline المستخرج من الـreplay يجب أن يطابق المستخرج من struct logs. عدم التطابق ⇒ INCONCLUSIVE(TIMELINE_MISMATCH) — وده في حد ذاته اكتشاف يستحق التسجيل.
يُبنى المستند، يُحوَّل لصيغته الـcanonical (05 §3–4)، يُحسب proof_id، ثم يُكتب.
الكتابة ذرية: ملف مؤقت ثم rename. لا ملف نصف مكتوب أبدًا.
evmx verify proof.evmxproof
- الافتراضي: offline strict. كل الفحوص التي لا تحتاج شبكة تعمل من الـwitness المضمّن.
--online: يضيف الفحوص التي تقارن بالشبكة (V2, V5).- الفحوص V1..V8 ومعنى كل ✓ بالضبط:
05 §7.
قاعدة العرض: الـverifier يطبع دائمًا جملة النطاق المرتبطة بـverdict.semantics، حتى لو كل الفحوص نجحت. ممنوع طباعة VALID مجردة بدون النطاق.
| المرحلة | تظهر في | يثبتها |
|---|---|---|
| Acquisition | v0.1 | fixtures مسجّلة + wiremock لسلوك الأخطاء |
| Structuring (شجرة) | v0.1/v0.2 | insta snapshots على 3 معاملات مرجعية |
| AccessTimeline | v0.4 | مقارنة مع timeline مرجعي محفوظ في الـfixture |
| State | v0.3 | تطابق ثلاثي المصادر على كل fixture |
| Detection | v0.4 | مصفوفة positive/negative (06 §5) |
| Proof | v0.5 | تشغيلان ⇒ نفس result_hash |
| Verify | v0.5 | proofs مُعطوبة عمدًا في الـregistry يجب أن تفشل بالفحص الصحيح |