zk-STARK: Xác minh tính toán trận chiến tự động phức tạp trên Ethereum

特邀专栏作者

2022-08-14 13:08 (UTC+8)

Bài viết này có khoảng 12818 từ, đọc toàn bộ bài viết mất khoảng 19 phút

Trong bài đăng này, tôi sẽ không đi sâu vào cách STARK hoạt động, nhưng tôi sẽ cung cấp một cái nhìn tổng quan thực tế về cách nó được sử dụng trong thực tế.

Tóm tắt AI

Tác giả gốc: Killari

Tiêu đề gốc: STARKs: Xác minh tính toán phức tạp của auto battler trên Ethereum — Mở rộng quy mô trò chơi phi tập trung

Việc thực thi các chức năng phức tạp trên Ethereum luôn là điều tối kỵ và không bao giờ nên thực hiện. Tính toán chuỗi khối rất tốn kém vì tất cả các nút được yêu cầu thực hiện cùng một phép tính để xác minh tính chính xác của nó.

StarkWare là một trong những dịch vụ mở rộng quy mô Ethereum cố gắng mở rộng quy mô Ethereum bằng cách sử dụng bằng chứng STARK (Bằng chứng tri thức minh bạch có thể mở rộng). Trong bài đăng này, tôi sẽ không đi sâu vào cách STARK hoạt động, nhưng tôi sẽ cung cấp một cái nhìn tổng quan thực tế về cách nó được sử dụng trong thực tế.

Đôi khi STARK có tiền tố là "zk-", có nghĩa là "bằng chứng không có kiến thức", cho phép STARK chứng minh điều gì đó mà không tiết lộ tất cả thông tin về điều chúng tôi đang cố gắng chứng minh. StarkWare đang làm việc để đưa ZK vào quy trình sau này, nhưng hiện tại họ chỉ tập trung vào khả năng mở rộng và không cần kiến thức để đạt được điều này.

Bài đăng trên blog của Vitalik là minh họa về cách zk-SNARK hiển thị cho người dùng.

Vitalik đã đưa ra một cái nhìn tổng quan ngắn về STARK trong bài viết của mình. STARK Phần 1: Chứng minh với Đa thức giải thích ngắn gọn cách hoạt động của các nguyên hàm mật mã này. Ngoài ra còn có SNARK (Lập luận kiến thức không tương tác ngắn gọn), đạt được điều gì đó tương tự như STARK, nhưng hơi khác một chút. Nếu bạn quan tâm hơn đến việc hiểu zk-SNARK, tôi thực sự khuyên bạn nên tham khảo tài liệu giải thích này: Nguyên tắc và triển khai zk-SNARK, giải thích có thẩm quyền của Maksym Petkus. Petkus đã giải thích nguyên tắc của zk-SNARK, bắt đầu từ toán học rất cơ bản, sau đó dần dần đi sâu vào toán học phức tạp hơn, đứng trên vai của những người đi trước. Kinh nghiệm đọc tuyệt vời.

Petkus tóm tắt zk-SNARK như sau:

tiêu đề phụ

STARK và trò chơi tự động chiến đấu

Trò chơi chiến đấu tự động (còn gọi là máy chiến đấu tự động, cờ vua tự động) là một loại trò chơi trong đó người chơi đưa ra các lựa chọn để phát triển nhân vật, nhưng họ không thể đưa ra bất kỳ lựa chọn nào trong các trận chiến mà sẽ tiến hành tự động. Sẽ rất vui nếu có một trò chơi như vậy chạy trên Ethereum L1, nhưng hiện tại một trò chơi như vậy không thể thực hiện được.

Vậy STARK có thể mang lại những lợi ích gì cho trò chơi tự động chiến đấu? Mô phỏng trò chơi tự động chiến đấu có thể rất phức tạp nên rất khó chạy. Nếu có một công nghệ giúp nó chỉ chạy một lần và những người chơi khác có thể tin tưởng vào tính toán này, đồng thời chắc chắn rằng không ai nói dối, thì nó sẽ cho phép chúng tôi có chế độ chơi tự động phi tập trung.

