Tezos Smart Contracts에 대한 소개

Michelson이 무엇인가요?

Michelson은 Tezos 블록체인에 스마트 계약서를 작성하는 데 사용되는 DSL(Domain-specific langauge)입니다. Michelson은 스택 기반(stack-based) 언어이며 변수가 없습니다. 스택 지향(Stack-oriented) 언어는 하나 이상의 스택에서 작동하며 각 스택은 서로 다른 용도로 사용될 수 있습니다.

이 링크는 Michelson documentation(영문)과 관련된 링크입니다. 이 링크는 Michelson 튜토리얼 시리즈(영문) 으로 camlCase애서 만들어졌습니다.

Liquidity는 무엇인가요?

Liquidity는 Tezos에서 Smart contract를 프로그래밍하는 데 사용하는 고급 언어(High level language)이고 완전 함수형 언어(fully functional language)입니다. Liquidity는 OCaml의 문법(syntax)을 사용하며, Michelson의 보안 제한을 엄격히 준수합니다. Liquidity는 100% Michelson의 특색을 가지며, Liquidity로 만들어진 계약은 메인 네트워크에 제출 가능합니다. 개발자는 현재 Liquidity로 만들어진 Smart contract의 정확성(correctness)을 증명하는 데 사용될 공식 메소드(formal-method) 프레임워크를 개발 중입니다.

Liquidity 와 Michelson의 차이점은 무엇인가요?

유동성은 Michelson에서 엄격하게 컴파일(compile) 됩니다. (프로그래밍)언어로서 Liquidity는 문법(syntax), 로컬 변수(local variables) 및 고급 타입(high-level type)을 사용하기 때문에 많은 개발자들이 스택 조작(stack manipulation)보다는 쉽게 접근 할 수 있습니다. Liquidity에 대한 형식-검증(Formal-verification) 프레임워크가 개발 중입니다.

Tezos 프로로토콜의 프로그래밍 언어인 OCaml은 무엇인가요??

Tezos 프로토콜은 표현이 풍부하고 (expressivness) 안전성을 중시하는 범용적이고 고성능(industrial-strength) 프로그래밍 언어 인 OCaml로 구현 되었습니다. 속도가 중요하고 실수 하나가 수백만 달러의 비용이 될 수있는 기업에서 선택하는 기술입니다. Ocaml 라이브러리는 Python이나 Perl과 같은 많은 어플리케이션에서 사용할 수있는 대형 표준 라이브러리가 있으며 대규모 소프트웨어 엔지니어링에 적용 할 수있는 견고한 모듈(robust modular)과 객체 지향 프로그래밍 구조가 있습니다. Facebook, Bloomberg, Docker, Jane Street 같은 상위 기업들이 OCaml을 사용합니다.

함수형 프로그래밍(functional programming)은 무엇인가요? 다른 (프로그래밍) 패러다임과의 차이는 무엇인가요?

함수형 프로그래밍(Functional programming)은 프로그래밍 패러다임 입니다. — 함수형 프로그래밍은 computation을 수학 함수의 값을 구하는것으로(evaluation) 간주하고 상태(state) 및 변경 가능한(mutable) 데이터 변경을 방지합니다.

이것은 선언적(declarative) 프로그래밍 패러다임으로, 프로그래밍이 문장 대신 표현식(expression)이나 선언(declaration)으로 수행된다는 것을 의미합니다. 함수형 코드(functional code)에서 함수의 출력 값은 함수에 전달 된 변수(argument)에만 의존합니다. 그러므로 변수 x에 대해 동일한 값을 갖는 함수 f를 두 번 호출하면 매번 동일한 결과인 f(x)가 생성됩니다. 이것은 로컬(local) 또는 전역 상태(global state)에 의존하는 프로시저(procedure)와는 달리 동일한 인수를 사용했지만 다른 프로그램 상태 일 때 다른 시간에 다른 결과를 만들 수 있습니다. 사이드 이펙트를 제거하면 즉 ,상태의 변화(change in state)가 함수 입력에 의존하지 않게 하면, 함수 프로그래밍 개발의 핵심 동기(key motivation) 중 하나인 프로그램의 동작 이해와 예측을 훨씬 쉽게 할 수 있습니다.

