Commit 3eaadae9 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Rename CursorList -> ChainedList

parent 5cd83c67
Pipeline #12242 failed with stage
in 22 seconds
......@@ -2,10 +2,10 @@
src/Automation.v
src/Blockchain.v
src/BoundedN.v
src/ChainedList.v
src/Circulation.v
src/Congress.v
src/Containers.v
src/CursorList.v
src/Extras.v
src/Finite.v
src/LocalBlockchain.v
......
......@@ -8,7 +8,7 @@ From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From SmartContracts Require Import CursorList.
From SmartContracts Require Import ChainedList.
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.
......@@ -767,7 +767,7 @@ Definition empty_state : ChainState :=
(* The ChainTrace captures that there is a valid execution where,
starting from one environment and queue of actions, we end up in a
different environment and queue of actions. *)
Definition ChainTrace := CursorList ChainState ChainEvent.
Definition ChainTrace := ChainedList ChainState ChainEvent.
Section Theories.
Ltac destruct_chain_event :=
......
(* This file implements, for lack of a better name, a cursor list.
This is a list for which each element contains a "cursor" type: each
element is parameterized over a 'from' and 'to' element of this type,
which must match with the previous element. For that reason this is
(* This file implements a chained list. This is a list for which
each element is a link between a from and to element of a provided
"link" type. That is, each link (element) has a "from" point that
must match the previous element's "to" point. For that reason this is
also a snoc list. Note that this is not unlike fhlist from CPDT,
except we place further restrictions on it. *)
From SmartContracts Require Import Automation.
Section CursorList.
Context {cursor_type : Type} {elm_type : cursor_type -> cursor_type -> Type}.
Section ChainedList.
Context {point : Type} {link : point -> point -> Type}.
Inductive CursorList : cursor_type -> cursor_type -> Type :=
| nil : forall {elm}, CursorList elm elm
| snoc : forall {from mid to}, CursorList from mid -> elm_type mid to -> CursorList from to.
Definition snoc_eq
{from mid mid' to}
(xs : CursorList from mid)
(x : elm_type mid' to) :
mid' = mid -> CursorList from to :=
fun eq =>
snoc xs (match eq with eq_refl => x end).
Inductive ChainedList : point -> point -> Type :=
| clnil : forall {elm}, ChainedList elm elm
| snoc : forall {from mid to},
ChainedList from mid -> link mid to -> ChainedList from to.
Fixpoint clist_app
{from mid to}
(xs : CursorList from mid)
(ys : CursorList mid to) : CursorList from to :=
(xs : ChainedList from mid)
(ys : ChainedList mid to) : ChainedList from to :=
match ys with
| nil => fun xs => xs
| clnil => fun xs => xs
| snoc ys' y => fun xs => snoc (clist_app xs ys') y
end xs.
......@@ -33,38 +26,38 @@ Infix "++" := clist_app (right associativity, at level 60).
Definition clist_prefix
{from mid to}
(prefix : CursorList from mid)
(full : CursorList from to) : Prop :=
(prefix : ChainedList from mid)
(full : ChainedList from to) : Prop :=
exists suffix, full = prefix ++ suffix.
Definition clist_suffix
{from mid to}
(suffix : CursorList mid to)
(full : CursorList from to) : Prop :=
(suffix : ChainedList mid to)
(full : ChainedList from to) : Prop :=
exists prefix, full = prefix ++ suffix.
Infix "`prefix_of`" := clist_prefix (at level 70).
Infix "`suffix_of`" := clist_suffix (at level 70).
Section Theories.
Lemma clist_app_nil_l {from to} (xs : CursorList from to) :
nil ++ xs = xs.
Lemma app_clnil_l {from to} (xs : ChainedList from to) :
clnil ++ xs = xs.
Proof. induction xs; auto; cbn; solve_by_rewrite. Qed.
Lemma clist_app_assoc
{c1 c2 c3 c4}
(xs : CursorList c1 c2)
(ys : CursorList c2 c3)
(zs : CursorList c3 c4) :
(xs : ChainedList c1 c2)
(ys : ChainedList c2 c3)
(zs : ChainedList c3 c4) :
xs ++ ys ++ zs = (xs ++ ys) ++ zs.
Proof. induction zs; intros; auto; cbn; solve_by_rewrite. Qed.
End Theories.
Lemma prefix_of_app
{from mid to to'}
{prefix : CursorList from mid}
{xs : CursorList from to}
{suffix : CursorList to to'} :
{prefix : ChainedList from mid}
{xs : ChainedList from to}
{suffix : ChainedList to to'} :
prefix `prefix_of` xs ->
prefix `prefix_of` xs ++ suffix.
Proof.
......@@ -72,13 +65,13 @@ Proof.
exists (ex_suffix ++ suffix).
rewrite clist_app_assoc; congruence.
Qed.
End CursorList.
End ChainedList.
Delimit Scope clist_scope with trace.
Bind Scope clist_scope with CursorList.
Bind Scope clist_scope with ChainedList.
Infix "++" := clist_app (right associativity, at level 60) : clist_scope.
Infix "`prefix_of`" := clist_prefix (at level 70) : clist_scope.
Infix "`suffix_of`" := clist_suffix (at level 70) : clist_scope.
Arguments CursorList : clear implicits.
Arguments ChainedList : clear implicits.
......@@ -3,7 +3,7 @@ chain implementing a chain type. More specifically, we show that the circulation
does not change during execution of blocks. This is proven under the (implicit)
assumption that the address space is finite. *)
From Coq Require Import List Permutation ZArith Psatz Morphisms.
From SmartContracts Require Import Automation Blockchain Extras Finite CursorList.
From SmartContracts Require Import Automation Blockchain Extras Finite ChainedList.
From RecordUpdate Require Import RecordSet.
Import ListNotations.
......
......@@ -9,7 +9,7 @@ From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
From SmartContracts Require Import Circulation.
From SmartContracts Require Import CursorList.
From SmartContracts Require Import ChainedList.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
From Coq Require Import Psatz.
......@@ -346,7 +346,7 @@ Section ExecuteActions.
destruct (execute_action_step _ _ _ _ exec_once) as [step].
destruct trace as [trace].
Hint Constructors ChainEvent : core.
Hint Constructors CursorList.
Hint Constructors ChainedList.
Hint Unfold ChainTrace.
destruct df; eapply IH; try eassumption; eauto.
(* BF case, where we need to permute *)
......@@ -379,7 +379,7 @@ Proof.
refine
{| lcb_lc := lc_initial; lcb_trace := _ |}.
constructor.
apply CursorList.nil.
exact clnil.
Defined.
Definition validate_header (new old : BlockHeader) : option unit :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment