대부분의 프로그래밍 언어와 달리 Simplicity의 표현식은 일련의 조합자(combinator)로 구성되며, 이 조합자들은 더 작은 표현식을 조합하여 만듭니다. 이러한 표현식은 일부 입력을 받아 일부 출력으로 매핑하는 함수를 나타냅니다.

다음은 가장 간단한 Simplicity 프로그램입니다.

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

여기서 마지막 Simplicity 표현식이 우리의 main 함수입니다. 아래에서 위로 읽어보면 여러 개의 작은 함수로 구성되어 있으며, 결국 단위 조합자로 귀결된다는 것을 알 수 있습니다. 단위 조합자는 빈 출력을 생성합니다. 단위 조합자는 임의의 입력을 받아 변경되지 않은 상태로 반환하는 iden, 외부에서 제공된 값을 출력하는 witness와 함께 모든 Simplicity 표현식의 기초를 형성합니다.

이 코드 스니펫에서는 표현식의 각 부분에서 다음 부분으로 어떤 데이터가 흐르는지를 나타내는 데 도움이 되는 타입 주석을 제공했습니다. 여기서 "1"은 단위 타입을 나타내며, 우리가 "빈 출력"이라고 부르는 것입니다. "2"는 비트를 나타내며 0 또는 1 값을 가질 수 있습니다.

이 스니펫을 자세히 따라오지 못했더라도 걱정하지 마세요. Simplicity 코드가 어떻게 생겼는지 시각적으로 보여드리기 위한 것일 뿐입니다. 이 글의 뒷부분에서는 좀 더 흥미로운 프로그램을 더 자세히 분석해 보겠습니다.

명세 언어

궁극적으로 모든 프로그래밍 언어는 계산을 결합해 더 큰 계산을 구축한다는 개념을 표현합니다. 비트코인 스크립트(Forth나 PostScript 같은)는 각 계산이 데이터 객체 목록을 차례로 조작하는 스택 머신을 통해 이를 수행합니다. 이더리움의 EVM은 코드가 다른 코드 블록(아마도 다른 계약에서)을 호출할 수 있는 함수 호출 아키텍처를 사용하여 데이터를 입력으로 받고 데이터를 출력으로 반환합니다. 이는 현재 거의 모든 주류 프로그래밍 언어가 사용하는 모델이기도 합니다.

프로그래밍 언어는 소비되는 트랜잭션과 같이 외부 세계와 상호작용하기 위해 부작용(side effect)을 사용합니다. EVM에서 계약은 키-값 데이터 저장소에 액세스할 수 있으며, 이를 통해 명시적으로 전달하지 않고도 트랜잭션 전반에서 상태를 유지할 수 있습니다.

비트코인 스크립트와 EVM 모두 단일 opcode로 비트 반전을 수행할 수 있습니다(비트코인 버전은 다양한 입력을 취할 수 있지만, 대부분은 비트와 유사하지 않은 반면, EVM 버전은 비트처럼 작동하지만 항상 256비트에 대해 한 번에 작동합니다). Simplicity 모델이 왜 이렇게 단순한 작업에 대해 이렇게 장황한 설명이 필요한지 의문을 제기하는 것도 당연합니다.

Simplicity의 목표는 프로그램이 어떤 함수를 표현하는지, 그리고 이를 평가하는 데 어떤 계산 리소스가 사용되는지 등 프로그램의 의미론을 형식적으로 명시하는 것입니다. 원칙적으로 비트코인 스크립트나 EVM처럼 작동하는 언어를 형식적으로 명시하는 것은 가능하지만, 그 작업은 매우 어렵고 그 결과 또한 누구도 검증하기 어려울 것입니다. 대신, 우리는 Simplicity를 통해 수학적으로 기본적인 함수 조합 방식을 반영하는 작은 기본 조합자 집합을 정의했습니다. 이 결과 언어의 시맨틱은 너무 작아서 티셔츠에 들어갈 정도입니다.

실제로 비트 반전과 같은 작업에서 이 코드는 한 번만 작성되고 재사용될 것입니다. 사실 이 작업은 저희가 작성하여 언어에 내장했습니다. 직접 코드를 작성할 때는 위의 코드 대신 간단한 jet_not 단축키를 사용하면 됩니다. 다음 섹션에서 jet에 대해 더 자세히 설명하겠습니다.

결국에는 거의 아무도 Simplicity 코드를 작성하지 않게 될 것입니다. Simplicity는 블록체인 프로그램을 위한 잘 정의된 기반을 제공하지만, 이는 단지 기반일 뿐입니다. 실제 작업은 올바른 작동 증명과 함께 Simplicity 코드로 컴파일되는 상위 언어에서 수행될 것입니다.

프로그램 vs. 표현식

자명한 입력값과 출력값을 가진 표현식에는 특별한 이름이 있습니다. 우리는 이러한 표현식을 프로그램이라고 부릅니다. 수학적으로 말하자면, 자명한 입력을 자명한 출력에 매핑하는 함수는 단 하나만 존재하기 때문에 이러한 Simplicity 표현식이 유용할지가 확실하지 않습니다. 하지만 이러한 표현식은 유용할 뿐만 아니라 블록체인에서 유일하게 허용되는 표현식입니다!

