‏SR9 قراردادهای کنیستر را به مرز اثبات تبدیل می‌کند؛ به‌ویژه در وضعیت‌های ناهمگام

پروژه‌ای تازه به نام SR9 که اکنون در مستندات با نام Sector9 معرفی می‌شود، قراردادهای صوری را به کد منبع کنیستر نزدیک می‌کند. ایده اصلی ساده است: نوع‌ها مشخص می‌کنند مقدارها چه شکلی می‌توانند داشته باشند، اما راستی‌آزمایی مشخص می‌کند یک انتقال وضعیت چه کاری مجاز است انجام دهد.

یک تابع می‌تواند بندهای requires، ensures، reads و modifies داشته باشد. یک actor نیز می‌تواند ناوردایی‌هایی تعریف کند که هر انتقال عمومیِ راستی‌آزایی‌شده باید حفظشان کند. در نمونه برداشت وجه، راستی‌آزما می‌تواند تفریق بدون قید روی Nat را با ارائه یک مثال نقض رد کند؛ مثلاً زمانی که مقدار برداشت از موجودی بیشتر است. افزودن نگهبان ورودی و پیش‌شرط منطقی متناظر، مرز گمشده را صریح می‌کند.

این تفکیک مهم است، چون SR9 میان فراخواننده بیرونی و فراخواننده راستی‌آزایی‌شده تفاوت می‌گذارد. entry_requires نگهبان زمان اجرا برای پیام‌های ورودی به کنیستر است؛ requires تعهد اثباتی برای کدی است که تابع را فراخوانی می‌کند. مستندات پروژه می‌گویند یک متد عمومی نمی‌تواند بدون نگهبان ورودی مناسب، از راستی‌آزما بخواهد واقعیت‌های تحت‌کنترل فراخواننده را فرض کند.

هدف مهم‌تر، وضعیت ناهمگام است. در یک await که اجرای کد را معلق می‌کند، پیام‌های دیگر ممکن است پیش از ادامه اجرا شوند. بنابراین مدل راستی‌آزمایی SR9 این مرز را نقطه‌ای برای تداخل احتمالی می‌داند و از اثبات می‌خواهد واقعیت‌های مورد اتکا را دوباره برقرار کند. دامنه اثر وضعیت، ناوردایی‌ها، قراردادهای صریح و محدودیت‌های aliasing قرار است این فرض‌ها را آشکار کنند، نه اینکه در بازبینی دستی کد پنهان بمانند.

زنجیره‌ابزار همچنین داده‌های مربوط به اثبات را از رفتار مستقرشده جدا می‌کند. مستندات توضیح می‌دهند که اعلان‌ها و assertionهای صرفاً اثباتی هنگام projection زمان اجرا حذف می‌شوند، در حالی که برای کنترل دفاعی واقعی می‌توان از assertion زمان اجرا استفاده کرد. کامپایل به WebAssembly و راستی‌آزمایی صوری فرمان‌های جداگانه‌اند؛ ساخت باینری لزوماً فرایند راستی‌آزمایی مبتنی بر SMT را اجرا نمی‌کند.

این مدل می‌تواند چرخه‌ای مفید برای توسعه با کمک هوش مصنوعی بسازد: agent یک کنیستر می‌نویسد، راستی‌آزما تعهد ناموفق یا مثال نقض برمی‌گرداند و agent قرارداد یا پیاده‌سازی را اصلاح می‌کند. نتیجه، اطمینانی نیست که از متن قانع‌کننده به دست آمده باشد؛ بلکه بررسی ویژگی‌هایی است که واقعاً نوشته شده‌اند.

محدودیت هم به همان اندازه مهم است. SR9 جایگزین مستقیم هر برنامه موتوکو نیست. زیرمجموعه راستی‌آزایی‌شده طبق مستندات به خلاصه‌سازی صریح اثرات، حساب صحیح بررسی‌شده، محدودیت برای await و futureهای بدون انتظار، و قواعد محتاطانه درباره aliasing قابل‌تغییر نیاز دارد. حلقه‌ها ممکن است به invariant نیاز داشته باشند، توابع import‌شده باید قراردادهای قابل‌استفاده داشته باشند و برخی الگوها ممکن است رد شوند، حتی اگر موتوکو معمولی آن‌ها را بپذیرد.

اعلامیه ماه مه در انجمن، SR9 را یک نسخه آلفا معرفی می‌کند و می‌گوید از یک کانتینر Docker اجرا می‌شود. همان اعلامیه می‌گوید لایه راستی‌آزمایی هنگام کامپایل حذف می‌شود و وارد Wasm نمی‌شود. همچنین از یک سرویس راستی‌آزمایی تحت حاکمیت Neutrinite سخن می‌گوید، اما این سرویس یک جهت طراحی پروژه است، نه مدرکی که نشان دهد همه کنیسترهای ICP به‌طور خودکار گواهی می‌شوند.

برای سازندگان ICP، داستان فوری نه یک runtime جدید است و نه تضمین ایمنی همگانی. موضوع، یک مرز توسعه تازه است: قواعد پروتکل می‌توانند کنار کد actor شبیه موتوکو نوشته شوند، در تغییرات وضعیت و لبه‌های ناهمگام بررسی شوند و وارد گردش‌کاری شوند که برای اصلاح ماشینی طراحی شده است. عملی‌شدن این مرز در مقیاس تولید به پوشش راستی‌آزما، کیفیت قراردادها و میزان بازآرایی لازم برای کنیسترهای واقعی بستگی دارد.