🎫 Ticket_storage.v
Proofs
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
The function [get_balance] is valid.
Lemma get_balance_is_valid ctxt key_value :
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Ticket_storage.get_balance ctxt key_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Ticket_storage.get_balance ctxt key_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [set_balance] is valid.
Lemma set_balance_is_valid ctxt key_value balance :
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Ticket_storage.set_balance ctxt key_value balance in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Ticket_storage.set_balance ctxt key_value balance in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
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 balance ⇒ balance = delta
| None ⇒ False (* get must return a balance because it was adjusted !? *)
end.
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 balance ⇒ balance = delta
| None ⇒ False (* get must return a balance because it was adjusted !? *)
end.
The function [adjust_storage_space] is valid.
Lemma adjust_storage_space_is_valid ctxt storage_diff :
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Ticket_storage.adjust_storage_space ctxt storage_diff in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Ticket_storage.adjust_storage_space ctxt storage_diff in
Raw_context.Valid.t ctxt.
Proof.
Admitted.