🎫 Ticket_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Ticket_storage.

(* @TODO *)
Axiom adjust_balance_get_eq : ∀ {ctxt} {key} {delta},
  letP? '(_, ctxt) := Ticket_storage.adjust_balance ctxt key delta in
  letP? '(balance, _) := Ticket_storage.get_balance ctxt key in
  match balance with
  | Some balance ⇒ balance = delta
  | None ⇒ False (* get must return a balance because it was adjusted !? *)
  end.