vm.py 12 KB

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