그렇다면 전략은 무엇일까요? 두 가지 전략이 있습니다. 하나는 주소에 커밋된 Simplicity 프로그램에 공백이 있어 코인이 실제로 사용될 때만 채워지는 것이고, 다른 하나는 Simplicity 프로그램에 부작용이 있어 블록체인 데이터에 접근하거나 조기에 중단할 수 있어 순수한 수학적 함수의 범위를 벗어나는 것입니다.

Simplicity 프로그램에 공백을 지정하는 방법에는 두 가지가 있는데요. disconnect 와 witness 조합자입니다. disconnect는 약간 미묘하며, 이에 대해 전에도 이야기한 적이 있습니다. 하지만 witness는 매우 간단합니다. witness 조합자는 디지털 서명, 해시 프리이미지 또는 특정 서명 키 선택과 같이 증인이라고 불리는 특정 유형의 값을 반환합니다.

Simplicity가 부작용을 지원하는 방법도 두 가지가 있습니다. 하나는 트랜잭션 데이터를 인트로스펙션(introspection) 하는 것이고(이후 포스팅에서 더 자세히 설명하겠습니다), 다른 하나는 어설션(assertion)을 통하는 것입니다. 어설션은 프로그램 실행을 중단시킵니다. 비트코인 스크립트에서는 어설션에 VERIFY opcode가 사용되며, 잘못된 서명이나 다른 데이터를 발견하면 프로그램이 실패하도록 합니다. EVM은 같은 목적으로 STOP opcode를 사용합니다.

이제 입력과 출력 유형이 명목적으로는 자명한 프로그램이지만 실제로는 유용한 계산에 영향을 줄 수 있다는 것을 알았습니다. 증인은 프로그램 입력의 목적을 수행하고 어설션은 "통과/실패" 프로그램 출력을 제공합니다.

다른 예를 살펴봅시다. 다음은 두 개의 증인을 받아 동일성을 확인하는 프로그램입니다.

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

이 프로그램을 아래에서 위로 읽어보면, 프로그램 자체는 1->1 타입(type)의 main이라는 단일 표현식입니다. 여기서 표현식의 '타입'은 입력과 출력으로 어떤 종류의 값을 받는지를 나타냅니다. 1 타입은 값이 하나뿐이므로 아무 정보도 나타내지 않습니다. 2 타입은 가능한 값이 두 개이므로 단일 비트, 2^32는 32비트 문자열 등을 나타낼 수 있습니다.

아래쪽의 등식을 보면 main은 이름이 cp3와 jt4인 표현식의 합성체(composition)임을 알 수 있습니다. 그런 다음 cp3 자체가 pr1과 jt2의 합성체입니다. 이 프로그램에는 다섯 가지 조합자가 사용됩니다:

●      Comp또는 composition은 두 개의 표현식을 취하고 첫 번째 출력을 입력으로 사용하여 두 번째 표현식을 평가합니다.

●      Pair는 두 개의 표현식을 취하고 왼쪽 부분은 첫 번째 표현식의 출력이고 오른쪽 부분은 두 번째 표현식의 출력인 값 쌍을 출력하는 새 표현식을 생성합니다.

●      Witness는 입력은 취하지 않지만 출력은 다형적(polymorphic) 타입입니다. 프로그램이 의미를 가지는데 필요한 그 어떠한 타입이 될 수 있습니다. 그리고 이 함수가 산출하는 값은 평가 시점에 제공되는 값입니다.

●      jet_eq_32는 jet이며, 이는 더 큰 Simplicity 표현식을 대체하는 단일 조합자라는 의미입니다. 대체된 표현식을 명세(specification)라고 하며, Simplicity 인터프리터는 이 명세를 평가하거나 동일한 효과를 내는 최적화된 기계 코드를 사용하여 jet를 평가할 수 있습니다. 이 특정 jet는 두 개의 32비트 값을 받아 두 값이 동일한지(1) 또는 다른지(0)를 나타내는 단일 비트를 출력합니다.

●      jet_verify 도 jet입니다. 이 함수는 단일 비트를 입력으로 취하며, 해당 비트가 0이면 프로그램을 중단합니다. 출력은 없습니다.

결론

이번 블로그 포스팅을 통해 Simplicity 코드가 어떻게 생겼는지 살펴보고, 단순해 보이는 기능도 명시적으로 작성하면 꽤 복잡해 보일 수 있다는 것을 알 수 있었습니다. 하지만 이러한 복잡성은 실제로 내부에서 일어나는 일을 반영합니다. 명세 언어인 Simplicity로 모든 것을 명시적으로 만들 수 있으므로, 수학적으로 모델링하고 애플리케이션에 필요한 필수 속성을 증명한 다음 캡슐화함으로써 코드에 확고한 기반이 있다는 확신을 가질 수 있습니다.

Simplicity에는 몇 가지 더 많은 조합자와 jet가 있으며, 이에 대해서는 이후 포스팅에서 설명하겠습니다. 언어를 구축하면서 좀 더 실용적인 예제를 살펴보고 프로그램의 속성을 '증명'한다는 것이 무엇을 의미하는지 살펴볼 것입니다.

다음 글에서는 두 개의 동일한 표현식을 하나로 병합할 수 있는 공유 개념을 소개하고 "동일하다"는 의미와 관련된 몇 가지 미묘한 점을 소개할 예정입니다.

GitHub의 Simplicity 토론에 참여하여 질문하고, 커뮤니티와 소통하고, 여러분의 인사이트를 공유하세요. 또한 트위터에서 @blksresearch 를 팔로우하여 Simplicity 블로그의 최신 포스팅을 확인하세요.