Skip to main content

🎫 Ticket_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

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

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [get_balance] is valid.
The function [set_balance] is valid.
The function [adjust_balance] is valid.
Lemma adjust_balance_is_valid ctxt key_value delta :
  Raw_context.Valid.t ctxt
  letP? '(_, ctxt) := Ticket_storage.adjust_balance ctxt key_value delta in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

(* @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 balancebalance = delta
  | NoneFalse (* get must return a balance because it was adjusted !? *)
  end.

The function [adjust_storage_space] is valid.