zk-STARK: Ethereum에서 복잡한 자동 전투 계산 검증

DAOrayaki

特邀专栏作者

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

이 기사는 약 12818자로, 전체를 읽는 데 약 19분이 소요됩니다

이 게시물에서는 STARK의 작동 방식에 대해 너무 깊이 들어가지는 않겠지만 실제로 어떻게 사용되는지에 대한 실질적인 개요를 제공할 것입니다.

AI 요약

펼치기

이 게시물에서는 STARK의 작동 방식에 대해 너무 깊이 들어가지는 않겠지만 실제로 어떻게 사용되는지에 대한 실질적인 개요를 제공할 것입니다.

원작자: 킬라리

원래 제목: STARKs: Ethereum에서 복잡한 자동 배틀러 계산 확인 — 탈중앙화 게임 확장

이더리움에서 복잡한 기능을 실행하는 것은 항상 절대 안 되는 일이며 절대 해서는 안 됩니다. 모든 노드가 정확성을 확인하기 위해 동일한 계산을 수행해야 하기 때문에 블록체인 계산은 매우 비쌉니다.

StarkWare는 STARK(Scalable Transparent Proof of Knowledge) 증명을 사용하여 Ethereum 확장을 시도하는 Ethereum 확장 서비스 중 하나입니다. 이 게시물에서는 STARK의 작동 방식에 대해 너무 깊이 들어가지는 않겠지만 실제로 어떻게 사용되는지에 대한 실질적인 개요를 제공할 것입니다.

때때로 STARK는 "영지식 증명"을 의미하는 "zk-" 접두사를 붙입니다. 이는 STARK가 우리가 증명하려는 것에 대한 모든 정보를 공개하지 않고 무언가를 증명할 수 있도록 합니다. StarkWare는 나중에 ZK를 파이프라인에 포함시키기 위해 노력하고 있지만 현재는 확장성에만 집중하고 있으며 이를 달성하기 위해 지식이 전혀 필요하지 않습니다.

Vitalik의 블로그 게시물은 zk-SNARK가 사용자에게 렌더링되는 방식을 보여줍니다.

Vitalik은 자신의 기사에서 STARK에 대한 간략한 개요를 제공했습니다. STARK 파트 1: 다항식을 사용한 증명에서는 이러한 암호화 프리미티브가 작동하는 방식을 간략하게 설명합니다. STARK와 비슷하지만 약간 다른 SNARK(Succinct Non-Interactive Arguments of Knowledge)도 있습니다. zk-SNARK에 대한 이해에 더 관심이 있다면 Maksym Petkus의 권위 있는 설명인 zk-SNARK의 원리 및 구현 설명 문서를 강력히 추천합니다. Petkus는 zk-SNARK의 원리를 매우 기초적인 수학에서 시작하여 점점 더 복잡한 수학을 심화시켜 전임자들의 어깨에 올라섰다고 설명했습니다. 훌륭한 독서 경험.

Petkus는 zk-SNARK를 다음과 같이 요약합니다.

보조 제목

STARK 및 자동 전투 게임

자동 전투 게임(Automatic Battle Machine, Auto Chess라고도 함)은 플레이어가 캐릭터의 성장을 위해 선택을 하지만 전투 중에는 아무 선택도 할 수 없고 자동으로 진행되는 일종의 게임입니다. 그런 게임을 이더리움 L1에서 돌리면 재미있겠지만 현재로서는 그런 게임을 할 수 없다.

그렇다면 STARK는 자동 전투 게임에 어떤 이점을 가져올 수 있습니까? 자동 전투 게임의 시뮬레이션은 매우 복잡할 수 있으므로 실행하기가 어렵습니다. 한 번만 실행되도록 하는 기술이 있고 다른 플레이어가 이 계산을 신뢰할 수 있으면서 아무도 거짓말을 하지 않는다는 것을 확신할 수 있다면 분산형 자동 플레이가 가능해질 것입니다.

행동 계획은 다음과 같습니다.

1) Python으로 자동 전투 로직을 작성합니다.

2) StarkNet의 카이로 언어로 유효성 검사기를 구축합니다(STARK 증명에 필요).

