Triết lý Kiến trúc: Thiết kế Ưu tiên Quy tắc (Rule-First Design)

Triết lý Kiến trúc: Thiết kế Ưu tiên Quy tắc (Rule-First Design)

Khi xây dựng một động cơ để xác minh mã nguồn do AI viết ra, các kiến trúc sư phải đối mặt với một tình thế khó xử. Các quy tắc nên nằm ở đâu, và ai sẽ thực thi chúng? Câu trả lời của Axiom rất đơn giản: Quy tắc phải đi trước mã code.

Nguyên tắc Ưu tiên Quy tắc (Rule-First)

Phát triển phần mềm truyền thống thường diễn ra theo quy trình: viết code, chạy test để bắt lỗi, thêm quy tắc để ngăn chặn lỗi tương tự, và lặp lại mãi mãi.

Cách tiếp cận phản ứng này sẽ tan vỡ thảm hại khi xác minh mã do AI tạo ra. Các Mô hình Ngôn ngữ Lớn (LLM) rất giỏi trong việc tạo ra các đầu ra vượt qua các bài kiểm thử nhưng lại ẩn giấu các lỗi logic—chúng là thiên sinh khi tạo ra những "câu trả lời sai có vẻ hợp lý". Bản chất xác suất của chúng có nghĩa là các lỗi sẽ tái xuất hiện dưới những hình thức tinh vi khác, lẩn tránh các công cụ phát hiện dựa trên kiểm thử.

Nếu không có các quy tắc được khóa chặt từ đầu, động cơ xác minh cuối cùng sẽ tự đánh lừa chính mình. Nó bắt đầu hạ thấp tiêu chuẩn xác minh để dung hòa cho những ảo giác của AI. Một động cơ xác minh mà khám phá ra quy tắc từ việc kiểm tra mã sẽ rơi vào một vòng lặp tự biện minh. Nó xác minh mã dựa trên các ràng buộc được dẫn xuất từ chính mã đó.

Vì vậy, Axiom đã đảo ngược hoàn toàn mô hình:

1. Khai báo quy tắc: Định nghĩa các bất biến (invariants), hợp đồng, thuộc tính an toàn trước.
2. Mã hóa (Encode): Chuyển đổi quy tắc thành các hiện vật xác minh.
3. Chứng minh (Prove): Chứng minh về mặt toán học rằng mã thỏa mãn các quy tắc.
4. Thực thi (Execute): Chỉ khi đó mới cho phép thực thi.

Hiến pháp - Điều lệ - Biên niên sử: Phân tầng Quy tắc

Axiom chia các quy tắc thành ba lớp. Cấu trúc này được vay mượn từ hệ thống pháp luật.