이래의 그림은 EVM(Ethereum Virtual Machine), WASM(Web Assembly) 및 Michelson 간의 고수준(high level)에서의 차이점을 보여주는 다이어그램입니다.

Michelson Language

소개

Michelson은 Tezos 블록체인에 Smart contract를 작성하는 데 사용되는 로우레벨(low-level) 스택 기반(stack-based) 프로그래밍 언어입니다. Michelson은 사용자가 계약의 속성을 증명할 수 있게하고 형식 검증(formal verification)을 용이하게하기 위해 설계되었습니다.

스택 rewrite 패러다임을 사용하고 그에 따라 각 함수가 입력 스택을 출력 스택으로 다시 작성합니다. (이에 대한 의미는 밑에서 완전히 설명 할 것입니다.) 이것은 순전히 함수적(functional) 방식으로 실행되고 입력값을 전혀 수정하지 않습니다. 따라서 모든 데이터 구조는 불변(immutable) 합니다.

Stack은 무엇인가요?

스택은 Collection에 인자를 추가하는 푸시(push) 와 아직 제거되지 않은 가장 최근에 추가 된 요소를 제거하는 팝(pop)의 두 가지 기본 조작으로 element collection의 역할을 하는 추상 데이터 타입(abstract data type)입니다. 인자(element)가 스택에서 빠져나오는 순서는 LIFO (last in, first out)입니다. 더해서 peek 오퍼레이션은 스택을 수정하지 않고도 스택의 상단에 액세스 할 수 있습니다.

출처: Wikipedia.

Stack 다시 쓰기

스택을 다시 작성하는 것(rewrite)이 무슨 의미인지 확인하기 위해서, Michelson에서 트랜잭션을 실행해볼 것입니다. 첫번째로 트랜잭션이 실행되기 전에 특정 해시의 블록체인 상태가 deserialize되어 변수storage로 스택에 담습니다. amount라는 트랜잭션 데이터를 받을 from 함수와 첨부 된 ꜩ의 양,함수의 매개변수인 parameter 를 가지고 있습니다. (형태를 소스코드로 나타내자면 아래와 같습니다. - 역자 주)

from [ (Pair (Pair amount parameter) storage) ]

스택을 갱신하지 않고 함수를 실행 한 후에 프로그램은 함수의 결과 인result 매개 변수와 직렬화(serialized)되어 블록체인에 저장되는storage 출력을 호출하는to 함수를 호출합니다. (이상의 설명을 소스코드로 나타내면 아래와 같습니다.- 역자 주)

to [ (Pair result storage) ]

이 예시에서는 Michelson이 스택을 함수적으로 조작만 하고 새로운 스택을 함수와 함수사이에 전달합니다.

"왜 Michelson 이죠?" (by Milo Davis)

처음 볼때는 Michelson은 이상한 언어처럼 보입니다. 다형성(polymorphism), 클로저(closures) 또는 명명 함수(named function)와 같은 기능은 포함하지 않습니다. Haskell이나 OCaml 같은 언어와 비교할 때, 능력이 좀 부족한 것처럼 보였습니다. (Michelson의) 스택이 항상 다루기 쉬운 것은 아니며 표준 라이브러리가 없습니다. 그러나 이러한 제한들은 언어의 디자인 목표에 의해 크게 영향을 받게 됩니다.

Michelson을 사용하는데 있어서 아래와 같은 두가지 주요한 동기가 있습니다.

  1. 읽을수 있는 bytecode를 제공함
  2. 스스로를 잘못된 것이 무엇인지 알수 있음 (To be introspectable)

Tezos는 Smart contract의 역할에 관해 Ethereum과 약간 다른 시각을 취합니다. 우리는 플랫폼을 일반적인 "세계 컴퓨터"보다는 특정 비즈니스 로직을 구현하는 방법으로 생각합니다. Ethereum에서 대부분의 계약은 multisig wallet, 토큰 획득권(vesting) 및 배포규칙 같은 것을 구현했는데 Michelson도 이러한 유형의 어플리케이션을 구현하려고 합니다.

