break-golf

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

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

الحالة: إثبات مفهوم. الموقع ثابت، والتقديمات تفتح مشكلة على GitHub، وإنسان يتخذ القرار. لا يوجد مُدقِّق Lean خلفه بعد.

البنية

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rewrite the ledger with scores and frontier
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 يعمل عند push و pull request: بوابات --check، وفحص الإعدادات، وفحص الموقع، وسلسلة من التقديمات التي يجب على المُدقِّق قبولها ورفضها — sorry، وnative_decide، وتحدٍّ مجهول، وميزة صفرية، ونص بلا كتلة Lean. workflow_dispatch يتحقق من تقديم واحد عند الطلب دون فتح مشكلة.

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

المُقدِّم لا يكتب البيان أبدًا

هذه هي الآلية كلها، وهي نفسها التي يستخدمها trailofbits/lean-golf في proof golf. المُدقِّق يبني نسخته الخاصة من Challenge.lean. التقديم يوفّر فقط:

def strategy : game.Param → PFunDDS.DDE game.Query game.Response
def verdict  : List (game.Query × Option game.Response) → Bool
theorem attackWins : attack.Wins score.budget score.advantage

بالإضافة إلى budget و advantage في النموذج. attack و score يُجمَّعان من تلك الأرقام في Challenge.lean، لذا لا يمكن لتقديم أن ينفق ميزانية أكبر مما يُسجَّل عليه، أو أن يثبت حدًّا أضعف مما يدّعي — ليس لأننا نتحقق، بل لأنه لا يمسك القلم أبدًا على أيٍّ من الكائنين.

أربعة رفضات يصدرها المُدقِّق دون قراءة أي شيء:

native_decide و maxHeartbeats و maxRecDepth مرفوضة أيضًا: الإثبات الذي لا يُغلق إلا بحد مرتفع هو إثبات لا يستطيع المُدقِّق تحمّله.

احتساب النقاط

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

score = log₂( budget / advantage^e )

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

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

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

الجبهة هي السجل الأساسي: تنضم إليها نتيجة عندما لا يتفوق عليها شيء آخر في الاستعلامات والميزة معًا. نتيجة البت هي العمود المرتَّب بجانبها، وليمّتان مُتحقَّقتان في طبقة Lean (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) تضمنان أن الترتيب لا يدفن أبدًا نتيجة تفوز على المحورين معًا.

التحديات

spoc128 — SpoC-128 كما قُدِّم إلى NIST LWC Round 2. مكسور: ثلاثة استعلامات، ميزة 1، 1.58 بت. load key n يضع nonce في rate وtagInput يدخل tagControl عبر XOR في نفس rate، لذا tagInput (load key n) = load key (n ^^^ tagControl). مدخل تبديل واحد يمكن بلوغه باستعلامين، وبما أن التبديل علني وقابل للعكس، نصفه يتسرب في tag ونصفه في كتلة ciphertext؛ اجمع، اقلب، خذ capacity، وهذا هو المفتاح.

spoc128-ds — نفس الوضع مع حجز بتات التحكم الأربع في nonce، لذا n ^^^ tagControl ليس nonce قانونيًا. مفتوح: لا يوجد هجوم معروف. القيد يعيش في نوع الاستعلام، لذا الهجوم المنشور ليس مجرد غير ناجح هنا — بل لا يمكن تقديمه كخصم أصلًا (SpoC128DS.attack_second_query_illegal).

هذا عمدًا ليس نسخة ثانية من الوضع. تقوية DDC.lean ستعني نموذجًا موازيًا يجب إبقاؤه متزامنًا؛ تقييد نطاق الاستعلام هو مسند واحد، وكل نظرية موجودة عن الوضع ما تزال تنطبق.

لا شيء هنا يدّعي أن النسخة آمنة. إغلاق طريق منشور واحد إلى وضع ليس حجة على عدم وجود طريق آخر — وهذا هو الهدف من طرحه.

إضافة تحدٍّ

وفّر Golf.Game في طبقة Lean — نوع معامل عام، ونوع استعلام واستجابة، والعالَمَين — ثم config.json هنا. الطبقة العامة تعيش في RandomSystems/Golf/Game.lean؛ وRandomSystems/Golf/Instances/SpoC128/ هو المثال العملي، ويعمل أيضًا كفحص على أن التجريد أمين: إيصالات كفايته هي rfl وتقديمه المرجعي يُغلَق بواسطة attack_distinguishing_advantage الموجود دون إعادة صياغة.

ما لا يُسجَّل

• العمل خارج الخط (offline)، بقرار. الخصم كائن رمزي واللوحة تسجّل تعقيد الاستعلام، الإطار المعلوماتي-النظري الذي تعيش فيه indifferentiability و lemma التبديل PRP/PRF أصلًا. التحدي الذي يحتاج جدوى حسابية يجب أن يقول ذلك ويحدد شكلًا يحمل تكلفة.
• التضخيم مُفترَض أنه متاح: q/α^e هو تكلفة تكرار هجوم حتى الثقة.
• التعادلات ليست تكافؤات. نفس مستوى البت يمكن أن يحمل نتائج مختلفة جدًا، ولهذا تجلس الجبهة بجانب الترتيب بدلًا من أن تُستبدل به.