Đây là kế hoạch hành động:

1) Viết logic chiến đấu tự động bằng Python.

2) Xây dựng trình xác thực bằng ngôn ngữ Cairo của StarkNet (bắt buộc đối với bằng chứng STARK).

3) Thực thi mã cho trận chiến tự động, sử dụng trình xác thực Cairo mà chúng tôi đã tạo để tạo bằng chứng STARK về việc thực thi chương trình.

tiêu đề phụ

Viết hệ thống chiến đấu tự động bằng Python

Để bắt đầu hành trình của mình, chúng tôi chỉ cần lập trình logic của trận chiến tự động như bình thường, không yêu cầu phép thuật STARK ở đây.

Chúng tôi tạo một trình giả lập trận chiến tự động giữa hai nhân vật. Những vai trò này có bốn trạng thái:

- khỏe mạnh. Bằng với tổng số thiệt hại mà họ có thể nhận.

@dataclass
class Character:
  health: int
  damage: int
  attackRecoverTime: int
  healthPerTurn: int

- làm hại. Mỗi cuộc tấn công sẽ gây ra bao nhiêu thiệt hại cho nhau.

- Attack Recovery Time: Sau mỗi lần tấn công, kẻ tấn công cần đợi bao lâu trước khi tấn công lại.

- Health per round: lượng máu nhân vật hồi phục mỗi hiệp.

Các thuộc tính này có thể được định nghĩa là một lớp trong Python như hình bên dưới.

Đây là một sự cố về cách cuộc chiến sẽ diễn ra:

Chúng tôi có một vòng lặp trò chơi xoay vòng qua các vòng chiến đấu.
Trong mỗi lần lặp lại, chúng tôi khôi phục sức khỏe cho cả hai nhân vật và để họ đánh bại nhau nhanh nhất có thể.
Chúng tôi sẽ khiến những nhân vật này chiến đấu đến chết. Nếu một trong các nhân vật chết hoặc cả hai nhân vật đều chết, trận chiến coi như kết thúc.

Bằng cách chọn các thuộc tính nhân vật cụ thể, có thể xảy ra tình huống trận chiến không bao giờ kết thúc mà tiếp tục mãi mãi. Ví dụ, điều này có thể tránh được bằng cách giới hạn số vòng tối đa mà các trận chiến của chúng ta có thể kéo dài, sau đó xem xét giải quyết trận chiến với tỷ số hòa, điều này không có ý định được xem xét trong mã mẫu của chúng tôi.

Khi kết thúc quá trình mô phỏng, hãy trả lại lượng máu còn lại của mỗi nhân vật và đếm xem trận chiến đã diễn ra bao nhiêu hiệp.

Đây là phiên bản được viết bằng mã Python:

def simulateFight(character1, character2):
currentTick = 0
lastAttack = [0, 0]

while 1:
     # Health regeneration
     character1.health += character1.healthPerTurn
     character2.health += character2.healthPerTurn

     # Player 1 hits player 2
     if (lastAttack[0] == character1.attackRecoverTime):
         character2.health -= character1.damage
         lastAttack[0] = 0
     else:
         lastAttack[0] = lastAttack[0] + 1

     # Player 2 hits player 1
     if (lastAttack[1] == character2.attackRecoverTime):
         character1.health -= character2.damage
         lastAttack[1] = 0
     else:
         lastAttack[1] = lastAttack[1] + 1

     if character1.health <= 0 or character2.health <= 0:
         # one of the characters have died
         break
     currentTick = currentTick + 1

return {
     'endHealths': [character1.health, character2.health],
     'nCombatRounds': currentTick
}

Tiếp theo, hãy chọn ai sẽ có trận chiến hoành tráng này:

Chúng ta sẽ có một yêu tinh với thanh máu dài (1000 máu!) Gây 48 sát thương cho mỗi đòn tấn công, nhưng chờ 80 lần giữa các đòn tấn công. Yêu tinh cũng phục hồi ba điểm máu mỗi lượt.

