TheReefink

مجموعة بحث من الهواة لامتدادات حتمية مُثبَتة آليًا لمساعدات الذكاء الاصطناعي المحلية · Ghillie، المخلب نفسه →

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

القواعد الثلاث

1. لا شيء يطلب الثقة. يجب أن يكون كل ادّعاء يعتمد عليه عضو قابلًا لإعادة الاشتقاق: برهان، أو مجموع تحقق، أو جدول حقيقة. عبارة “القائم على الصيانة يقول ذلك” ليست فئة نستخدمها.
2. الرفض نتيجة. برهان يفشل في الإبراء، ومخزن لا يمكن قراءته، وثغرة تُسجَّل بصدق — هذه كلها النظام وهو يعمل، وتُدوَّن دائمًا، ولا تُموَّه أبدًا. التقرير المملّ — فعل تمامًا ما قالته نظرياته، مرة أخرى — نتيجة أيضًا.
3. صاحب الجهاز أعلى رتبة من المخلب، دائمًا. الامتدادات تقرر؛ ولا تكتسب سلطة أبدًا. لا يغيّر أي تجريب ذلك، مهما أثبت.

كن جزءًا منها — أعد اشتقاق برهانك الأول اليوم

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

1. احصل على أداة الإثبات. سلسلة أدوات GNAT FSF المجانية — تحمل مُثبِت SPARK وأيضًا أدوات البناء في حزمة واحدة:

https://github.com/alire-project/GNAT-FSF-builds/releases
  (gnatprove-x86_64-linux, -darwin, or -windows64 — unpack anywhere)

هذه الحزمة وحدها تكفي للخطوة 3، إعادة اشتقاق البرهان. لكنها لا تكفي للخطوة 4، بناء الواجهة: فهي تحمل gcc و ld لكن بلا بيئة تشغيل C ولا كائنات بدء تشغيل، فعلى جهاز يفتقر إليها يفشل البناء بعد أن يكون البرهان قد أُبرئ بالفعل — أسوأ لحظة ممكنة لاكتشاف نقص في جزء. تحتاج أيضًا إلى binutils و libc6-dev. هذه هي أساسيات البناء المعتادة في أي نظام لينكس، موجودة أصلًا على أي جهاز يكاد يُستخدم للتطوير؛ والحاوية الخالية أو التثبيت الأدنى الطازج هما ما يفتقران إليها. على Debian و Ubuntu:

sudo apt-get install binutils libc6-dev
# Fedora/RHEL: the equivalents are binutils and glibc-devel

2. احصل على الامتداد التمهيدي. نواة قرار حقيقية — سياسة brief-fill، التي تقرر متى يجوز للمساعد أن يجيب نيابة عن صاحبه — تصل كشيفرة مصدرية مع برهانها وجدول حقيقتها الكامل:

3. أعد اشتقاق البرهان. من الحزمة بعد فكها:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2
# success: "0 unproved" — four named theorems, discharged on YOUR machine:
#   NEVER-FILLED-WITHOUT-A-LICENSING-RULE
#   AN-ABSENT-STORE-NEVER-LETS-A-FILL-THROUGH
#   NOTHING-INVENTED-EVER
#   NOTHING-ASKED-THAT-A-RULE-ALREADY-ANSWERS

4. حاول كسره. عدّل الشيفرة المصدرية بحيث يسمح مخزن قواعد غائب بمرور إجابة، ثم شغّل أداة الإثبات مرة أخرى. سترفض — وتسمّي بالضبط النظرية التي خنتها. ذلك الرفض هو نموذج الأمان بأكمله، وقد شاهدته للتو يعمل دون أن تثق بأحد. ثم ابنِ الواجهة وتحقق من كل صف في جدول الحقيقة المشحون معها (core/REPROVE.md في الحزمة يرشدك خطوة بخطوة).

الهدف

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

لماذا سُمِّي العمل Wu

وحدة العمل في المصنع — قاعدة واحدة مُثبَتة، مصوغة من جملة عادية — تُسمّى Wu، تيمنًا بـ Chien-Shiung Wu.