Lớp	Từ khóa	Mẫu tệp	Mục đích	Tần suất thay đổi
Hiến pháp (Constitution)	Context	CONTEXT.md	Các nguyên tắc thiết kế bất biến	Gần như không bao giờ
Điều lệ (Ordinances)	Spec	docs/spec/*.md	Các thuật toán và ràng buộc chi tiết	Trung bình
Biên niên sử (Annals)	History	docs/history/*.md	Hồ sơ quyết định và lịch sử	Thường xuyên

Lớp 1: Hiến pháp (Context)

Định danh của dự án. Các nguyên tắc như "Tính toán cốt lõi phải chỉ sử dụng các hàm thuần túy (func)" thuộc về đây. Những thứ vi phạm nền tảng dự án sẽ nằm ở đây. Việc sửa đổi CONTEXT.md yêu cầu một cuộc xem xét kiến trúc nghiêm túc.

Ví dụ về quy tắc cốt lõi:

## 2. Nguyên tắc Kiến trúc Cốt lõi (SSOT)

### Thứ bậc Tính thuần túy
- **Tầng Tính toán Cốt lõi**: Tính toán trong `src/core` chỉ sử dụng `func` độc quyền
- **Tầng Thực thi Biên giới**: `proc` chỉ tồn tại ở các giao diện/hệ điều hành
- **Quy tắc Chỉ thực thi**: `proc` biên giới không được sở hữu logic nghiệp vụ

Lớp 2: Điều lệ (Spec)

Các quy tắc vận hành thực tế. Các giao diện trình giải SMT, chiến lược chứng minh Lean 4—các thông số kỹ thuật cụ thể nằm ở đây. Đây là hướng dẫn trong quá trình triển khai.

• bmc_core.md: Thuật toán kiểm tra mô hình, giao diện Z3, quy tắc thời gian chờ.
• uap_logic.md: Các giai đoạn pipeline chung, đề xuất phản ví, tinh chỉnh bất biến.
• lean_proof.md: Ngữ nghĩa Lean 4, chiến thuật, giao thức phát lại.

Lớp 3: Biên niên sử (History)

Trả lời câu hỏi "Tại sao chúng ta lại quyết định như vậy ngày xưa?". Ghi lại các thỏa hiệp trong quá khứ và bối cảnh quyết định. Biên niên sử chỉ để tham khảo—chúng không bao giờ nên điều khiển việc triển khai hiện tại.

Biên niên sử tách biệt với các quy tắc. Khi bạn cần "tại sao quy tắc này tồn tại?", hãy kiểm tra biên niên sử. Khi triển khai mã, hãy tập trung vào hiến pháp và điều lệ.

Chính sách Không hạ cấp: Đường ranh giới cứng

Axiom thực thi một quy tắc trên tất cả các quy tắc khác. Tính toàn vẹn chỉ có thể tăng lên, không bao giờ giảm xuống.

Bẫy func → proc

Ngôn ngữ Nim phân biệt nghiêm ngặt giữa các hàm thuần túy (func) và các thủ tục không thuần túy (proc). Trong quá trình phát triển, sự cám dỗ thường ập đến:

"Chỉ cần một câu lệnh echo nhanh ở đây. Để tôi tạm thời chuyển sang proc..."

Cách này không hoạt động trong Axiom.

Tại sao?

1. Hạ cấp là một chiều: Một khi proc tồn tại, các nhà phát triển sẽ tiếp tục thêm các tác dụng phụ. Nó lan truyền như cỏ dại.
2. Tính thuần túy là nhị phân: Một hàm要么 thuần túy,要么 không. "Hơi không thuần túy" là vô nghĩa.
3. Xác minh yêu cầu tính thuần túy: Bạn không thể chứng minh về mặt toán học các thuộc tính của các hàm có các tác dụng phụ khó lường trước.

Chế độ strictFuncs trong Nim 2.0+ và hệ thống theo dõi hiệu ứng làm cho sự khác biệt này trở nên mạnh mẽ hơn:

# strictFuncs thực thi tính thuần túy tại thời điểm biên dịch
{.push strictFuncs.}
func verifyLogic(node: Node): Result[void, Error] {.raises: [], tags: [].} =
  # Trình biên dịch từ chối bất kỳ đột biến trạng thái bên ngoài hoặc lệnh gọi IO nào
  if node.isValid: ok() else: err(InvalidNode)
{.pop.}

Đây là lý do Nim phù hợp hoàn hảo với kiến trúc của Axiom. Ngôn ngữ tự nó thực thi các ranh giới tính thuần túy tại thời điểm biên dịch, không chỉ ở khâu review code.

Cơ chế Thực thi của Axiom

Axiom duy trì một Thứ bậc Tính thuần túy:

┌─────────────────────────────────────────────────────────────┐
│ Tầng Tính toán Cốt lõi (src/core)                            │
│ ┌─────────────────────────────────────────────────────────┐ │
│ │ Chỉ dùng func: tính toán, phân tích cú pháp, chuẩn hóa  │ │
│ │ Trả về: Result[T], Option[T], VerifiedType[T]           │ │
│ │ Cấm: IO, đột biến, ngoại lệ                              │ │
│ └─────────────────────────────────────────────────────────┘ │
│                                                             │
│ Tầng Thực thi Biên giới (src/ui, src/cli, gateway)          │
│ ┌─────────────────────────────────────────────────────────┐ │
│ │ Cho phép proc: OS, TTY, hệ thống tệp, tiến trình        │ │
│ │ Vai trò: Thực thi kết quả func, tiêm phụ thuộc          │ │
│ │ Cấm: Logic nghiệp vụ, quy tắc miền                      │ │
│ └─────────────────────────────────────────────────────────┘ │
└─────────────────────────────────────────────────────────────┘

Khi proc xuất hiện trong src/core, nó sẽ bị gắn cờ là nợ kiến trúc (design debt)—một sự thỏa hiệp tạm thời với kế hoạch refactor bắt buộc. Mã sẽ không được xuất xưởng cho đến khi:

1. Ranh giới thực thi được đánh dấu rõ ràng.
2. Nhiệm vụ "thăng cấp func" tồn tại trong backlog.
3. Lý do không thuần túy được ghi lại trong CONTEXT.md.

Khi nào Bạn Vi phạm Quy tắc này

Trong Axiom, việc hạ cấp func thành proc không chỉ là sửa đổi mã. Nó được coi là phá hủy tính toàn vẹn toán học. Các bản hạ cấp không có lý do chính đáng (cập nhật CONTEXT.md) sẽ bị chặn hoàn toàn ở giai đoạn CI.

CI của Axiom thực thi điều này thông qua Cổng Thủ tục (Procedure Gate):

1. Nếu các tệp src/core thay đổi, hãy kiểm tra các bổ sung proc.
2. Nếu chuyển đổi func → proc xuất hiện trong diff, lỗi commit.
3. Nếu proc tồn tại mà không có tài liệu Biên giới tương ứng, lỗi commit.

Ngoại lệ duy nhất: Các thay đổi chỉ về phong cách (lỗi chính tả, chú thích, khoảng trắng). Mọi thứ khác都需要 cần biện minh kiến trúc.

Tại thời điểm biên dịch, hệ thống hiệu ứng của Nim cung cấp khả năng thực thi bổ sung:

# [Lớp 1: Tầng Tính toán Cốt lõi]
{.push strictFuncs.}
func verifyNodeIntegrity(node: AxiomNode): Result[void, IntegrityError] {.raises: [].} =
  ## Không IO, không đột biến, không ngoại lệ - thuần túy về mặt toán học
  if node.fingerprint == node.computedFingerprint():
    ok()
  else:
    err(IntegrityError.FingerprintMismatch)

# [Lớp 2: Tầng Thực thi Biên giới]
proc executeVerification(node: AxiomNode, output: File) {.raises: [IOError].} =
  ## Thực thi mỏng: tiêm phụ thuộc, ủy thát tất cả logic cho func
  let result = verifyNodeIntegrity(node)  # Gọi hàm thuần túy
  if result.isOk:
    output.write("Verification Passed\n")  # IO bị cô lập tại biên giới
  else:
    output.write("Verification Failed: " & $result.error & "\n")
{.pop.}

Bạn thấy khuôn mẫu chưa? verifyNodeIntegrity là toán học thuần túy. executeVerification là một lớp bao mỏng xử lý IO. Logic nghiệp vụ không bao giờ vượt qua vào lãnh thổ không thuần túy.

Ví dụ Thực tế

Khi triển khai hiển thị báo cáo, Axiom phải đối mặt với một lựa chọn:

# Cách tiếp cận ban đầu hấp dẫn:
proc renderReport(data: seq[ProofResult]) =
  # IO trực tiếp: ghi ra stdout
  for r in data:
    echo r.format()

# Cách tiếp cận thực thi tính thuần túy:
func renderReportLines(data: seq[ProofResult]): seq[string] {.noSideEffect.} =
  # Tính toán thuần túy: trả về chuỗi
  for r in data:
    result.add r.format()

proc writeReport(data: seq[ProofResults]) =
  # Thực thi mỏng: tiêm luồng đầu ra
  let lines = renderReportLines(data)
  for line in lines:
    echo line

Cách tiếp cận thứ hai tách biệt các mối quan tâm:

• renderReportLines là thuần túy, có thể kiểm thử, có thể xác minh.
• writeReport là thực thi tầm thường, có thể thay thế bằng đầu ra tệp, đầu ra mạng hoặc giả lập kiểm thử.

Đây không phải là kỹ thuật quá mức (over-engineering). Đây là điều làm cho việc xác minh trở nên khả thi.

Tại sao Các Nguyên tắc này Tồn tại

Axiom xác minh mã do AI tạo ra. Để làm điều này một cách đáng tin cậy, nó phải nghiêm ngặt hơn mã mà nó xác minh.

Thiết kế Ưu tiên Quy tắc đảm bảo:

• Các quy tắc xác minh không bao giờ được sửa đổi ngược để biện minh cho mã hiện có.
• Các nguyên tắc kiến trúc rõ ràng, có thể khám phá, và được thực thi.
• Tính toàn vẹn chỉ di chuyển theo một hướng: đi lên.

Sự tách biệt Hiến pháp - Điều lệ - Biên niên sử đảm bảo:

• Các nguyên tắc vẫn hiển thị mà không bị chìm trong các chi tiết.
• Người triển khai dễ dàng tìm thấy các thông số kỹ thuật.
• Lịch sử cung cấp thông tin nhưng không gây lộn xộn.

Chính sách Không hạ cấp đảm bảo:

• Tính thuần túy không bị hy sinh vì sự tiện lợi.
• Xác minh vẫn giữ âm thanh toán học.
• Nợ kỹ thuật hiển thị, được theo dõi và tạm thời.

Kết luận

Các nguyên tắc này không chỉ là mong muốn. Các cổng CI, review mã và tài liệu kiến trúc đều thực thi chúng. Mỗi lần Axiom commit phải vượt qua Cổng Thủ tục. Mỗi proc trong lõi phải biện minh cho sự tồn tại của nó. Mọi thay đổi quy tắc phải được tài liệu hóa trước khi triển khai.

Kiến trúc tự nó phải có thể xác minh được.

Xây dựng một động cơ xác minh có nghĩa là bạn không thể xác minh mã xác suất bằng các công cụ xác suất. Nền tảng phải là xác định, được chứng minh về mặt toán học và thuần túy về mặt kiến trúc.