Appendix C - Constructs you may see in proof output

The math used by the prover is different from C maths, so you may see some expressions that are neither part of standard C nor part of the eCv specification extensions. Here is a list of [some of] them. You should not see these in error messages, or anywhere else other than in proof/unproven output files - let us know if you do.

Binary operators ./ and .%

These are round-towards-zero versions of the / and % integer operators. Plain / and % in proofs refer to the version of integer division that always rounds down and the version of modulo that yields a result having the same sign as the divisor.

Unary operator #

This means the number of elements in the collection operand. For an array arr, #arr equates to arr.count.

Subscripted variables

A variable of the form foo_543,21 means the value of variable foo at line 543 column 21 in the .i file that was generated by the preprocessor. Similarly, heap_543,21 means the value of the heap at that location.

"$r.value" expressions

The expression p.$r.value where p is a simple pointer is the prover's internal representation of *p. The expression ap.$r.value where ap is an array pointer is the prover's internal representation of ap.all, i.e. all the elements in the array to which ap points.

TOC