3) STARK 프로그램 실행 증명을 생성하기 위해 구축한 카이로 유효성 검사기를 사용하여 자동 전투용 코드를 실행합니다.

보조 제목

Python으로 자동 전투 시스템 작성

여정을 시작하기 위해 우리는 평소처럼 자동 전투의 논리를 프로그래밍하기만 하면 됩니다. 여기에는 STARK 마법이 필요하지 않습니다.

우리는 두 캐릭터 간의 자동 전투 시뮬레이터를 만듭니다. 이러한 역할에는 네 가지 상태가 있습니다.

- 건강한. 그들이 받을 수 있는 피해의 총량과 동일합니다.

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

- 피해. 각 공격이 서로에게 입히는 피해량.

- 공격 복구 시간: 각 공격 후 공격자가 다시 공격하기 전에 기다려야 하는 시간입니다.

- 라운드당 체력: 캐릭터가 라운드당 회복하는 체력.

이러한 속성은 아래와 같이 Python에서 클래스로 정의할 수 있습니다.

다음은 전투가 진행되는 방식에 대한 분석입니다.

전투 라운드를 순환하는 게임 루프가 있습니다.
반복할 때마다 두 캐릭터의 체력을 회복하고 최대한 빨리 서로를 때리도록 합니다.
우리는 이 캐릭터들이 죽을 때까지 싸우게 만들 것입니다. 캐릭터 중 하나가 죽거나 두 캐릭터가 모두 죽으면 전투가 끝난 것으로 간주됩니다.

특정 캐릭터 속성을 선택하면 전투가 끝나지 않고 영원히 계속되는 상황을 가질 수 있습니다. 예를 들어 전투가 지속될 수 있는 최대 라운드 수를 제한한 다음 무승부로 전투를 해결하는 것을 고려하여 이를 방지할 수 있습니다. 이는 샘플 코드에서 고려되지 않습니다.

시뮬레이션이 끝나면 각 캐릭터의 체력이 얼마나 남았는지 반환하고 전투가 몇 라운드 걸렸는지 세어 봅시다.

다음은 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
}

다음으로, 누가 이 장대한 전투를 벌일지 선택합시다:

공격당 48의 피해를 입히지만 공격 사이에 80번을 기다리는 긴 체력 막대(1000 건강!)를 가진 오우거가 있습니다. 오우거는 또한 턴당 3개의 체력을 회복합니다.

도전자 영웅은 체력이 훨씬 낮고 체력이 240에 불과하며 체력 재생이 전혀 없고 공격당 피해가 적습니다(20). 하지만 우리의 영웅은 공격하기 전에 2턴만 기다리면 됩니다. 그래서 적어도 우리의 영웅은 오우거보다 낫습니다! 이것은 우리의 영웅입니다. 이것은 진정한 다윗과 골리앗의 전투입니다.

다음과 같이 코드에서 역할을 정의할 수 있습니다.

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

그런 다음 전투 함수를 호출하여 전투를 시뮬레이션할 수 있습니다.