في عام 1956، طرح Chen-Ning Yang و Tsung-Dao Lee سؤالًا عظيمًا — هل تميّز الطبيعة بين اليسار واليمين؟ — ظنّ الجميع تقريبًا أنه لا يستحق أن يُطرَح. كانت تجربة Wu — تصميمها، وجهازها، وقياسها — هي التي أجابت عنه. ذهبت جائزة نوبل، في العام التالي، إلى المنظّرَين وحدهما. استحق السؤال جائزته؛ واستحقت الإجابة جائزتها أيضًا، لكن الإجابة أُسقِطت.

يعيش نصفا تلك القصة هنا. السؤال الجريء، المطروح بوضوح، هو من حيث تبدأ كل قطعة من عملنا — نكرّم Yang، ونحتذي به. لكننا نسمّي وحدة العمل تيمنًا بـ Wu، لأن البرهان هو العمل: لا الفكرة، ولا الإعلان — بل النتيجة المُبرهَنة القابلة للتحقق. ونسمّيها باسمها علنًا لأننا نعرف كم يسهل محو من يقوم بالبرهنة، ولن يحدث ذلك هنا.

ما هو قادم

• الطرفية — المخلب الذي تخدمه هذه الامتدادات: مساعد محلي بلا أي مستمع (listener) وبلا مسار وارد (يستطلع إلى الخارج فقط؛ لا شيء يصل إلى الداخل)، والقرارات المهمة كل واحد منها خلف نواة مُثبَتة. مفتوح المصدر (AGPL-3.0) — صدر بالفعل: الشيفرة المصدرية والملفات التنفيذية على github.com/the-dark-factory/Ghillie_AGPL. تحقق من الملفات التنفيذية قبل تشغيلها: يحمل الإصدار SHA256SUMS-assets.txt، الذي يغطي الحزم المضغوطة تمامًا كما نُزِّلت، لذا فإن sha256sum -c SHA256SUMS-assets.txt يتحقق منها كما هي. (لا يزال SHA256SUMS الأقدم موجودًا لمن استشهد به؛ فهو يسرد مجاميع تحقق الملفات التنفيذية بعد فكّها بصيغة مسبوقة باسم المنصة لا يستطيع sha256sum -c قراءتها.)
• الكتالوج فعّال الآن — يثبّت ghillie قيد التشغيل امتدادات تعيد إثبات نفسها على جهازه هو: ghillie -catalogue https://thereef.ink/catalogue -abilities-available، ثم -get-ability <name> -reprove. لا شيء يُثبَّت ما لم يُبرَأ برهانه على عتادك أولًا.
• الكتالوج — مزيد من الامتدادات القابلة لإعادة الإثبات على الشكل نفسه: ساعات الصمت، وأسقف الإنفاق، ومنح التواصل، وقاعدة الفم (لا تُعاد صياغة الرفض أبدًا)، ولكل منها نظرياتها المسمّاة.
• التعاونية — سجلات ثغرات مشتركة، بحيث تصبح نقطة عمياء سجّلها مخلب واحد بصيرةً لكل مخلب، وعمل إثبات مُجمَّع: الإثبات هو عبء العمل الوحيد الذي يمكنك قبوله بأمان من غرباء، لأن الإبراء إما يُعاد اشتقاقه أو لا يُعاد.

التقارير

أجريت البرهان؟ كسرت شيئًا بأدب؟ وجدت النتيجة المملّة؟ اكتب إلى tonythegair@gmail.com. تُنشَر النتائج؛ ولا يُطلَب منك شيء آخر عنك — هذه الصفحة بلا سكربتات، ولا كعكات، ولا تحليلات، ويمكنك التحقق من ذلك بقراءتها. لكن الجهاز الذي يسلّمك الصفحة يحتفظ بسطر قصير مقتَطع لكل طلب، ونقول ذلك بصراحة: ما يسجّله الخادم.

الرعاية

ترعى The Dark Factory Ltd TheReefink، وقد كرّست موارد كبيرة لنجاحها — آلية الإثبات، والامتدادات الأولى، والطرفية القادمة. لا تشتري الرعاية أي استثناءات: كل ما يشحنه الراعي هنا قابل للتحقق بالقاعدة نفسها التي يخضع لها كل شيء آخر، ومن كسره من الأعضاء بأدب يكون قد قدّم خدمة للمجموعة.