Anh hùng thách thức của chúng ta có lượng máu thấp hơn nhiều, chỉ có 240 máu, hoàn toàn không hồi phục sức khỏe và sát thương mỗi đòn tấn công ít hơn (20), nhưng anh hùng của chúng ta chỉ phải đợi 2 lượt trước khi tấn công. Vì vậy, ít nhất anh hùng của chúng ta bằng cách nào đó tốt hơn yêu tinh! Đây là anh hùng của chúng tôi. Đây là một trận chiến thực sự của David và Goliath.

Chúng ta có thể xác định vai trò của mình trong mã như sau

player1 = Character(1000, 48, 80, 3) # Ogre
player2 = Character(240, 20, 2, 0) # Hero

Sau đó chúng ta có thể mô phỏng chiến đấu bằng cách gọi chức năng chiến đấu.

simulateFight(player1, player2

Chúng tôi sẽ nhận được kết quả của trận chiến:

{
    "player1": {
     "stats": [
      2000,
      48,
      80,
      3
     ]
    },
    "player2": {
     "stats": [
      1240,
      20,
      2,
      0
     ]
    },
    "log": {
     "endHealths": [
      999,
      1096
     ],
     "nCombatRounds": 272
    }
}ZERO_HP_POINT = 1000
assert player1.damage < ZERO_HP_POINT
assert player2.damage < ZERO_HP_POINT
data = {
    'player1': {
     'stats': [ZERO_HP_POINT + player1.health, player1.damage, player1.attackRecoverTime, player1.healthPerTurn]
    },
    'player2': {
     'stats': [ZERO_HP_POINT + player2.health, player2.damage, player2.attackRecoverTime, player2.healthPerTurn]
    },
  'log': simulateFight(player1, player2)
}
data['log']['endHealths'] = [h + ZERO_HP_POINT for h in data['log']['endHealths']]
with open('combat-input.json', 'w') as outfile:
json.dump(data, outfile)

Từ kết quả, chúng ta có thể đọc được rằng trận chiến kéo dài 272 hiệp và trận chiến kết thúc vì yêu tinh đã bị đánh bại. Anh hùng của chúng ta đã chiến thắng với 96 điểm máu khổng lồ! Đây là anh hùng của chúng tôi.

Tiếp theo, hãy lưu trữ tất cả thông tin quan trọng cần thiết về trận chiến trong một tệp để sau này chúng ta có thể chứng minh trận chiến bằng bằng chứng STARK. Tất cả những gì chúng ta cần là đầu vào chương trình (định nghĩa của người chơi 1 và người chơi 2) và đầu ra của chương trình (sức khỏe ở cuối và số lượt thực hiện). Trình xác nhận của chúng tôi hoàn toàn không cần chương trình!

Chúng tôi sẽ viết trình xác thực ở Cairo. Cairo là ngôn ngữ lập trình để viết các chương trình có thể kiểm chứng. Một trong nhiều yêu cầu của Cairo là tất cả các đầu vào phải không âm. Đó là sự bất hạnh của các nhà phát triển của chúng ta, nhưng phước lành của anh hùng của chúng ta, sức khỏe của yêu tinh trở nên âm, đó là một con số âm :(

Để giải quyết giới hạn này, chúng tôi sẽ thêm 1000 vào tất cả các giá trị sức khỏe và nếu sức khỏe của một nhân vật dưới 1000, anh ta được coi là đã chết. Để phương pháp này hoạt động với các giá trị sát thương khác nhau của nhân vật, chúng ta cũng cần đảm bảo rằng sát thương của nhân vật không bao giờ vượt quá 1000, vì khi đó sức khỏe của ai đó có thể trở lại âm. Đây là mã:

tiêu đề phụ

{
    "player1": {
     "stats": [
      2000,
      48,
      80,
      3
     ]
    },
    "player2": {
     "stats": [
      1240,
      20,
      2,
      0
     ]
    },
    "log": {
     "endHealths": [
      999,
      1096
     ],
     "nCombatRounds": 272
    }
}

Viết trình xác thực Cairo

Tiếp theo, chúng ta cần viết một chương trình xác minh để có thể STARK việc thực thi chương trình Python của chúng ta. Chương trình cần có khả năng xác minh rằng, với các thuộc tính trình phát ban đầu, khi mã mô phỏng được chạy, trình giả lập sẽ tạo ra đầu ra chính xác được hiển thị trong vùng nhật ký. Để đạt được điều này, chúng tôi sẽ chuyển sang lập trình bằng ngôn ngữ Cairo.

Chúng tôi sẽ xác định cấu trúc vai trò ở Cairo theo cách rất giống với những gì chúng ta thấy trong python:

struct Character:
    member health: felt
    member damage: felt
    member attackRecoverTime: felt
    member healthPerTurn: felt
end

Một điểm khác biệt lớn ở đây so với Python là chúng ta cần gán tất cả các biến cho một số kiểu dữ liệu không quen thuộc (viết tắt của phần tử trường). Loại dữ liệu cảm nhận là loại biến 252-bit (kỳ lạ, phải không?) được xác định giữa (-P/2, P/2), trong đó P là số nguyên tố lớn 252-bit.

Mặc dù nó có vẻ kỳ lạ, nhưng đối với mục đích của chúng tôi, cảm thấy hoạt động giống như một số nguyên. Tầm quan trọng của loại dữ liệu này là trình biên dịch Cairo dễ dàng tạo bằng chứng STARK từ mã của chúng tôi hơn là nếu chúng tôi thực sự xử lý các loại biến số nguyên hoặc dấu phẩy động. Bạn có thể đọc thêm về các loại biến cảm nhận từ tài liệu của Cairo.

Bây giờ, hãy bắt đầu viết chương trình Cairo để đảm bảo rằng trận chiến diễn ra theo đúng kế hoạch và người thực hiện chương trình không thể nói dối những người chơi khác. Ngoài loại nỉ và tính không âm của các biến đầu vào, Cairo còn có một số hạn chế khác. Chúng tôi đã sử dụng vòng lặp while trong mã Python, nhưng không thể sử dụng vòng lặp độ dài động ở Cairo, chúng tôi cần đệ quy để triển khai logic tương tự. Vì vậy, hãy xác định một hàm đệ quy sẽ xác thực một vòng chiến đấu và sau đó xác thực đệ quy tất cả các vòng chiến đấu khác:

func simulateCombat{ range_check_ptr } (
player1: Character,
player2: Character,
currentHealths: (felt, felt),
lastAttacks: (felt, felt),
currentRound: felt,
nCombatRounds: felt
) -> (
simNextHealths: (felt, felt),
simNextLastAttacks: (felt, felt)
)

Chức năng này lấy hai nhân vật của chúng ta, sức khỏe hiện tại của họ và bộ đếm thời gian tấn công lần cuối, vòng chiến đấu hiện tại và số vòng chiến đấu để mô phỏng. Sau đó, chúng tôi sẽ trả lại tình trạng và bộ đếm thời gian đã cập nhật của cuộc tấn công cuối cùng sau vòng xác thực để có thể xác thực vòng tiếp theo theo cách đệ quy.

Bạn có thể đã nhận thấy range_check_ptr ở đầu hàm của chúng tôi. range_check_ptr là một con trỏ chúng ta cần sử dụng để kiểm tra phạm vi (toán tử<, >, >=,<=). Các hoạt động này cũng khó khăn ở Cairo, nhưng may mắn là chúng ta vẫn có thể thực hiện chúng bằng cách sử dụng chức năng có sẵn range_check_ptr của Cairo.

Tiếp theo, hãy bắt đầu xác định phần bên trong của hàm. Về cơ bản, chúng tôi triển khai logic chính xác giống như vòng chiến của chúng tôi trong Python:

alloc_locals
local nextHealths: (felt, felt)
local nextLastAttacks: (felt, felt)
local ZERO_HP_POINT = 1000
if lastAttacks[1] == player2.attackRecoverTime:
tempvar afterDamage = currentHealths[0] - player2.damage
nextHealths[0] = afterDamage + player1.healthPerTurn
nextLastAttacks[1] = 0
else:
nextHealths[0] = currentHealths[0] + player1.healthPerTurn
nextLastAttacks[1] = lastAttacks[1] + 1
end
if lastAttacks[0] == player1.attackRecoverTime:
tempvar afterDamage = currentHealths[1] - player1.damage
nextHealths[1] = afterDamage + player2.healthPerTurn
nextLastAttacks[0] = 0
else:
nextHealths[1] = currentHealths[1] + player2.healthPerTurn
nextLastAttacks[0] = lastAttacks[0] + 1
end

Mã Cairo được viết hơi khác một chút so với Python. Điều này là do ở Cairo, chúng tôi chỉ có thể sử dụng các biến không đổi (một hạn chế thú vị khác). Khi chúng tôi đặt giá trị cho một biến, chúng tôi không thể thay đổi nội dung của nó nữa. Vì vậy, khi chúng tôi tăng sức khỏe của người chơi để phục hồi sức khỏe, chúng tôi đã tính toán nó cùng lúc với thiệt hại.

Tiếp theo, chúng tôi kiểm tra xem chúng tôi đã mô phỏng đủ số vòng yêu cầu chưa, nếu vậy chúng tôi kết thúc quá trình mô phỏng. Nếu quá trình mô phỏng chưa kết thúc, chúng ta cần kiểm tra xem cả hai người chơi có còn sống hay không. Nếu chúng tôi không có kiểm tra này, một trình giả lập độc hại có thể tiếp tục mô phỏng chiến đấu cho đến khi cả hai người chơi đều chết, điều này sẽ cho phép một người chơi đã chết tiếp tục chiến đấu! Chúng ta không thể cho phép sự điên rồ như vậy, chúng ta không thể cho phép những chiến binh bất tử xuất hiện trên đấu trường của chúng ta!

if currentRound == nCombatRounds:
return(nextHealths, nextLastAttacks)
else:
# if the combat has not ended, nobody can be dead
assert_nn(nextHealths[0] - ZERO_HP_POINT)
assert_nn(nextHealths[1] - ZERO_HP_POINT)
end

Ở đây chúng tôi đang sử dụng hàm assert_nn để kiểm tra xem giá trị bên trong hàm có phải là số âm hay không: nextHealths[0] > ZERO_HP_POINT. Nếu khẳng định là sai, quá trình thực thi không thành công và chúng tôi biết rằng người chạy trình giả lập đã nói dối chúng tôi.

Cuối cùng, hãy gọi hàm của chúng ta để nhận vòng mô phỏng tiếp theo và sau đó chúng ta sẽ trả về kết quả mô phỏng cuối cùng.

let (simulatedEndHealths, simulatedLastAttacks) = simulateCombat(
player1 = player1,
player2 = player2,
currentHealths = nextHealths,
lastAttacks = nextLastAttacks,
currentRound = currentRound + 1,
nCombatRounds = nCombatRounds
)
return(
simNextHealths = simulatedEndHealths,
simNextLastAttacks = simulatedLastAttacks
)

Khi chúng tôi có mã cho logic mô phỏng, chúng tôi cần viết chức năng chính cho chương trình Cairo của chúng tôi. Chương trình cần đọc đầu ra của chương trình Python và sau đó gọi hàm SimimCombat mà chúng ta vừa tạo. Hàm này sẽ trả về giá trị sức khỏe cuối cùng, sau đó chúng ta cần so sánh với đầu ra của chương trình Python. Đây là mã:

func main{ output_ptr: felt*, range_check_ptr }() -> ():
alloc_locals
local range_check_ptr = range_check_ptr
local pl1: Character*
local pl2: Character*
local endHealths: felt*
local nCombatRounds: felt
%{
     log = program_input['log']
     dat_endHealths = log['endHealths']
     dat_nCombatRounds = log['nCombatRounds']

     ids.pl1 = pl1 = segments.add()
     for i, val in enumerate(program_input['player1']['stats']):
         memory[pl1 + i] = val

     ids.pl2 = pl2 = segments.add()
     for i, val in enumerate(program_input['player2']['stats']):
         memory[pl2 + i] = val
     ids.endHealths = endHealths = segments.add()
     for i, val in enumerate(dat_endHealths):
         memory[endHealths + i] = val
     ids.nCombatRounds = dat_nCombatRounds
     assert len(program_input['player1']['stats']) == 4
     assert len(program_input['player2']['stats']) == 4
     assert len(dat_endHealths) == 2
%}

local player1: Character = pl1[0]
local player2: Character = pl2[0]

local currentHealths: (felt, felt) = (player1.health, player2.health)
local lastAttacks: (felt, felt) = (0, 0)

let (simulatedEndHealths, lastSimulatedAttacks) = simulateCombat(
     player1 = player1,
     player2 = player2,
     currentHealths = currentHealths,
     lastAttacks = lastAttacks,
     currentRound = 0,
     nCombatRounds = nCombatRounds
)

# Check that the healths will match what was claimed
assert simulatedEndHealths[0] = endHealths[0]
assert simulatedEndHealths[1] = endHealths[1]
# Return the program input and output
serialize_word(player1.health)
serialize_word(player1.damage)
serialize_word(player1.attackRecoverTime)
serialize_word(player1.healthPerTurn)

serialize_word(player2.health)
serialize_word(player2.damage)
serialize_word(player2.attackRecoverTime)
serialize_word(player2.healthPerTurn)

serialize_word(simulatedEndHealths[0])
serialize_word(simulatedEndHealths[1])

return ()
end

tiêu đề phụ

Tại sao chúng ta cần hai chương trình?

tiêu đề phụ

chạy!

Chúng tôi có thể chạy trình giả lập Python để biên dịch trình xác nhận Cairo của mình với:

> python combat.py
> cairo-compile combat.cairo -- output combat-compiled.json

Sau đó, chúng tôi có thể chạy chương trình Cairo với tệp đầu vào mà chúng tôi đã tạo bằng combat.py, tạo tệp combat.pie:

> cairo-run -- program=combat-compiled.json -- program_input=combat-input.json -- layout=small -- cairo_pie_output=combat.pie

Chúng tôi cũng có thể xác minh rằng tệp bánh là chính xác bằng lệnh sau:

> cairo-run -- layout=small -- run_from_cairo_pie=combat.pie

Bạn có thể thử sửa đổi các giá trị sức khỏe kết quả trong tệp battle-input.json, lưu ý rằng bạn không thể sửa đổi chúng mà không nhận được lỗi xác thực từ Cairo. Đối với mỗi đầu vào bắt đầu (Người chơi 1, Người chơi 2 và số lượt), trận chiến chỉ có một giải pháp. Ví dụ: nếu chúng tôi cố gắng gian lận bằng cách cho anh hùng của mình một thanh máu bổ sung khi kết thúc trận chiến, trình xác thực sẽ nhận thấy rằng chúng tôi đang cố gắng gian lận.

combat.cairo:120:5: Error at pc=0:201:
An ASSERT_EQ instruction failed: 1096 != 1097
assert simulatedEndHealths[1] = endHealths[1]
^*******************************************^

Tệp .pie chứa tất cả thông tin mà SHARP cần để tạo bằng chứng cho chúng tôi. SHARP là một dịch vụ do StarkWare điều hành, tạo ra bằng chứng về tính hợp lệ của việc thực thi chương trình Cairo. Sau đó, nó sẽ gửi các bằng chứng này đến mạng thử nghiệm Ethereum (Goerli) để được xác minh bằng các hợp đồng thông minh Ethereum.

Hiện tại, SHARP không thể chạy cục bộ và cách duy nhất để tạo bằng chứng từ các chương trình Cairo là sử dụng máy chủ của StarkWare để xác minh bằng chứng. Hy vọng rằng điều này sẽ thay đổi trong tương lai và bất cứ ai cũng có thể tạo ra bằng chứng về bất cứ điều gì. StarkWare có kế hoạch phát hành mã nguồn cho SHARP ở giai đoạn sau. Hiện tại, các trò chơi phi tập trung không thể được xây dựng bằng Cairo.

Hãy gửi công việc của chúng tôi tới SHARP:

> cairo-sharp submit -- cairo_pie combat.pie
Submitting to SHARP...
Job sent.
Job key: f48c551e-c0c6-4cf5-8a52-a0aa1c43728c
Fact: 0x17ee903dfb54b55e53cc03d5a47602e83ed0ff9e219fe4567b8d59fa2666f682

Sau một thời gian, chúng ta sẽ thấy thực tế của mình được xác thực và hợp lệ:

> cairo-sharp is_verified 0x17ee903dfb54b55e53cc03d5a47602e83ed0ff9e219fe4567b8d59fa2666f682 -- node_url=https://goerli-light.eth.linkpool.io/
True

tiêu đề phụ

https://www.cairo-lang.org/playground/sharp.html?job_key=f48c551e-c0c6-4cf5-8a52-a0aa1c43728c

Bằng chứng sử dụng trên hợp đồng thông minh Ethereum

Bây giờ chúng tôi biết rằng đối với một giá trị đầu vào nhất định (Người chơi 1, Người chơi 2 và số vòng), với hàm băm thực tế, chương trình sẽ xuất ra giá trị sức khỏe cuối cùng, chúng tôi có thể xác minh phép tính trên chuỗi mà không cần phải làm lại on-chain Thực hiện tính toán.

Trên thực tế, còn một thông tin nữa mà chúng tôi đang thiếu, đó là hàm băm của chương trình.

> cairo-hash-program -program combat-compiled.json
0x248070cb7b7f20b0b9445a382fdb4faa6b69c1f3653355077ae05b82c636ddf

Đây là đỉnh cao của tất cả các công việc trước đây của chúng tôi, một điều kỳ diệu của mật mã hiện đại, một chức năng Solidity đơn giản xác minh một thực tế và kiểm tra xem programOutput có hợp lệ không. Tất cả đều không có sự tính toán.

function verifyCombatOutput(uint256[] memory programOutput) public
bytes32 cairoProgramHash_ = 0x248070cb7b7f20b0b9445a382fdb4faa6b69c1f3653355077ae05b82c636ddf
// Ensure that a corresponding proof was verified.
bytes32 outputHash = keccak256(abi.encodePacked(programOutput));
bytes32 fact = keccak256(abi.encodePacked(cairoProgramHash_, outputHash));
require(cairoVerifier_.isValid(fact), "MISSING_CAIRO_PROOF");
// Ensure the output consistency with current system state.
require(programOutput.length == 10, "INVALID_PROGRAM_OUTPUT");
require(player1.health == programOutput[0], "INVALID_PROGRAM_OUTPUT 0");
require(player1.damage == programOutput[1], "INVALID_PROGRAM_OUTPUT 1");
require(player1.attackRecoverTime == programOutput[2], "INVALID_PROGRAM_OUTPUT 2");
require(player1.healthPerTurn == programOutput[3], "INVALID_PROGRAM_OUTPUT 3");

require(player2.health == programOutput[4], "INVALID_PROGRAM_OUTPUT 4");
require(player2.damage == programOutput[5], "INVALID_PROGRAM_OUTPUT 5");
require(player2.attackRecoverTime == programOutput[6], "INVALID_PROGRAM_OUTPUT 6");
require(player2.healthPerTurn == programOutput[7], "INVALID_PROGRAM_OUTPUT 7");

// Now we know that programOutput[8] and programOutput[9] represent the resulting health values,
// given the initial combat state variables programOutput[0..7]!.

// Pure Magic.
}