Simplicity

핵심은 수학적으로 정의된 denotational semantics와 operational semantics를 갖는 작은 typed combinator 집합이다. Rocq의 형식 model을 통해 언어, 구현, 특정 program 속성에 관한 증명을 기계로 확인할 수 있다. [1]

이 언어에는 무한 loop나 일반 재귀가 없어 실행 전에 계산, memory, data의 상한을 구할 수 있다. 따라서 program이 알 수 없는 gas 소모에서 멈추거나 영원히 실행되어서는 안 된다. [1]

Program은 merklized expression tree이며 쓰지 않는 branch는 지출할 때 그 Merkle root로 대체할 수 있다. Validator는 전체 program에 대한 commitment를 확인하지만 on-chain에는 필요한 path와 witness data만 공개된다. [1]

Jet은 특정 Simplicity expression을 인식해 최적화된 native function으로 실행한다. Consensus 안전을 위해 결과는 expression의 reference semantics와 정확히 같아야 하며 jet이 숨은 새 의미를 더하지 않는다. [1]

libSimplicity에는 C의 최소 consensus-sensitive runtime, Haskell의 reference와 generator 부분, Rocq의 형식 model이 들어 있다. 각 layer는 서로 점검하지만 repository는 언어와 구현이 계속 개발 중이라고 명시한다. [2]

SimplicityHL은 Simplicity bytecode로 compile되는 더 읽기 쉬운 Rust 유사 언어다. Project 자체가 work in progress이며 production-ready가 아니라고 밝힌다. Contract audit은 source, compiler, bytecode, witness, jets를 모두 다뤄야 한다. [3]

Simplicity는 2025년에 Liquid mainnet에 배포됐다. Liquid는 여러 asset과 Confidential Transactions를 지원하는 federated sidechain이므로 이 배포는 Bitcoin mainnet consensus의 activation이 아니며, 거기에는 별도 proposal과 soft fork가 필요하다. [4]

형식 의미론이 올바른 경제적 의도, 안전한 key, 신뢰할 counterparty를 보장하지 않는다. 검증할 때 저수준 program, SimplicityHL tooling, 구체적인 jet set, Liquid version, 가상의 Bitcoin integration을 구분해야 한다. [2]