caSPESC2Vyper: Conformant and Automatic Generation from DeFi SPESC Legal Contract to Vyper Smart Contract

Abstract

Decentralized Finance (DeFi) can provide traditional financial services through blockchain and smart contract technology. The generation of DeFi smart contracts from DeFi legal contracts has become a hot topic. However, we found that current approaches for generating DeFi smart contracts from legal contracts fail to ensure conformance between the two. To address this, we propose caSPESC2Vyper, a method to generate Vyper smart contracts from SPESC legal contracts while guaranteeing conformance. First, we define the executable formal semantics K-SPESC. Next, we establish a syntactic structure mapping from the SPESC language to the Vyper language, based on which caSPESC2Vyper is implemented. Finally, we analyze the conformance and demonstrate that caSPESC2Vyper effectively ensures conformance between DeFi legal contracts and Vyper smart contracts.