vm.py 12 KB

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