Fix go_left specification
The specification of go_left
is incorrect:
Definition go_left (pos height : nat) := pos < 2 ^ height.-1.
This makes the insert_overflow implementation fail the incremental tests. The right definition should be:
(* The ocaml spec alternative for go_left requires non-structural reduction:
let rec go_left_spec pos height =
assert (Compare.Int64.(pos >=0L));
if Compare.Int64.(pos = 0L) then true
else let full = pow2 height
in if Compare.Int64.(pos < full) then pos < pow2 (height - 1)
else go_left_spec (Int64.sub pos full) height
*)
Translated to Coq:
(* We add gas, as we can always have an upper bound on the
position. Notice also that in the case of an overflowing position
argument [pos], it will converge to 0 quicker than [gas].*)
Fixpoint go_left_spec' (pos height gas: nat) :=
if gas isn't S g then true
else if pos < 2 ^ height then pos < 2 ^ height.-1
else go_left_spec' (pos - 2 ^ height) height g.
Definition go_left_spec pos height := go_left_spec' pos height pos.+1.
TODO
-
Test the new spec in OCaml (in tezos/tezos/germanD@sapling-tests) -
Test incrementality with the new Coq spec -
Prove insert_overflow_spec
Edited by Germán Delbianco