위키원
미켈슨
테조스(Tezos)
미켈슨(Michelson)은 테조스(Tezos) 블록체인에 스마트 컨트랙트(Smart contract)를 작성하는데 사용되는 로우레벨(Low-Level) 스택 기반 프로그래밍 언어이다. 미켈슨은 테조스 블록체인에 스마트 계약서를 작성하는 데 사용되는 DSL(Domain-specific langauge)이다. 미켈슨은 스택 기반(stack-based) 언어이며 변수가 없고, 스택 지향(Stack-oriented) 언어는 하나 이상의 스택에서 작동하며 각 스택은 서로 다른 용도로 사용될 수 있다.
개요
미켈슨(Michelson) 프로그래밍 언어 는 스택 기반이며 다형성(polymorphism), 클로저(closures), 또는 명명 함수(named function)와 같은 기능이 포함되어 있지 않다. 리퀴디티(Liquidity)라는 고급프로그래밍을 작성하여 미켈슨(Michelson) 언어로 컴파일할 수 있다. 미켈슨(Michelson)의 언어의 구현은 오카멜(OCaml) GADT를 기반으로 한다. 미켈슨은 테 조스 블록체인에 Smart contract를 작성하는 데 사용되는 로우레벨(low-level) 스택 기반(stack-based) 프로그래밍 언어이다. 미켈슨은 사용자가 계약의 속성을 증명할 수 있게 하고 형식 검증(formal verification)을 용이하게 하기 위해 설계되었다. 스택 rewrite 패러다임을 사용하고 그에 따라 각 함수가 입력 스택을 출력 스택으로 다시 작성한다. 이것은 순전히 함수적(functional) 방식으로 실행되고 입력값을 전혀 수정하지 않았다. 따라서 모든 데이터 구조는 불변(immutable)한다.
특징
미켈슨(Michelson)은 손으로 쓸 수 있으며 컴파일러의 출력조차도 이해할 수 있게 한다는 목표로 알아보기 쉽게 설계되었다. 미켈슨(Michelson)을 사용하는 데 있어 두 가지의 중요한 동기가 있다. 첫 번째는 읽을 수 있는 바이트코드 를 제공하고, 두 번째는 자신이 잘못된 것이 무엇인지 알 수 있는 것이다. 로우레벨(Low-Level)의 바이트코드에서 프로그램과 컴파일러 툴에 대한 확신이 필요하다. 미켈슨(Michelson)을 사용하면 실행된 프로그램의 속성을 더욱 쉽게 검사하고 확인할 수 있다. 미켈슨(Michelson)의 현재 구현은 오카멜(OCaml) GADT를 기반으로 하며 언어의 정확성과 시간을 검증하는 데 사용한다. 또한 스택 기반 언어라 구현은 시멘틱에 직접 매핑된다.[1] 그리고 테조스(Tezos)에서 사용되고 있는 이 미켈슨(Michelson)과 오카멜(OCaml)의 프로그래밍 언어 는 빠른 속도와 높은 보안성 구현이 가능하다. 먼저 미켈슨(Michelson)은 세부적인 오류를 잡아내는데 특화된 언어로서 높은 보안성이 가능하다. 오카멜(OCaml)은 짧은 코드로 기능들을 구현할 수 있는 언어이기에 수정이 쉽고 빠르다. 두 프로그래밍 언어 는 스마트 컨트랙트 의 복잡한 코드를 더욱 쉽게 설계한 언어이다.[2]
- 리퀴디티, 미켈슨 차이점
- 리퀴디티(Liquidity)는 테조스(Tezos)를 위해 개발된 완전 함수형 프로그래밍 언어로 리퀴디티는 테조스에서 Smart contract를 프로그래밍하는 데 사용하는 고급 언어이고 완전 함수형 언어(fully functional language)이며, 리퀴디티는 OCaml의 문법(syntax)을 사용하며, Michelson의 보안 제한을 엄격히 준수한다. 리퀴디티는 100% Michelson의 특색을 가지며, 리퀴디티로 만들어진 계약은 메인 네트워크에 제출할 수 있다. 그럼 리퀴디티와 미켈슨의 차이점으로는 유동성이 있다. 유동성은 Michelson에서 엄격하게 컴파일(compile)된다. (프로그래밍) 언어로서 리퀴디티는 문법(syntax), 로컬 변수(local variables) 및 고급 타입(high-level type)을 사용하기 때문에 많은 개발자가 스택 조작(stack manipulation)보다는 쉽게 접근 할 수 있고 리퀴디티에 대한 형식-검증(Formal-verification) 프레임워크가 개발 중이다.
- 문자열 : 부호 있는 정수 및 부호 없는 정수, 단위, 곱, 합계, 옵션, 목록, 세트, 맵 및 고차 함수를 포함하여 공정한 내장 데이터 유형 세트가 있으나 사용자가 자신의 데이터 형식을 정의할 수 있는 방법은 없으며, 변수 나 루틴의 이름을 지정할 방법이 없다. 모든 것은 스택에서 데이터 구조를 탐색하여 액세스해야 한다.
- 미켈슨 단점 : 미켈슨을 사용하여 바로 작성하는 것이 가능하였으나, 변수의 유형이 적고 스택 기반의 문법들 때문에 쓰는 것도 읽기도 너무 어렵다는 단점이 있고, 추론 규칙은 단형인 유형을 할당하는데, 이는 각 항에 정확히 하나의 유형이 있다는 의미하며, 이것은 많은 유형에 작용하는 다형성 루틴인 함수형 프로그래밍에서 가장 성공적인 아이디어 중 하나를 생략한다. 파스칼의 안 좋은 시절로 돌아가는 것을 의미한다. 여기서 하나는 정수 목록을 정렬하기 위해 하나의 루틴을 작성하고 문자열 목록을 정렬하기 위해 다른 루틴을 작성해야 한다.[3]
미켈슨 언어{#michelson_KR}
- 미켈슨은 이상한 언어처럼 보이지만, 다형성(polymorphism), 클로저(closures) 또는 명명 함수(named function)와 같은 기능은 포함하지 않는다. 하스겔(Haskell)이나 오카멜(OCaml) 같은 언어와 비교할 때, 능력이 좀 부족한 것처럼 보이지만, 미켈슨의 스택이 항상 다루기 쉬운 것은 아니며 표준 라이브러리가 없다. 그러나 이러한 제한들은 언어의 디자인 목표에 따라 크게 영향을 받게 되는데, 미켈슨을 사용하는 데 있어서 아래와 같은 두 가지 주요한 동기가 있다.
- 읽을 수 있는 bytecode를 제공한다.
- 스스로를 잘못된 것이 무엇인지 알 수 있다(To be introspectable).
- 테조스는 Smart contract의 역할에 관해 이더리움(Ethereum)과 약간 다르다. 플랫폼을 일반적인 세계 컴퓨터보다는 특정 비즈니스 로직을 구현하는 방법으로 생각하고, 이더리움에서 대부분의 계약은 multisig wallet, 토큰 획득권(vesting) 및 배포 규칙 같은 것을 구현했는데 미켈슨도 이러한 유형의 애플리케이션을 구현하려고 한다. 메켈슨은 심지어 손으로도 쓸 수 있고 컴파일러의 출력조차도 이해할 수 있게 한다라는 목표로 알아보기 쉬운 컴파일러로 설계되었으며, 언어는 개발자가 자신의 분석 툴과 컴파일러를 개발자가 원하는 데로 만들 수 있도록 간단해야 한다. 이는 EVM의 에서 출발한 것이며, EVM의 바이트 코드는 어셈블리와 매우 유사하다. 낮은 수준의 바이트 코드에서는 프로그램과 컴파일러 툴체인에 대한 확신이 필요하지만, 미켈슨을 사용하면 실제로 실행된 프로그램의 속성을 더욱 쉽게 검사(verify)하고 확인(check)할 수 있다. 고급 바이트 코드를 사용하면 컴파일 출력물에 대한 속성을 증명하는 프로세스가 단순해지는데, 미켈슨으로 작성된 프로그램은 SMT solver로 적절하게 분석 할 수 있으며 분리 논리(Seperation logic)와 같은 더 복잡한 기법을 사용할 필요 없이 Coq로 형식화(formalize)된다. 마찬가지로 강제 들여쓰기(indentation)와 대문자 표기법(Capitalization)으로 인한 제한 사항으로 들여쓰기와 정렬 트릭으로 소스를 난독화할 수 없다.[4]
- 미켈슨의 현재 구현은 OCaml GADT를 기반으로 하고 있으며, OCaml GADT는 언어의 타입-적정성을(type-soundness) 검증하는 데 사용된다. 또한 스택 기반 언어의 구현은 시멘틱(의미론, Semantic)에 직접 매핑된다. lambda-calculus를 효율적으로 구현하는 경우에도 그대로 적용되고, 또한 공식적으로 검증된 미켈슨의 구현은 두 개가 있는데, 하나는 Coq에, 다른 하나는 F*에 구현되어 있다. 마지막으로, 테 조스의 주요 장점 중 하나는 시스템이 수정 가능하다(Amendable)는 것이다. 자신 있는 작은 코어 언어로 시작하여 좋은 use case가 만들어지면서 기능을 추가하고자 하고, 시작할 때 모든 것을 언어에 담고 이후의 호환성을 깨뜨리고 싶지 않다. 미켈슨은 비즈니스 로직을 위한 간단한 플랫폼을 제공하고, 이해하기 쉬운 바이트 코드를 제공하며, 스스로 잘못된 것이 뭔지 아는 것이 가능하도록 하고, 올린 쉬버(Olin Shivers)와 함께 일할 때, 그는 항상 작업을 위한 충분히 작은 도구를 사용하는 것을 매우 좋아했다. 미켈슨은 그런 도구가 되도록 조심스럽게 설계되었다.[4]
구성
- 미켈슨 프로그램 : 미켈슨 언어의 자세한 형식적 의미는 주어진 프로그램과 초기 스택에서 미켈슨 인터프리터가 수행하는 계산을 기호 방식으로 설명하여 해당 결과 스택을 생성한다. 미켈슨 인터프리터는 순수한 함수이다. 환경에 영향을 주지 않고 초기 요소의 요소에서만 결과 스택을 작성한다. 이 의미론은 자연스럽게 큰 단계 형태, 즉 재귀 참조 해석기의 상징적 정의로 제공된다. 이 정의는 인터프리터 (프로그램 및 스택)의 가능한 모든 입력을 다루고 해당 결과 스택의 계산을 설명하는 규칙 목록의 형식이다.[5]
- 규칙 양식 및 선택
> (syntax pattern) / (initial stack pattern) => (result stack pattern) iff (conditions) where (recursions) and (more recursions)
- => 이 부호의 왼쪽은 규칙을 선택하는 데 사용된다. 프로그램과 초기 스택이 주어지면 다음 프로세스를 사용하여 하나의 규칙 만 선택할 수 있으며, 프로그램의 최상위 구조는 구문 패턴과 일치해야 한다. 명령어 시퀀스를 처리할 수 있는 사소한 패턴이 거의 없고 나머지는 하나의 특정 명령어와 일치하는 사소한 패턴으로 만들어지기 때문에 이것은 매우 간단하다. 그런 다음 초기 스택은 초기 스택 패턴과 일치해야 하고 마지막으로, 일부 규칙은 iff 키워드 뒤에 오는 스택의 값보다 추가 조건을 추가한다. 때때로 주어진 규칙에 여러 규칙이 적용될 수 있으며, 이 경우에 사양에서 처음 나타나는 것이 선택된다. 규칙이 적용되지 않으면 결과는 명시적 규칙과 동일하고, 다음 섹션에서 설명하는 것처럼 형식이 잘 지정된 프로그램에서는 이 경우가 발생하지 않는다. 오른쪽은 규칙이 적용되는 경우 통역사의 결과, 스택 패턴으로 구성되며, 그 부분은 상수이거나 => 부호의 왼쪽에 이름이 지정된 컨텍스트 요소(프로그램 및 초기 스택)이다.[5]
- 재귀 규칙 (큰 단계 형식)
where (intermediate program) / (intermediate stack) => (partial result)
- 즉, 왼쪽의 중간 상태를 해석할 때 오른쪽에 패턴이 제공되는 경우에 규칙이 적용된다. 부호의 왼쪽 =>부호는 초기 상태의 요소 또는 다른 부분 결과로 구성되며 오른쪽은 규칙의 결과 스택을 작성하는 데 사용할 수 있는 부분을 식별하며, 부분 결과 패턴이 실제로 해석 결과와 일치하지 않으면 전체 규칙의 결과는 명시적 FAILWITH명령 의 결과와 동일하다. 이 절은 다음 섹션에서 설명하는 것처럼 형식이 잘 지정된 프로그램에서는 발생하지 않는다.[5]
패턴의 형식
- 코드 패턴
- INSTR(대문자 식별자)는 간단한 명령어 이다(예 :) DROP
- INSTR (arg) ...인수는 코드, 데이터 또는 유형 패턴 (예 :)일 수 있는 복합 명령어이다.PUSH nat 3
- { (instr);….}빈 시퀀스의 명령어일 수 있다. (예 :), 중첩된 시퀀스는 괄호를 삭제할 수 있다.IF { SWAP ; DROP } { DROP }
- name 는 모든 프로그램과 일치하는 패턴이며 결과를 빌드하는 데 사용할 수 있는 일치하는 프로그램의 일부이다.
- _ 모든 명령어와 일치하는 패턴이다.
- 스택 패턴
- [FAILED] 특수 실패 상태이다.
- [] 빈 스택이다.
- (top) : (rest)는 최상위 요소가 (top)왼쪽의 데이터 패턴과 일치하고 나머지 요소가 (rest)오른쪽의 스택 패턴과 일치하는 스택이다. (예 :) x : y : rest
- name 는 스택과 일치하고 결과를 빌드하는 데 사용하기 위해 이름을 지정하는 패턴이다.
- _ 모든 스택과 일치하는 패턴이다.
- 데이터 패턴
- 명령어 이름, 기호 상수 및 데이터 생성자 도메인은 이 사양으로 고정되어 있으며, 미켈슨은 프로그래머가 자신의 유형을 소개하도록 허용하지 않고, 사양에 사용된 구문은 구체적인 구문과 약간 다를 수 있다. 특히 일부 명령어에는 유형 검사기에 의해 합성되므로 구체적인 언어로 표시되지 않는 유형이 주석으로 표시된다.
- 정수 / 자연수 리터럴(예 :) 3
- 문자열 리터럴(예 "contents")
- 원시 바이트 시퀀스 리터럴(예 0xABCDEF42)
- Tag(대문자)는 기호 상수이다. (예를 들어 Unit, True, False)
- (Tag (arg) .)태그가 생성된 데이터(예 :)(Pair 3, 4)
- 퍼스트 클래스 코드 값의 코드 패턴
- name 값을 사용하여 결과를 작성하는 데 사용한다.
- _ 모든 값과 일치한다.
타입 시스템 표기법
- 유형 표기법
- 값 유형, 용어 및 스택에 대한 표기법을 소개하면, 언어 전체 중 일부 위치에서 형식 주석 형태로 나타나는 값 형식의 하위 집합 외에도 이 형식 언어는 사양에만 존재한다는 것을 이해하는 것이 중요하다. 스택 유형으로는 다음과 같다.
- [] 빈 스택
- (top) : (rest)첫 번째 값이 type (top)이고 queue가 stack type인 스택의 경우 (rest)
- 언어의 지시 사항, 프로그램 및 프리미티브도 입력되며 해당 유형이 작성된다.
(type of stack before) -> (type of stack after)
- 스택의 값 유형은 다음과 같다.
- identifier프리미티브 데이터 유형(예 :) bool
- identifier (arg)매개 변수 유형이 하나인 파라 메트릭 데이터 유형 (arg)(예 :) list nat
- identifier (arg) ...여러 파라미터들 (예를 들면 파라 메트릭 데이터 유형 )map string int
- [ (type of stack before) -> (type of stack after) ]코드 인용 (예에 대한 )[ int : int : [] -> int : [] ]
- lambda (arg) (ret)에 대한 바로 가기이다. [ (arg) : [] -> (ret) : [] ]
- 메타 형 변수
- 타이핑 규칙은 메타 타입 변수를 도입한다. 분명히, 이것은 미켈슨이 가지고 있지 않은 다형성과 관련이 없다. 이러한 변수는 사양 수준에서만 존재하며 프로그램 부분 간의 일관성을 나타내는 데 사용되며, 예를 들어 IF구문에 대한 타이핑 규칙은 메타 변수를 도입하여 두 가지 모두 동일한 유형을 가져야 함을 나타낸다.
- 메타 유형 변수에 대한 표기법은 다음과 같습니다.
- 'a 유형 변수의 경우
- 'A 스택 유형 변수의 경우
- _ 익명 타입 또는 스택 타입 변수
활용
- 미켈슨(Michelson) 언어
- 미켈슨(Michelson) 언어는 스마트 계약의 수학적 코드의 정확성을 검증하는 데 필요한 간단한 트랜잭션 의 논리적 프로세스와 시스템의 간단한 관리를 위해 사용된다. 또, 다중 서명 지갑(multi-signal wallets), 권리 부여 및 분배(vesting and distribution)와 같은 사업을 도와주는 데 집중하고 있으며, 이를 다른 언어에 비해 쉽고 누구나 사용할 수 있게 만들어져 있다. 또한, 테조스(Tezos)만의 특징인 스스로 수정해나가는 점과 같이 미켈슨(Michelson) 언어도 천천히 확장해 나가며 기능들을 추가함을 계획하고 있다.[6]
- 오카멜 언어
- 미켈슨, 오카멜 언어는 테조스 블록체인에서 스마트계약을 기록하기 위한 언어이다. 두 언어 모두 스마트계약의 코드를 수학적으로 구현하는 데 특화됐으며, 간단한 코드로 설계된 언어인 만큼 수정하기 쉽다. 이 자체 언어들은 수정도 쉽지만, 안정적이라는 장점도 있고, 원조 블록체인인 비트코인의 C++ 언어는 그간 버그(프로그램 오류) 발생 가능성이 있다는 지적을 받았다. 버그가 악용될 경우 블록체인 네트워크가 마비될 수 있기 때문에 보안에도 악영향을 끼치며, 보안이 흔들리는 플랫폼 위에서 디앱들은 안정적으로 구축될 수 없다. 그러나 앞서 말했듯 테조스의 미켈슨, 오카멜 언어는 스마트계약의 코드를 수학적으로 증명하기에 적합하며, 이는 보안을 향상하는 데 이용되는 기술인 공식검증을 가능하게 하고, 버그 발생 가능성을 낮춘다. 디앱들이 보다 안정적으로 자리 잡을 수 있게 되는 것이고 테조스가 스마트계약과 댑(DApp)을 위한 플랫폼을 내세울 수 있는 이유다.[7]
각주
- ↑ ㈜테조스코리아 공식 커뮤니티 - https://tezoskoreacommunity.org/
- ↑ 코인원, 〈(코인원의 코인스낵) 1. 스스로 진화하는 블록체인, 테조스(Tezos)〉, 《네이버블로그》, 2018-10-12
- ↑ Philip Wadler, 〈Simplicity and Michelson〉, 《에든버러》
- ↑ 4.0 4.1 고영준, 〈Tezos Smart Contracts에 대한 소개 {#faq_KR}〉, 《테조스코리아커뮤니티》
- ↑ 5.0 5.1 5.2 Nomadic Labs, 〈Michelson: Tezos 스마트 계약의 언어〉, 《테조스 개발자문서》
- ↑ areyoucrazy, 〈테조스의 특징을 초보자의 눈높이에 맞게 이야기해보았습니다.〉, 《스팀잇》, 2018-02-20
- ↑ 박현영 기자, 〈[신비한 코인사전<22> 하드포크 필요 없는 블록체인 '테조스']〉, 《서울경제》, 2018-10-02
참고자료
- ㈜테조스코리아 공식 커뮤니티 - https://tezoskoreacommunity.org/
- areyoucrazy, 〈테조스의 특징을 초보자의 눈높이에 맞게 이야기해보았습니다.〉, 《스팀잇》, 2018-02-20
- 박현영 기자, 〈(신비한 코인사전)<22> 하드포크 필요 없는 블록체인 '테조스'〉, 《서울경제》, 2018-10-02
- 코인원, 〈(코인원의 코인스낵) 1. 스스로 진화하는 블록체인, 테조스(Tezos)〉, 《네이버블로그》, 2018-10-12
- Skkrypto, 〈(TezosXSkkrypto) 테조스 실습노트 #6〉, 《브런치》, 2019-05-06
- 고영준, 〈Tezos Smart Contracts에 대한 소개 {#faq_KR}〉, 《테조스코리아커뮤니티》
- Nomadic Labs, 〈Michelson: Tezos 스마트 계약의 언어〉, 《테조스 개발자문서》
- Philip Wadler, 〈Simplicity and Michelson〉, 《에든버러》
같이 보기
이 문서는 로고 수정이 필요합니다.
