Move, ngôn ngữ lập trình đang thu hút nhiều dự án Web3, chúng ta cùng thảo luận thông qua hai tính năng: Tài nguyên có thể lập trình hỗ trợ tỷ lệ giao dịch cao và xác minh chính thức giúp cải thiện tính bảo mật.
Chúng ta cùng khám phá về Move với hợp đồng thông minh với, một trình ngôn ngữ mới. Bài viết sau đây tìm hiểu về chủ đề kỹ thuật của Move, trình bày cú pháp, mô hình bộ nhớ của Move, đồng thời xem xét một số lỗi phổ biến mà Move đang gặp phải.
Move đang phổ biến rộng rãi với những dự án như Aptos, Sui, OL và Starcoin, ban đầu được phát triển trong dự án Diem, mạng thanh toán dựa trên blockchain do Meta (trước đây là Facebook) đã dừng hoạt động.
Tài nguyên có thể lập trình
Tài nguyên (resource) đại diện cho một phần dữ liệu có giá trị, chẳng hạn như số lượng tài sản dự án do người dùng nắm giữ. Trong Move, mỗi tài chứa nội dung thường lưu trữ dữ liệu đại diện cho nội dung đó, trái ngược với việc thể hiện tài sản dự án trong Solidity. Hai ưu điểm chính trong việc sử dụng tài nguyên của Move như sau:
Thứ nhất, Move tạo thành một mô hình lập trình hợp đồng thông minh hỗ trợ tỷ lệ giao dịch cao. Nếu một giao dịch liên quan đến hai tài khoản chỉ tương tác với nhau, thì nó có thể được thực hiện song song với các giao dịch khác. Aptos đang làm điều tương tự, sử dụng bộ nhớ giao dịch phần mềm để chạy các giao dịch song song và phát hiện xem hai giao dịch đồng thời có bị xung đột hay không.
Thứ hai, Move có thể tự động xác minh chương trình đối với một số loại lỗi nhất định, tài nguyên không thể bị xóa hoặc sao chép, điều này được thực hiện bởi trình biên dịch Move. Nhưng vẫn có thể đưa ra các lỗi số học hoặc logic trong mã hợp đồng thông minh, dẫn đến giá trị tài nguyên không chính xác.
Move tổ chức sơ đồ hoạt động theo kiểu mỗi địa chỉ blockchain là một tài khoản. Không giống như Ethereum, chủ sở hữu Basic Coin có dữ liệu trong tài khoản của họ cho biết lượng Basic Coin họ nắm giữ.
Các tính năng bảo mật của Move
Ngoài tính năng trình biên dịch kiểm tra việc sử dụng tài nguyên cơ bản, Move hỗ trợ xác minh chính thức và loại bỏ những cấu trúc ngôn ngữ gây khó khăn.
Hệ thống di chuyển và Rust
Khi xử lý dữ liệu có giá trị, điều quan trọng là phải theo dõi ai sở hữu dữ liệu và hạn chế các hoạt động trên dữ liệu, chẳng hạn như sao chép hoặc xóa. Các nhà phát triển của Move lấy cảm hứng từ ý tưởng của Rust.
Những thông tin cơ bản của Move:
Sơ đồ cấu trúc của Move, các kiểu được xây dựng từ các kiểu khác:
Cấu trúc của Move là một tập hợp các giá trị được lưu trữ trong một trường:
struct S {
val : u64,
a : address,
}
Trong Move, cấu trúc là loại giá trị, được sắp xếp tuyến tính trong bộ nhớ hoặc bộ lưu trữ và một tham chiếu đến cấu trúc phải được xây dựng rõ ràng. Điều này khác với Solidity, trong đó các biến cấu trúc thường là tham chiếu đến giá trị cơ bản. Sơ đồ sau đây sẽ minh họa:
Move triển khai hệ thống sở hữu giống Rust cho các giá trị của kiểu cấu trúc, trong đó mỗi giá trị được sở hữu bởi biến hoặc trường chứa nó. Tài liệu tham khảo không sở hữu bất kỳ giá trị nào họ trỏ đến.
Thông thường, các giá trị cấu trúc chỉ có thể được chuyển cho chủ sở hữu khác, chúng không thể được sao chép hoặc xóa, khi đã được chuyển thì chủ sở hữu trước không thể truy cập.
Sau khi một giá trị của loại cấu trúc được tạo, chỉ có một bản sao có thể sử dụng được của giá trị tại một thời điểm. Đoạn mã sau minh họa điều này:
Khả năng khai thác trong phần khai báo kiểu cấu trúc của Move được thể hiện như sau:
Việc tính toán không chính xác và các lỗi logic phức tạp hơn liên quan đến tài nguyên vẫn có thể xảy ra. Giao diện lập trình cho lưu trữ toàn cầu trên chuỗi khối thực thi một hạn chế, mỗi tài khoản có thể chứa tối đa một bản sao của mỗi tài nguyên.
Xác minh chính thức
Các kỹ sư viết thông số kỹ thuật và thể hiện hành vi dự kiến của mã theo toán học, sau đó kiểm tra chúng có phù hợp hay không.
Move cũng có hỗ trợ tích hợp cho các kỹ thuật xác minh chính thức. Một ngôn ngữ đặc tả phong phú để xác minh, có thể tiêu chuẩn hóa các thuộc tính phức tạp hơn so với các mệnh đề yêu cầu và khẳng định của Solidity, đồng thời loại bỏ có chủ đích các cấu trúc ngôn ngữ gây ra sự cố khi xác minh chính thức. Môi trường phát triển Move bao gồm một trình kiểm tra có tên là “Move Prover”.
Một ví dụ đơn giản về chức năng kép và đặc điểm kỹ thuật của Move. Chức năng của hàm double là nhân đôi một số nguyên không dấu 64-bit (unsigned integer). Thông số kỹ thuật kép được đưa ra bởi spec double mô tả một cách toán học kết quả mong đợi.
fun double (x: u64): u64 {
x + x
}
spec double {
ensures result == x * 2;
}
Move Prover chuyển đổi thông số kỹ thuật và ngữ nghĩa thành các biểu thức logic. Sau đó, chúng được chuyển đến các bộ giải lý thuyết modulo thỏa mãn (SMT) chẳng hạn như Z3 và CVC5 để chứng minh hoặc bác bỏ. Sơ đồ đơn giản hóa rất nhiều sau đây minh họa điều này:
Tổng kết
Hy vọng bài viết mang đến cái nhìn tổng quan về ngôn ngữ Move. Tuy là ngôn ngữ sử dụng cách đây vài năm, nhưng khi ứng dụng vào blockchain thì Move vẫn còn mới mẻ. Không có ngôn ngữ nào an toàn 100% và mã không thể mở rộng hoặc không chính xác vẫn có cơ hội can thiệp vào chức năng tích hợp sẵn của Move. Chúng ta cùng chờ đợi sự bùng nổ của các hệ sinh thái sử dụng ngôn ngữ Move!
