Chứng chỉ biên dịch cho hợp đồng thông minh (SCP)
Translation certification for smart contracts (SCP).
Tính chính xác của trình biên dịch là một vấn đề cũ, nhưng với sự xuất hiện của các hợp đồng thông minh trên Blockchain, vấn đề đó lại xuất hiện dưới một góc nhìn mới. Hợp đồng thông minh là các phần mềm độc lập kiểm soát các tài sản (có giá trị) trong môi trường đối nghịch; một khi đã cam kết với Blockchain, các hợp đồng thông minh này không thể bị sửa đổi. Hợp đồng thông minh thường được phát triển bằng ngôn ngữ hợp đồng cấp cao và được biên dịch thành mã máy ảo cấp thấp trước khi được cam kết với Blockchain. Để người dùng hợp đồng thông minh tin tưởng một phần mã cấp thấp nhất định trên Blockchain, họ phải tự thuyết phục mình rằng (a) họ đang sở hữu mã nguồn trùng khớp và (b) trình biên dịch đã dịch đúng mã nguồn sang mã cấp thấp nhất định. Các phương pháp tiếp cận cổ điển về tính chính xác của trình biên dịch giải quyết điểm thứ hai. Các tác giả lập luận rằng chứng chỉ biên dịch cũng giải quyết triệt để điểm đầu tiên. Các tác giả mô tả kiến trúc chứng minh của một khung chứng chỉ biên dịch và chứng minh cách họ có thể mô hình hóa đường ống biên dịch như một chuỗi các mối liên hệ biên dịch. Các tác giả đưa ra một bản tường trình chi tiết về các mối liên hệ như vậy đối với hầu hết các lệnh của trình biên dịch Plutus Tx, mà họ đã chính thức hóa trong Coq. Phương pháp tiếp cận này tạo điều kiện cho phương pháp xác minh mô đun và mạnh mẽ khi đối mặt với việc triển khai trình biên dịch đang phát triển.