vm.py 8.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312
  1. import argparse
  2. import sys
  3. from enum import Enum
  4. def eprint(*args):
  5. print(*args, file=sys.stderr)
  6. class Line:
  7. def __init__(self, text, line_number):
  8. self.text = text
  9. self.orig = text
  10. self.lineno = line_number
  11. self.clean()
  12. def clean(self):
  13. # Remove the comments
  14. self.text = self.text.split("#", 1)[0]
  15. # Remove whitespace
  16. self.text = self.text.strip()
  17. def is_empty(self):
  18. return bool(self.text)
  19. def __repr__(self):
  20. return "Line %s: %s" % (self.lineno, self.orig.lstrip())
  21. def command(self):
  22. if not self.is_empty():
  23. return None
  24. return self.text.split(" ")[0]
  25. def args(self):
  26. if not self.is_empty():
  27. return None
  28. return self.text.split(" ")[1:]
  29. def clean(contents):
  30. # Split input into lines
  31. contents = contents.split("\n")
  32. contents = [Line(line, i) for i, line in enumerate(contents)]
  33. # Remove empty blank lines
  34. contents = [line for line in contents if line.is_empty()]
  35. return contents
  36. def divide_sections(contents):
  37. state = "NOSCOPE"
  38. segments = {}
  39. current_segment = []
  40. contract_name = None
  41. for line in contents:
  42. if line.command() == "contract":
  43. if len(line.args()) != 1:
  44. eprint("error: missing contract name")
  45. eprint(line)
  46. return None
  47. contract_name = line.args()[0]
  48. if state == "NOSCOPE":
  49. assert not current_segment
  50. state = "INSCOPE"
  51. continue
  52. else:
  53. assert state == "INSCOPE"
  54. eprint("error: double contract entry violation")
  55. eprint(line)
  56. return None
  57. elif line.command() == "end":
  58. if len(line.args()) != 0:
  59. eprint("error: end takes no args")
  60. eprint(line)
  61. return None
  62. if state == "NOSCOPE":
  63. eprint("error: missing contract start for end")
  64. eprint(line)
  65. return None
  66. else:
  67. assert state == "INSCOPE"
  68. state = "NOSCOPE"
  69. segments[contract_name] = current_segment
  70. current_segment = []
  71. continue
  72. elif state == "NOSCOPE":
  73. # Ignore lines outside any contract
  74. continue
  75. current_segment.append(line)
  76. if state != "NOSCOPE":
  77. eprint("error: reached end of file with unclosed scope")
  78. return None
  79. return segments
  80. alloc_commands = {
  81. "param": 1,
  82. "private": 1,
  83. "public": 1,
  84. }
  85. op_commands = {
  86. "set": 2,
  87. "mul": 2,
  88. }
  89. constraint_commands = {
  90. "lc0_add": 1,
  91. "lc1_add": 1,
  92. "lc2_add": 1,
  93. "lc0_add_one": 0,
  94. "lc1_add_one": 0,
  95. "lc2_add_one": 0,
  96. "enforce": 0,
  97. }
  98. def extract_relevant_lines(contract, commands_table):
  99. relevant_lines = []
  100. for line in contract:
  101. command = line.command()
  102. if command not in commands_table.keys():
  103. continue
  104. define = commands_table[command]
  105. if len(line.args()) != define:
  106. eprint("error: wrong number of args")
  107. return None
  108. relevant_lines.append(line)
  109. return relevant_lines
  110. class VariableType(Enum):
  111. PUBLIC = 1
  112. PRIVATE = 2
  113. class Variable:
  114. def __init__(self, symbol, index, type, is_param):
  115. self.symbol = symbol
  116. self.index = index
  117. self.type = type
  118. self.is_param = is_param
  119. def __repr__(self):
  120. return "<Variable %s:%s>" % (self.symbol, self.index)
  121. def generate_alloc_table(contract):
  122. relevant_lines = extract_relevant_lines(contract, alloc_commands)
  123. alloc_table = {}
  124. for i, line in enumerate(relevant_lines):
  125. assert len(line.args()) == 1
  126. symbol = line.args()[0]
  127. command = line.command()
  128. if command == "param":
  129. type = VariableType.PRIVATE
  130. is_param = True
  131. elif command == "private":
  132. type = VariableType.PRIVATE
  133. is_param = False
  134. elif command == "public":
  135. type = VariableType.PUBLIC
  136. is_param = False
  137. else:
  138. assert False
  139. alloc_table[symbol] = Variable(symbol, i, type, is_param)
  140. return alloc_table
  141. def symbols_list_to_indexes(line, alloc):
  142. indexes = []
  143. for symbol in line.args():
  144. if symbol not in alloc:
  145. eprint("error: missing unallocated symbol")
  146. eprint(line)
  147. return None
  148. # Lookup variable index
  149. index = alloc[symbol].index
  150. indexes.append(index)
  151. return indexes
  152. class Operation:
  153. def __init__(self, line, indexes):
  154. self.command = line.command()
  155. self.args = indexes
  156. self.line = line
  157. def generate_ops_table(contract, alloc):
  158. relevant_lines = extract_relevant_lines(contract, op_commands)
  159. ops = []
  160. for line in relevant_lines:
  161. indexes = symbols_list_to_indexes(line, alloc)
  162. ops.append(Operation(line, indexes))
  163. return ops
  164. class Constraint:
  165. def __init__(self, line, indexes):
  166. self.command = line.command()
  167. self.args = indexes
  168. self.line = line
  169. def args_comment(self):
  170. return ", ".join("%s" % symbol for symbol in self.line.args())
  171. def generate_constraints_table(contract, alloc):
  172. relevant_lines = extract_relevant_lines(contract, constraint_commands)
  173. constraints = []
  174. for line in relevant_lines:
  175. indexes = symbols_list_to_indexes(line, alloc)
  176. constraints.append(Constraint(line, indexes))
  177. return constraints
  178. class Contract:
  179. def __init__(self, alloc, ops, constraints):
  180. self.alloc = alloc
  181. self.ops = ops
  182. self.constraints = constraints
  183. def __repr__(self):
  184. repr_str = ""
  185. repr_str += "Alloc table:\n"
  186. for symbol, variable in self.alloc.items():
  187. repr_str += " // %s\n" % symbol
  188. repr_str += " %s %s\n" % (variable.type, variable.index)
  189. repr_str += "Operations:\n"
  190. for op in self.ops:
  191. repr_str += " // %s\n" % op.line
  192. repr_str += " %s %s\n" % (op.command, op.args)
  193. repr_str += "Constraints:\n"
  194. for constraint in self.constraints:
  195. if constraint.args:
  196. repr_str += " // %s\n" % constraint.args_comment()
  197. repr_str += " %s %s\n" % (constraint.command, constraint.args)
  198. return repr_str
  199. def compile(contract, constants):
  200. # Allocation table
  201. # symbol: Private/Public, is_param, index
  202. alloc = generate_alloc_table(contract)
  203. # Operations lines list
  204. if (ops := generate_ops_table(contract, alloc)) is None:
  205. return None
  206. # Constraint commands
  207. if (constraints := generate_constraints_table(contract, alloc)) is None:
  208. return None
  209. return Contract(alloc, ops, constraints)
  210. def process(contents):
  211. # Remove left whitespace
  212. contents = clean(contents)
  213. # Parse all constants
  214. constants = [line for line in contents if line.command() == "constant"]
  215. # Divide into contract sections
  216. if (pre_contracts := divide_sections(contents)) is None:
  217. return None
  218. # Process each contract
  219. contracts = {}
  220. for contract_name, pre_contract in pre_contracts.items():
  221. if (contract := compile(pre_contract, constants)) is None:
  222. return None
  223. contracts[contract_name] = contract
  224. return contracts
  225. def main(argv):
  226. parser = argparse.ArgumentParser()
  227. parser.add_argument("filename", help="VM PISM file: proofs/vm.pism")
  228. group = parser.add_mutually_exclusive_group()
  229. group.add_argument('--display', action='store_true',
  230. help="show the compiled code in human readable format")
  231. group.add_argument('--rust', action='store_true',
  232. help="output compiled code to rust for testing")
  233. args = parser.parse_args()
  234. src_filename = args.filename
  235. contents = open(src_filename).read()
  236. if (contracts := process(contents)) is None:
  237. return -2
  238. def default_display():
  239. for contract_name, contract in contracts.items():
  240. print("Contract:", contract_name)
  241. print(contract)
  242. if args.display:
  243. default_display()
  244. elif args.rust:
  245. import vm_export_rust
  246. for contract_name, contract in contracts.items():
  247. vm_export_rust.display(contract)
  248. else:
  249. default_display()
  250. return 0
  251. if __name__ == "__main__":
  252. sys.exit(main(sys.argv))