vm.py 12 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430
  1. import argparse
  2. import sys
  3. from enum import Enum
  4. alloc_commands = {
  5. "param": 1,
  6. "private": 1,
  7. "public": 1,
  8. }
  9. op_commands = {
  10. "set": 2,
  11. "mul": 2,
  12. "add": 2,
  13. "sub": 2,
  14. "divide": 2,
  15. "load": 2,
  16. "local": 1,
  17. }
  18. constraint_commands = {
  19. "lc0_add": 1,
  20. "lc1_add": 1,
  21. "lc2_add": 1,
  22. "lc0_sub": 1,
  23. "lc1_sub": 1,
  24. "lc2_sub": 1,
  25. "lc0_add_one": 0,
  26. "lc1_add_one": 0,
  27. "lc2_add_one": 0,
  28. "lc0_add_coeff": 2,
  29. "lc1_add_coeff": 2,
  30. "lc2_add_coeff": 2,
  31. "enforce": 0,
  32. }
  33. def eprint(*args):
  34. print(*args, file=sys.stderr)
  35. class Line:
  36. def __init__(self, text, line_number):
  37. self.text = text
  38. self.orig = text
  39. self.lineno = line_number
  40. self.clean()
  41. def clean(self):
  42. # Remove the comments
  43. self.text = self.text.split("#", 1)[0]
  44. # Remove whitespace
  45. self.text = self.text.strip()
  46. def is_empty(self):
  47. return bool(self.text)
  48. def __repr__(self):
  49. return "Line %s: %s" % (self.lineno, self.orig.lstrip())
  50. def command(self):
  51. if not self.is_empty():
  52. return None
  53. return self.text.split(" ")[0]
  54. def args(self):
  55. if not self.is_empty():
  56. return None
  57. return self.text.split(" ")[1:]
  58. def clean(contents):
  59. # Split input into lines
  60. contents = contents.split("\n")
  61. contents = [Line(line, i) for i, line in enumerate(contents)]
  62. # Remove empty blank lines
  63. contents = [line for line in contents if line.is_empty()]
  64. return contents
  65. def divide_sections(contents):
  66. state = "NOSCOPE"
  67. segments = {}
  68. current_segment = []
  69. contract_name = None
  70. for line in contents:
  71. if line.command() == "contract":
  72. if len(line.args()) != 1:
  73. eprint("error: missing contract name")
  74. eprint(line)
  75. return None
  76. contract_name = line.args()[0]
  77. if state == "NOSCOPE":
  78. assert not current_segment
  79. state = "INSCOPE"
  80. continue
  81. else:
  82. assert state == "INSCOPE"
  83. eprint("error: double contract entry violation")
  84. eprint(line)
  85. return None
  86. elif line.command() == "end":
  87. if len(line.args()) != 0:
  88. eprint("error: end takes no args")
  89. eprint(line)
  90. return None
  91. if state == "NOSCOPE":
  92. eprint("error: missing contract start for end")
  93. eprint(line)
  94. return None
  95. else:
  96. assert state == "INSCOPE"
  97. state = "NOSCOPE"
  98. segments[contract_name] = current_segment
  99. current_segment = []
  100. continue
  101. elif state == "NOSCOPE":
  102. # Ignore lines outside any contract
  103. continue
  104. current_segment.append(line)
  105. if state != "NOSCOPE":
  106. eprint("error: reached end of file with unclosed scope")
  107. return None
  108. return segments
  109. def extract_relevant_lines(contract, commands_table):
  110. relevant_lines = []
  111. for line in contract:
  112. command = line.command()
  113. if command not in commands_table.keys():
  114. continue
  115. define = commands_table[command]
  116. if len(line.args()) != define:
  117. eprint("error: wrong number of args")
  118. return None
  119. relevant_lines.append(line)
  120. return relevant_lines
  121. class VariableType(Enum):
  122. PUBLIC = 1
  123. PRIVATE = 2
  124. class Variable:
  125. def __init__(self, symbol, index, type, is_param):
  126. self.symbol = symbol
  127. self.index = index
  128. self.type = type
  129. self.is_param = is_param
  130. def __repr__(self):
  131. return "<Variable %s:%s>" % (self.symbol, self.index)
  132. def generate_alloc_table(contract):
  133. relevant_lines = extract_relevant_lines(contract, alloc_commands)
  134. alloc_table = {}
  135. for i, line in enumerate(relevant_lines):
  136. assert len(line.args()) == 1
  137. symbol = line.args()[0]
  138. command = line.command()
  139. if command == "param":
  140. type = VariableType.PRIVATE
  141. is_param = True
  142. elif command == "private":
  143. type = VariableType.PRIVATE
  144. is_param = False
  145. elif command == "public":
  146. type = VariableType.PUBLIC
  147. is_param = False
  148. else:
  149. assert False
  150. if symbol in alloc_table:
  151. eprint("error: duplicate symbol '%s'" % symbol)
  152. eprint(line)
  153. return None
  154. alloc_table[symbol] = Variable(symbol, i, type, is_param)
  155. return alloc_table
  156. class Operation:
  157. def __init__(self, line, indexes):
  158. self.command = line.command()
  159. self.args = indexes
  160. self.line = line
  161. class VariableRefType(Enum):
  162. AUX = 1
  163. LOCAL = 2
  164. CONST = 3
  165. class VariableRef:
  166. def __init__(self, type, index):
  167. self.type = type
  168. self.index = index
  169. def __repr__(self):
  170. return "%s(%s)" % (self.type.name, self.index)
  171. def symbols_list_to_refs(line, alloc, local_vars, constants):
  172. indexes = []
  173. for symbol in line.args():
  174. if symbol in alloc:
  175. # Lookup variable index
  176. index = alloc[symbol].index
  177. index = VariableRef(VariableRefType.AUX, index)
  178. elif symbol in local_vars:
  179. index = local_vars[symbol]
  180. index = VariableRef(VariableRefType.LOCAL, index)
  181. elif symbol in constants:
  182. index = constants[symbol][0]
  183. index = VariableRef(VariableRefType.CONST, index)
  184. else:
  185. eprint("error: missing unallocated symbol '%s'" % symbol)
  186. eprint(line)
  187. return None
  188. indexes.append(index)
  189. return indexes
  190. def generate_ops_table(contract, alloc, constants):
  191. relevant_lines = extract_relevant_lines(contract, op_commands)
  192. ops = []
  193. local_vars = {}
  194. for line in relevant_lines:
  195. # This is a special case which creates a new local stack value
  196. if line.command() == "local":
  197. assert len(line.args()) == 1
  198. symbol = line.args()[0]
  199. local_vars[symbol] = len(local_vars)
  200. indexes = []
  201. else:
  202. if (indexes := symbols_list_to_refs(line, alloc,
  203. local_vars, constants)) is None:
  204. return None
  205. # Handle this here directly since only the
  206. # load command deals with constants
  207. if line.command() == "load":
  208. assert len(indexes) == 2
  209. # This is the only command which uses consts
  210. if indexes[1].type != VariableRefType.CONST:
  211. eprint("error: load command takes a const argument")
  212. eprint(line)
  213. return None
  214. elif any(index.type == VariableRefType.CONST for index in indexes):
  215. eprint("error: invalid const arg")
  216. eprint(line)
  217. return None
  218. ops.append(Operation(line, indexes))
  219. return ops
  220. class Constraint:
  221. def __init__(self, line, lcargs):
  222. self.command = line.command()
  223. self.args = lcargs
  224. self.line = line
  225. def args_comment(self):
  226. return ", ".join("%s" % symbol for symbol in self.line.args())
  227. def symbols_list_to_lcargs(line, alloc, constants):
  228. lcargs = []
  229. for symbol in line.args():
  230. if symbol in alloc:
  231. # Lookup variable index
  232. index = alloc[symbol].index
  233. lcargs.append(index)
  234. elif symbol in constants:
  235. value = constants[symbol]
  236. lcargs.append(value)
  237. else:
  238. eprint("error: missing unallocated symbol '%s'" % symbol)
  239. eprint(line)
  240. return None
  241. return lcargs
  242. def generate_constraints_table(contract, alloc, constants):
  243. relevant_lines = extract_relevant_lines(contract, constraint_commands)
  244. constraints = []
  245. for line in relevant_lines:
  246. if (lcargs := symbols_list_to_lcargs(line, alloc, constants)) is None:
  247. return None
  248. constraints.append(Constraint(line, lcargs))
  249. return constraints
  250. class Contract:
  251. def __init__(self, constants, alloc, ops, constraints):
  252. self.constants = constants
  253. self.alloc = alloc
  254. self.ops = ops
  255. self.constraints = constraints
  256. def __repr__(self):
  257. repr_str = ""
  258. repr_str += "Constants:\n"
  259. for symbol, value in self.constants.items():
  260. repr_str += " // %s\n" % symbol
  261. repr_str += " %s: %s\n" % value
  262. repr_str += "Alloc table:\n"
  263. for symbol, variable in self.alloc.items():
  264. repr_str += " // %s\n" % symbol
  265. repr_str += " %s %s\n" % (variable.type, variable.index)
  266. repr_str += "Operations:\n"
  267. for op in self.ops:
  268. repr_str += " // %s\n" % op.line
  269. repr_str += " %s %s\n" % (op.command, op.args)
  270. repr_str += "Constraints:\n"
  271. for constraint in self.constraints:
  272. if constraint.args:
  273. repr_str += " // %s\n" % constraint.args_comment()
  274. repr_str += " %s %s\n" % (constraint.command, constraint.args)
  275. return repr_str
  276. def compile(contract, constants):
  277. # Allocation table
  278. # symbol: Private/Public, is_param, index
  279. if (alloc := generate_alloc_table(contract)) is None:
  280. return None
  281. # Operations lines list
  282. if (ops := generate_ops_table(contract, alloc, constants)) is None:
  283. return None
  284. # Constraint commands
  285. if (constraints := generate_constraints_table(
  286. contract, alloc, constants)) is None:
  287. return None
  288. return Contract(constants, alloc, ops, constraints)
  289. def parse_constants(contents):
  290. relevant_lines = [line for line in contents if line.command() == "constant"]
  291. constants = {}
  292. for line in relevant_lines:
  293. assert line.command() == "constant"
  294. if len(line.args()) != 2:
  295. eprint("error: wrong number of args for constant")
  296. eprint(line)
  297. return None
  298. symbol, value = line.args()
  299. try:
  300. int(value, 16)
  301. except ValueError:
  302. eprint("error: invalid constant value for '%s'" % symbol)
  303. eprint(line)
  304. return None
  305. if len(value) != 32*2 + 2 or value[:2] != "0x":
  306. eprint("error: invalid hex value for constant")
  307. eprint(line)
  308. return None
  309. # Remove 0x prefix
  310. value = value[2:]
  311. constants[symbol] = (len(constants), value)
  312. return constants
  313. def process(contents):
  314. # Remove left whitespace
  315. contents = clean(contents)
  316. # Parse all constants
  317. if (constants := parse_constants(contents)) is None:
  318. return None
  319. # Divide into contract sections
  320. if (pre_contracts := divide_sections(contents)) is None:
  321. return None
  322. # Process each contract
  323. contracts = {}
  324. for contract_name, pre_contract in pre_contracts.items():
  325. if (contract := compile(pre_contract, constants)) is None:
  326. return None
  327. contracts[contract_name] = contract
  328. return contracts
  329. def main(argv):
  330. parser = argparse.ArgumentParser()
  331. parser.add_argument("filename", help="VM PISM file: proofs/vm.pism")
  332. group = parser.add_mutually_exclusive_group()
  333. group.add_argument('--display', action='store_true',
  334. help="show the compiled code in human readable format")
  335. group.add_argument('--rust', action='store_true',
  336. help="output compiled code to rust for testing")
  337. args = parser.parse_args()
  338. src_filename = args.filename
  339. contents = open(src_filename).read()
  340. if (contracts := process(contents)) is None:
  341. return -2
  342. def default_display():
  343. for contract_name, contract in contracts.items():
  344. print("Contract:", contract_name)
  345. print(contract)
  346. if args.display:
  347. default_display()
  348. elif args.rust:
  349. import vm_export_rust
  350. for contract_name, contract in contracts.items():
  351. vm_export_rust.display(contract)
  352. else:
  353. default_display()
  354. return 0
  355. if __name__ == "__main__":
  356. sys.exit(main(sys.argv))