Xác minh

import guarantees from ‘@data/halis/guarantees.json’;

Một lời tuyên bố không kiểm chứng được chỉ là khẩu hiệu. Các bảo đảm của Halis được ghim vào một sổ cái kiểm chứng bằng máy, và khu vực xác minh chính là bộ máy kiểm tra chúng.

Sổ cái soundness

{guarantees.count} dòng, mỗi dòng có cơ chế thực thi, điểm neo trong cây mã nguồn và các probe âm tính phải thất bại đúng như mong đợi:

{guarantees.ids.map((id) => \${id}``).join(’, ’)}

Phạm vi của tài liệu thưởng bug-bounty chính là sổ cái đó: một tuyên bố được thưởng ứng với đúng một dòng ledger, và người báo cáo gọi tên dòng đó.

make guarantee-report tái dựng ledger và render nó. hls-guarantee verify chứng minh lại toàn bộ ledger trên trình biên dịch đang chạy, và từ chối viết một báo cáo từ một ledger đã bị vi phạm.

Điểm cố định của bootstrap

Trình biên dịch được viết bằng Halis, nên nó phải biên dịch được chính nó — và phải cho ra đúng kết quả đó. Xem luật bootstrap.

Kiểm thử vi sai

Interpreter, bản build native và backend WebAssembly phải cho ra cùng một ký tự trên cùng một chương trình. Các bộ test vi sai chạy trên mọi pull request, và chúng so sánh lớp dừng chứ không chỉ so sánh kết quả — một chương trình dừng vì lý do khác ở backend khác là một lỗi.

Dashboard hồi quy

Hiệu năng, kích thước RSS, thời gian biên dịch và kích thước binary được ghi lại theo từng commit. Một hồi quy không có ghi chép chấp thuận sẽ fail cổng.

Kiểm toán độc lập

Có hai bộ audit của bên thứ ba: bộ audit thường trực và bộ audit cuối cùng ghim bề mặt đã đóng băng, manifest snapshot và sổ cái bảo đảm. Mỗi lượt bằng chứng được dán nhãn mức độ độc lập, và con dấu đóng hồ sơ bị cổng make finalaudit-gate cưỡng chế.

Cổng phát hành

make release-acceptance đánh giá cây mã như một trạng thái hợp pháp của dòng phát hành, và hls-lts status đọc đồng hồ của dòng đã mở. Một lần push tag không có mục phát hành tương ứng sẽ bị pipeline từ chối.