break-golf

لوحة لنتائج التحليل التشفيري التي تكون مُثبتة، لا مُنفَّذة.

التحدي يحدد عالمين والعبارة التي يجب عليك إثباتها. تكتب خصمًا وإثباتًا على أنه يميز بينهما. الفوز هو الإثبات: لا شيء يُنفَّذ، أو يُعاين، أو يُعاد تشغيله، ولا يقرأ أي إنسان الطلب ليقرر ما إذا كان يُحتسب.

الحالة: المدقق يعمل. تُفصَّل مسألة verify: في CI وفق النوع المثبَّت للتحدي وتُدقَّق باستخدام #print axioms؛ وتعود النتيجة كتعليق. لا تزال السجلات تُضاف إلى scoring/ledger.json يدويًا.

هذا مشروع Lake مستقل. يأخذ الرياضيات كاعتمادية git مثبَّتة على مراجعة محددة، بحيث تتحقق اللوحة وفق عبارة ثابتة للنمط:

require RandomSystems from git
  "https://github.com/MarcIlunga/random-systems.git" @ "08aec7a7"

وقت البناء هو ذاكرة تخزين مؤقت، وليس مشكلة: تأتي ملفات oleans الخاصة بـ Mathlib من شبكة CDN الخاصة بها عبر lake exe cache get، وتقع ملفات oleans الخاصة بالإصدار المثبّت والتحدي بحجم ~400 ميغابايت في ذاكرة التخزين المؤقت لـ Actions مفهرسةً على البيان ومصادرنا الخاصة.

التخطيط

المسار	ما هو
challenges/<name>/Challenge.lean	موثوق. يثبّت الأنواع الدقيقة التي يجب أن يحتويها أي إرسال. ليس جزءًا من أي رفع.
challenges/<name>/Cost.lean	يُنشئه النظام الأساسي لكل إرسال من أرقام النموذج.
challenges/<name>/config.json	التقييم، والمعيار، والبديهيات المسموح بها، والمهلة الزمنية. الملف الوحيد الذي تعدّله لإضافة تحدٍّ.
challenges/<name>/Solve.template.lean	الهيكل الذي يملؤه المُرسِل.
tools/manifest.py	يستخرج docs/data/manifest.json من challenges/.
tools/ledger.py	يستخرج docs/data/ledger.json من scoring/ledger.json، مع تقييم السجلات وترتيبها.
tools/record.py	يضيف إرسالًا موثّقًا إلى السجل. يرفض أي شيء غير proved.
tools/verify.py	يوثّق إرسالًا واحدًا: معرّف التحدي كـ argv[1]، والمحتوى على stdin، والحكم بصيغة JSON على stdout. نفس واجهة lean-golf.
tools/lint_challenges.py	كل إعداد تحدٍّ يحمل ما تحتاجه اللوحة والمدقّق.
tools/check_site.py	يمكن للموقع الثابت تحميل بياناته المُنشأة وعرضها.
scoring/ledger.json	مجموعة السجلات.
docs/	موقع GitHub Pages. ثابت؛ يقرأ الملفين المُنشأين فقط.
examples/	عناصر اختبار: إرسال يُوثّق ولا يفوز بشيء، وتوأمه المبالغ في الادعاء.

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rescore and sort the records
python3 tools/lint_challenges.py   # configs are complete
python3 tools/check_site.py        # the site can render what the tools generate

printf '%s' "$BODY" | python3 tools/verify.py spoc128    # one submission

CI

يعمل verify.yml عند الدفع وطلبات السحب: بوابات --check، وفحص الإعدادات، وفحص الموقع، ومجموعة من الطلبات التي يجب أن يقبلها المدقّق ويرفضها — وهي sorry، وnative_decide، وتحدٍّ غير معروف، وميزة صفرية، ونص بلا كتلة Lean. ويتحقق workflow_dispatch من طلب واحد عند الطلب دون فتح issue.

يعالج submission.yml issue من نوع verify: في وظيفتين. الأولى تحلّل مدخلات غير موثوقة ولا تملك أي صلاحيات كتابة؛ والثانية تنزّل حكمها وتنشر التعليق. هذا التقسيم مأخوذ من lean-golf وهو السبب في أن نص الـ issue لا يمكنه الوصول إلى token.

المُرسِل لا يكتب العبارة أبدًا

الطلب هو تعريف واحد يسكن نوعًا يثبّته التحدي:

-- Challenge.lean, trusted. The verifier builds its own copy.
def score : Golf.Score := ⟨budget, advNum, advDen⟩   -- from the submission form

structure Solution where
  strategy : game.Param → PFunDDS.DDE game.Query game.Response
  verdict  : List (game.Query × Option game.Response) → Bool
  wins     : Golf.Attack.Wins (G := game) ⟨strategy, verdict⟩ score.budget score.advantage

-- Solve.lean, the upload.
def solution : Challenge.SpoC128.Solution where
  strategy := …
  verdict  := …
  wins     := …

بنية واحدة بدلًا من ثلاثة أسماء منفصلة، لأن الأسماء المنفصلة تتعارض: ملف Solve.lean يستورد ملف Challenge.lean الذي يعلن بالفعل strategy/verdict/attackWins يفشل بخطأ "has already been declared". جعل التسليم قيمةً من نوع موثوق يزيل التعارض ويختزل فحص النوع لدى المدقّق إلى #check واحدة.

لماذا يُعدّ اختيار المُقدِّم للنتيجة آمنًا

يجب أن يتحقق أمران، ولا يُؤخذ أيٌّ منهما على الثقة.

الأرقام جزء من القضية. تكتبها المنصة في Cost.lean، ويبني Challenge.lean قيمة score منها، وتظهر score داخل نوع Solution.wins. تغيير رقم يغيّر ما يجب إثباته.

يجب أن يسكن التسليم في نوعنا. تستورد خطوة التدقيق التحدي الموثوق إلى جانب التسليم وتُوسِّع

example : Challenge.SpoC128.Solution := Solution.SpoC128.solution

إذن، تقديم يعلن عن Challenge.SpoC128.Solution الخاص به يتعارض مع الخاص بنا، وأي تقديم يستخدم أي نوع آخر يفشل في فحص الأنواع. بدون هذه الخطوة، يمكن لتقديم لا يستورد التحدي أبدًا أن يعرّف بنية تافهة بالاسم نفسه ويُثبت عند 0 بت — كانت تلك الثغرة حقيقية، والهجومان الآن حالتان في CI.

عدد الاستعلامات لا يحتاج إلى إثبات منفصل. فهو ليس ادعاءً عن خصم مكتمل؛ بل هو وسيط مُنشئ. Attack.distinguisher q هو DDD.ofDDE strategy q verdict، مقطوعًا عند q بحكم البناء، و Attack.silent_past يثبت أنه لا يصدر شيئًا يتجاوزه. لا توجد طريقة لتجاوز الميزانية، لذا لا يوجد شيء يجب فحصه.

budget وadvNum وadvDen تأتي من نموذج التقديم، وهي غير موثوقة. لكنها لا تحتاج إلى أن تكون كذلك: تستبدلها المنصة في Cost.lean، ويبني Challenge.lean قيمة score منها، وتظهر score داخل Solution.wins. لذلك فإن الأرقام جزء من القضية، وليست ادعاءً عنها.

مفحوصة مقابل هجوم SpoC-128 الحقيقي:

الادعاء	النتيجة
budget = 3، الأفضلية 1	يُترجم — الادعاء الصادق
budget = 1، الأفضلية 1	يفشل — Wins 1 1 مبرهنة مختلفة وأقوى
budget = 3، الأفضلية 2	يفشل — لا شيء يمكن أن يتجاوز الأفضلية 1

ولا يوجد حافز للتقليل من الشأن: score = log₂(budget / advantage^e)، لذا فإن أفضلية مُدّعاة أصغر أو ميزانية مُدّعاة أكبر ترفع النتيجة. كلا الاتجاهين أسوأ. الحركة الوحيدة هي الادعاء الأضيق الذي يمكنك إثباته فعليًا.

أربعة رفضات أخرى يقوم بها المدقق دون قراءة أي شيء:

الحيلة	الحكم
إضعاف الادعاء	عدم تطابق النوع مقابل Solution المثبتة
إضافة فرضية ملائمة	نفسه
استخدام sorry في الإثبات	sorryAx ليس في permitted_axioms
native_decide / رفع maxHeartbeats	مرفوض مباشرة

التقييم

لا شيء محدد مسبقًا. في مخطط لم يدرسه أحد، ما الأفضلية القابلة للوصول وبأي تكلفة هو السؤال البحثي، لذا فإن أي هدف هو تخمين — والهدف المحدد عاليًا جدًا يعطي مميزًا حقيقيًا بقيمة 2⁻³⁰ درجة صفر. بدلًا من ذلك، تقيس اللوحة النتيجة:

score = log₂( budget / advantage^e )

الاستعلامات لكل وحدة ميزة؛ لوغاريتمها للأساس اثنين هو مستوى الأمان بالبتات الذي يدحضه الهجوم. الأقل أفضل. التقليل من ميزتك يرفع النتيجة، لذا لا شيء تكسبه بالادعاء بأقل مما تستطيع إثباته.

e خاص بكل تحدٍّ وليس له قيمة افتراضية. e = 2 للعبة قرار — الميزة α تحتاج إلى نحو α⁻² تكرار للتضخيم — وe = 1 للعبة ذات طابع بحثي. كلا الاصطلاحين موجود في الأدبيات والتناقض معروف (Micciancio–Walter، On the Bit Security of Cryptographic Primitives)، لذا يذكر كل تحدٍّ أيّهما يستخدم.

المستوى المرجعي (Par) هو ادعاء المصمم نفسه، مأخوذ من المواصفة، لذا لا يظهر أي تخمين حول صعوبة الهجوم في أي مكان. ما دون المستوى المرجعي هو كسر للادعاء.

تُدرج السجلات بأفضل نتيجة أولاً. هذا هو الترتيب بأكمله.