Michelson은 심지어 손으로도 쓸 수 있고 컴파일러의 출력조차도 이해할 수 있게 한다라는 목표로 알아보기 쉬운 컴파일러로 설계 되었습니다. 언어는 개발자가 자신의 분석 툴과 컴파일러를 개발자가 원하는데로 만들 수 있도록 간단해야 합니다. 이는 EVM의 에서 출발한 것이며, EVM의 바이트 코드는 어셈블리와 매우 유사합니다. 로우 레벨의 바이트 코드에서는 프로그램과 컴파일러 툴체인에 대한 확신이 필요합니다. Michelson을 사용하면 실제로 실행 된 프로그램의 속성을 보다 쉽게 ​​검사(verify)하고 확인(check)할 수 있습니다.

고급 바이트 코드를 사용하면 컴파일 출력물에 대한 속성을 증명하는 프로세스가 단순해집니다. Michelson으로 작성된 프로그램은 SMT solver로 적절하게 분석 할 수 있으며 분리논리(Seperation logic)와 같은 더 복잡한 기법을 사용할 필요없이 Coq로 형식화(formalize)됩니다. 마찬가지로 강제 들여쓰기(indentation)와 대문자 표기법(Capitalization)으로 인한 제한 사항으로 들여쓰기와 정렬 트릭으로 소스를 난독화할 수 없습니다.

Michelson의 현재 구현은 OCaml GADT를 기반으로 합니다. OCaml GADT는 언어의 타입-적정성을(type-soundness) 검증하는 데 사용됩니다. 또한 스택 기반 언어의 구현은 시멘틱(의미론, Semantic)에 직접 매핑됩니다. lambda-calculus를 효율적으로 구현하는 경우에도 그대로 적용됩니다. 또한 공식적으로 검증된 Michelson의 구현은 두개가 있습니다. 하나는 Coq에, 다른 하나는 F*에 구현되어 있습니다. 언젠가 현재 구현을 검증 된 구현체로 대체할 수 있었으면 합니다.

마지막으로, Tezos의 주요장점 중 하나는 시스템이 수정 가능하다(Amendable)는 것입니다. 우리는 자신 있는 작은 코어 언어로 시작하여 좋은 use case가 만들어지면서 기능을 추가하고자합니다. 우리는 시작할때 모든 것을 언어에 담고 이후의 호환성을 깨뜨리고 싶지 않습니다.

자 그렇다면 왜 Michelson인가요? Michelson은 비즈니스 로직을 위한 간단한 플랫폼을 제공하고, 이해하기 쉬운 바이트 코드를 제공하며, 스스로 잘못된 것이 뭔지 아는것이 가능하도록 합니다. 올린 쉬버(Olin Shivers)와 함께 일할 때, 그는 항상 "작업을 위한 충분히 작은 도구"를 사용하는 것을 매우 좋아했습니다. Michelson은 그런 도구가 되도록 조심스럽게 설계되었습니다.

Liquidity

Liqudity는 Tezos에서 Smart contract를 프로그래밍하는 고급(high-level)언어입니다. 완전한 함수형 언어이며 OCaml의 문법(syntax)을 사용하며 Michelson의 보안 제한 사항을 엄격히 준수합니다.

개발자들은 현재 Liquidity로 작성된 Smart contract의 정확성(Correctness)을 증명하는 데 사용할 공식-메소드(formal-method) 프레임워크를 개발 중입니다.

Liquidity 는 다음과 같은 특징이 있습니다.

  • Michelson 언어의 전체 범위 : Michelson에서 작성할 수있는 모든 것은 Liquidity에서도 작성가능 합니다,
  • 스택 조작(Stack manipulation) 대신 로컬 변수(Local variables) : 값을 로컬 변수에 저장할 수 있습니다.
  • 고급 타입 : Liquidity 프로그램에 합계 타입(sum-type) 및 레코드 타입(record-type)과 같은 타입을 정의하고 사용할 수 있습니다.

Liquidity는 이미 모든 Michelson 기능을 커버하며 Liquidity으로 만들어진 Smart contract는 현재 메인넷(Mainnet) 과 제로넷(zeroent)에 제출할 수 있습니다.

프로그래밍 언어 Resources

Michelson:

Liquidity:

OCaml: