binary-search example setup-verifier fails

[jimouris]

Hello,

bellow is the trace of command ./pepper_compile_and_setup_V.sh binary_search binary_search.vkey binary_search.pkey :

❯❯ pepper (master) ./pepper_compile_and_setup_V.sh binary_search binary_search.vkey binary_search.pkey

+ compiling common objs

============================================
=== Compiling computation to constraints ===
============================================

+ compile apps/binary_search.c --metrics -b 0 -w 10240 -t ZAATAR -db-hash-func ggh -db-num-addresses 1024 -ram-cell-num-bits 32 -db-hash-num-bits 1216 -db-thr-num-addresses-naive 32768 -fast-ram-address-width 32 -fast-ram-word-width 64
metric_num_lines_in_sfdl binary_search 56
metric_num_lines_in_source binary_search 56
make[1]: Entering directory '/home/jimouris/repos/pequin/compiler/frontend'
ant compile
Buildfile: /home/jimouris/repos/pequin/compiler/frontend/build.xml

compile:

BUILD SUCCESSFUL
Total time: 0 seconds
make[1]: Leaving directory '/home/jimouris/repos/pequin/compiler/frontend'
WARNING: --cstdarithtruncate is disabled, so type errors will warn and arithmetic is not ANSI C compliant
Compiling binary_search.c
Expanding circuit to file binary_search.c.ZAATAR.circuit
Type Error set to WARNING mode: Type error, could not perform assignment 609=&25
, cannot assign pointer-to-uint bits 1 to #compute$$$$#ramget$ptrToTarget which is a pointer-to-uint bits 32.
Writing constant values to binary_search.c.ZAATAR.spec.cons
metric_compile_1_utime binary_search 0.47
metric_compile_1_stime binary_search 0.02

metric_compile_1_wires binary_search 343
metric_compile_tac2_utime binary_search 0.00
metric_compile_tac2_stime binary_search 0.00

WARNING: --cstdarithtruncate is disabled, so type errors will warn and arithmetic is not ANSI C compliant
metric_compile_p2_utime binary_search 0.16
metric_compile_p2_stime binary_search 0.00

metric_compile_untac2_utime binary_search 0.00
metric_compile_untac2_stime binary_search 0.00

WARNING: --cstdarithtruncate is disabled, so type errors will warn and arithmetic is not ANSI C compliant
Optimizing previously compiled circuit binary_search.c.ZAATAR.circuit2
Using variable dependencies from profile binary_search.c.ZAATAR.circuit2.profile
(Complete.)
Expanding circuit to file binary_search.c.ZAATAR.circuit
Writing constraints to binary_search.c.ZAATAR.spec_tmp
metric_num_occurrences_exo_compute 0
metric_num_occurrences_ext_gadget 0
metric_num_occurrences_hashget 0
metric_num_occurrences_hashput 0
metric_num_occurrences_ramget 5
metric_num_occurrences_ramget_fast 0
metric_num_occurrences_ramput 16
metric_num_occurrences_ramput_fast 0
Cleaning up constraints, result will appear in binary_search.c.ZAATAR.spec
metric_compile_2_utime binary_search 0.79
metric_compile_2_stime binary_search 0.01

metric_compile_2_wires binary_search 129
Expanding database operations in ../binary_search.c.ZAATAR.spec
Creating prover worksheet, result will appear at bin/binary_search.pws
Writing QAP matrices to ../../pepper/bin/binary_search.qap
Traceback (most recent call last):
  File "zcc_backend.py", line 331, in <module>
    main()
  File "zcc_backend.py", line 328, in main
    gen.generate_code_from_template(opt.spec)
  File "zcc_backend.py", line 209, in generate_code_from_template
    self.generate_matrices(spec_file, defs)
  File "zcc_backend.py", line 130, in generate_matrices
    (defs['NzA'], defs['NzB'], defs['NzC'], defs['num_constraints']) = zcc_parser.generate_zaatar_matrices(spec_file, shuffledIndices, qap_file_name)
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 1765, in generate_zaatar_matrices
    process_spec_section(spec_file, START_TAG + CONSTRAINTS_TAG, END_TAG + CONSTRAINTS_TAG, f)
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 81, in process_spec_section
    func(line)
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 1723, in f
    for bc in basic_constraints:
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 1251, in to_basic_constraints
    yield expand_basic_constraint(bc)
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 1266, in expand_basic_constraint
    expansion += expand_polynomial_str(tokens)
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 1280, in expand_polynomial_str
    expanded = expand_polynomial(tokens)
  File "/home/jimouris/repos/pequin/compiler/backend/zcc_parser.py", line 1294, in expand_polynomial
    raise Exception("expand_polynomial: Format error: " + str(tokens))
Exception: expand_polynomial: Format error: deque(['EXTERN', 'state_op_put_bits_1024_ggh_32', '0'])
make: *** [Makefile:124: bin/binary_search.params] Error 1

==========================================
===== Running setup (key generation) =====
==========================================

./pepper_compile_and_setup_V.sh: line 35: bin/pepper_verifier_binary_search: No such file or directory

Other files (such as mm_pure_arith or base_2_log) run smoothly.

Thanks in advance,
Dimitris

[maxhowald]

Hmm, thanks for reporting this. It looks like this is caused by the ramput() function calls in this example, which are compiled to constraints using a Merkle tree-based approach.

I'll try to look in to this more closely soon, but for now, you may want to check out this example, which is re-written to use a permutation network to compile computations that use RAM more efficiently.

Note that using this approach, there is no need to explicitly call a function like ramput(). The compiler automatically handles ordinary statements which require a concept of RAM, such as an array access where the array index depends on the input to the computation. Section 3 of this paper has more information on how such constructs are compiled to constraints.

[jimouris]

Thanks for the response. I was wondering why those ramput/ramget commands were necessary, but it seems clear now. binary_search_fast.c does the work for me, feel free to close the issue.

[zhluo94]

A follow-up question: are these ramput_fast commands expected?

I could understand ramget_fast's, as binary search incurs logSIZE number of random reads. However, after playing with parameters, it seems that binary_search_fast.c incurs the same number of ramput_fast's as the length of the input array (SIZE, by default). Could we get rid of these ramput_fast's? Asking because binary search has this nice logarithmic cost, the benefit of which will be gone if a linear number of ramput_fast's are needed...