simulateFight(player1, player2

전투 결과는 다음과 같습니다.

{
    "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)

전투는 272라운드 지속되었고 오우거가 패배하여 전투가 종료되었다는 결과를 읽을 수 있습니다. 우리의 영웅은 엄청난 96점의 피로 승리했습니다! 이것은 우리의 영웅입니다.

다음으로 전투에 필요한 모든 중요 정보를 파일에 저장하여 나중에 STARK 증명으로 전투를 증명할 수 있습니다. 우리에게 필요한 것은 프로그램 입력(플레이어 1과 플레이어 2의 정의)과 프로그램 출력(마지막의 체력과 수행한 턴 수)뿐입니다. 우리의 유효성 검사기는 프로그램 자체가 전혀 필요하지 않습니다!

우리는 카이로에서 유효성 검사기를 작성할 것입니다. Cairo는 검증 가능한 프로그램을 작성하기 위한 프로그래밍 언어입니다. Cairo의 많은 요구 사항 중 하나는 모든 입력이 음수가 아니어야 한다는 것입니다. 우리 개발진의 불행이지만 우리 영웅의 축복, 오우거의 체력이 마이너스가 되니 음수입니다 :(

이 제한을 피하기 위해 모든 체력 값에 1000을 추가하고 캐릭터의 체력이 1000 미만이면 죽은 것으로 간주합니다. 이 방법이 다른 캐릭터 데미지 값으로 작동하려면 캐릭터의 데미지가 절대 1000을 초과하지 않도록 해야 합니다. 그러면 누군가의 건강이 다시 마이너스가 될 수 있기 때문입니다. 코드는 다음과 같습니다.

보조 제목

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

카이로 유효성 검사기 작성

다음으로 Python 프로그램의 실행을 STARK할 수 있도록 검증 프로그램을 작성해야 합니다. 프로그램은 초기 플레이어 속성이 주어지면 시뮬레이션 코드가 실행될 때 시뮬레이터가 로그 영역에 표시된 정확한 출력을 생성하는지 확인할 수 있어야 합니다. 이를 달성하기 위해 우리는 카이로 언어로 프로그래밍을 전환할 것입니다.

우리는 카이로에서 우리가 파이썬에서 보는 것과 매우 유사한 방식으로 역할 구조를 정의할 것입니다:

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

여기서 파이썬과 비교했을 때 큰 차이점은 모든 변수를 익숙하지 않은 데이터 유형 펠트(필드 요소의 줄임말)에 할당해야 한다는 것입니다. 펠트 데이터 유형은 (-P/2, P/2) 사이에 정의된 252비트(이상하지 않습니까?) 변수 유형입니다. 여기서 P는 큰 252비트 소수입니다.

이상하게 보일 수 있지만 우리의 목적을 위해 펠트는 정수처럼 작동합니다. 이 데이터 유형의 중요성은 실제로 정수 또는 부동 소수점 변수 유형을 처리하는 것보다 Cairo 컴파일러가 코드에서 STARK 증명을 만드는 것이 더 쉽다는 것입니다. Cairo 문서에서 펠트 변수 유형에 대해 자세히 읽을 수 있습니다.

이제 전투가 계획대로 진행되고 프로그램 실행자가 다른 플레이어에게 거짓말을 할 수 없도록 카이로 프로그램 작성을 시작하겠습니다. 입력 변수의 펠트 유형 및 비음성 외에도 Cairo에는 몇 가지 다른 제한 사항이 있습니다. Python 코드에서 while 루프를 사용했지만 카이로에서는 동적 길이 루프가 불가능하므로 동일한 논리를 구현하려면 재귀가 필요합니다. 따라서 단일 전투 라운드를 검증한 다음 다른 모든 전투 라운드를 재귀적으로 검증하는 재귀 함수를 정의해 보겠습니다.

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)
)

이 기능은 두 캐릭터, 현재 건강 및 마지막 공격 타이머, 현재 전투 라운드 및 시뮬레이션할 전투 라운드 수를 사용합니다. 그런 다음 다음 라운드를 재귀적으로 검증할 수 있도록 검증 라운드 후 마지막 공격의 업데이트된 상태와 타이머를 반환합니다.

함수 시작 부분에 있는 range_check_ptr을 눈치챘을 것입니다. range_check_ptr은 범위 검사에 사용해야 하는 포인터입니다(연산자<, >, >=,<=). 이러한 작업은 카이로에서도 어렵지만 다행스럽게도 카이로의 range_check_ptr 내장 함수를 사용하여 수행할 수 있습니다.

다음으로 함수의 내부 정의를 시작하겠습니다. 우리는 기본적으로 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

카이로 코드는 파이썬과 약간 다르게 작성되었습니다. 카이로에서는 상수 변수만 사용할 수 있기 때문입니다(또 다른 흥미로운 제한 사항). 변수에 값을 설정하면 더 이상 내용을 변경할 수 없습니다. 그래서 체력 재생을 위해 플레이어의 체력을 증가시킬 때 데미지와 동시에 계산했습니다.

다음으로 필요한 라운드 수를 시뮬레이션했는지 확인하고 그렇다면 시뮬레이션을 종료합니다. 시뮬레이션이 아직 끝나지 않았다면 두 플레이어가 아직 살아 있는지 확인해야 합니다. 이 검사가 없으면 악의적인 에뮬레이터 러너가 두 플레이어가 모두 죽을 때까지 전투를 시뮬레이션하여 이미 죽은 플레이어가 계속 싸울 수 있습니다! 우리는 그런 광기를 허용할 수 없습니다. 언데드 전사가 우리 경기장에 나타나는 것을 허용할 수 없습니다!

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

여기서 우리는 함수 내부의 값이 음수가 아닌지 확인하는 assert_nn 함수를 사용하고 있습니다: nextHealths[0] > ZERO_HP_POINT. assert가 false이면 실행이 실패하고 에뮬레이터를 실행하는 사람이 우리에게 거짓말을 했음을 알 수 있습니다.

마지막으로 함수를 호출하여 시뮬레이션의 다음 라운드를 가져온 다음 최종 시뮬레이션 결과를 반환합니다.

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

시뮬레이션 논리에 대한 코드가 있으면 카이로 프로그램의 기본 기능을 작성해야 합니다. 프로그램은 Python 프로그램의 출력을 읽은 다음 방금 생성한 시뮬레이션 전투 함수를 호출해야 합니다. 이 함수는 최종 상태 값을 반환하며 Python 프로그램의 출력과 비교해야 합니다. 코드는 다음과 같습니다.

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

보조 제목

왜 두 개의 프로그램이 필요한가요?

보조 제목

달리다!

Python 에뮬레이터를 실행하여 다음을 사용하여 Cairo 유효성 검사기를 컴파일할 수 있습니다.

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

그런 다음 battle.py로 생성한 입력 파일로 Cairo 프로그램을 실행하여 battle.pie 파일을 생성할 수 있습니다.

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

다음 명령을 사용하여 파이 파일이 올바른지 확인할 수도 있습니다.

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

battle-input.json 파일에서 결과 상태 값을 수정할 수 있습니다. Cairo에서 유효성 검사 오류를 받지 않고는 수정할 수 없습니다. 각 시작 입력(플레이어 1, 플레이어 2 및 턴 수)에 대해 전투에는 하나의 해결 방법만 있습니다. 예를 들어, 싸움이 끝날 때 영웅에게 여분의 체력 막대를 제공하여 속임수를 시도하면 유효성 검사기는 우리가 속임수를 시도하고 있음을 알아차릴 것입니다.

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

.pie 파일에는 SHARP가 우리를 위해 증명 생성을 수행하는 데 필요한 모든 정보가 포함되어 있습니다. SHARP는 Cairo 프로그램 실행의 유효성 증명을 생성하는 StarkWare에서 운영하는 서비스입니다. 그런 다음 이 증명을 이더리움 테스트넷(Goerli)으로 보내 이더리움 스마트 계약에서 확인하도록 합니다.

현재 SHARP는 로컬에서 실행할 수 없으며 Cairo 프로그램에서 증명을 생성하는 유일한 방법은 증명 확인을 위해 StarkWare의 서버를 사용하는 것입니다. 바라건대 이것은 미래에 변경되고 누구나 모든 것에 대한 증거를 생성할 수 있습니다. StarkWare는 추후 SHARP용 소스 코드를 공개할 계획입니다. 현재 카이로를 사용하여 분산 게임을 구축할 수 없습니다.

작업을 SHARP에 제출해 보겠습니다.

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

잠시 후 우리는 사실이 검증되고 유효한 것을 볼 수 있습니다.

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

보조 제목

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

Ethereum 스마트 계약에 대한 사용 증명

이제 우리는 주어진 입력 값(플레이어 1, 플레이어 2 및 라운드 수)에 대해 팩트 해시가 주어지면 프로그램이 최종 건강 값을 출력해야 한다는 것을 알았으므로 온체인에서 다시 수행 계산을 수행합니다.

사실 우리가 놓치고 있는 정보가 하나 더 있는데, 바로 프로그램의 해시입니다.

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

이것은 우리의 모든 이전 작업의 정점, 현대 암호화의 경이로움, 사실을 확인하고 programOutput이 유효한지 확인하는 간단한 Solidity 기능입니다. 계산 자체가 없는 모든 것.

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.
}