Behavioral up/down casting for statically typed languages (Coq artifact)
Creators: name: Bacchiani, Lorenzo
name: Bravetti, Mario
name: Giunti, Marco
name: Mota, João
name: Ravara, António
Publisher: name: Zenodo
Year: 2023

description: Artifact Submission


Title of the submitted paper: Behavioral up/down casting for statically typed languages



What does the artifact comprise?


The Docker image contains:



Coq source code (in the /proofs folder);

HTML documentation (in the /proofs/docs folder).


Following is a mapping from definitions in the paper to the corresponding Coq ones:




Definition
Paper
Coq file
Name of formalization
Notation




States
Definition 1
Protocols.v
state
 


Typestate name definitions
Definition 2
Protocols.v
unfold
 


State simulation
Definition 3
Subtyping.v
state_sim
 


Subtyping on states
Definition 4
Subtyping.v
state_sub
a <s b


Algorithmic state subtyping
Definition 7
Subtyping.v
state_sub_alg
 


Types
Definition 10
Types.v
ttype
 


Subtyping on types
Definition 11
Subtyping.v
type_sub
a <: b


Super relation on classes
Definition 14
Classes.v
super
 


Subtyping relation on classes
Definition 15
Classes.v
class_sub
a <c b


Protocol input states
Definition 17
Classes.v
prot_input_states
 


Upcast on types
Definition 19
Casting.v
upcast
 


Downcast on types
Definition 24
Casting.v
downcast
 


Evolve on types
Definition 31
Evolve.v
evolve
 


Typestate Trees
Definition 36
TypestateTrees.v
TT
 


Well-formedness Of Typestate Trees
Definition 38
TypestateTrees.v
well_formed_tt
|- tt


Upcast on typestate trees
Definition 39
TypestateTrees.v
upcast_tt
 


Closest subtree
Definition 41
TypestateTrees.v
closest
 


Downcast on typestate trees
Definition 43
TypestateTrees.v
downcast_tt
 


Evolve on typestate trees
Definition 45
TypestateTrees.v
evolve_tt
 


Typestate Tree Height
Definition 47
TypestateTrees.v
height
 


Classes in typestate tree set
Definition 48
TypestateTrees.v
classes
 


Find in typestate tree set
Definition 49
TypestateTrees.v
find
 


Merge on typestate trees
Definition 50
TypestateTrees.v
merge_tt
 


Sequence of upcasts on types
Definition 52
Casting.v
upcast_many
 


Soundness Of Typestate Trees
Definition 53
Soundness.v
sound_tt
 




Regarding some definitions in the paper that differ from the Coq formalization:




Definition
Paper
Explanation




Reachable states
Definition 16
Excluding unreachable states is an optimization, and since our results do not depend on it, we do not formalize it in Coq.


Typestates in type
Definition 18
The purpose of this function is to contrain the typestates occuring in a type. In the paper, it is always used in the form typestates(t) ⊆ ProtInputStates(c). Because of that, in Coq, we define the relation all_typestates_in t c (defined in the Classes.v file with the notation t \in c) which states that all typestates in t belong to the protocol of class c.


No duplicate classes
Definition 37
Defined directly with List.NoDup (classes tts), so no auxiliary definition is required.




Following is a mapping from the main theorems and lemmas in the paper to the corresponding Coq ones:




Theorem/Lemma
Paper
Coq file
Name of formalization




Reflexivity (of states subtyping)
Lemma 5
Subtyping.v
state_sub_reflex


Transitivity (of states subtyping)
Lemma 6
Subtyping.v
state_sub_trans


Algorithm soundness and completeness
Theorems 8 and 9
Subtyping.v
state_sub_alg_sound_complete


Reflexivity (of types subtyping)
Lemma 12
Subtyping.v
type_sub_reflex


Transitivity (of types subtyping)
Lemma 13
Subtyping.v
type_sub_trans


Upcast preserves protocol membership
Lemma 20
Casting.v
upcast_preserves_prot


Upcast Consistency
Theorem 21
Casting.v
upcast_consistency


Upcast Least Upper Bound
Theorem 22
Casting.v
upcast_least_upper_bound


Upcast Preserves Subtyping
Theorem 23
Casting.v
upcast_preserves_subtyping


Downcast preserves protocol membership
Lemma 25
Casting.v
downcast_preserves_prot


Downcast Consistency
Theorem 26
Casting.v
downcast_consistency


Downcast Greatest Lower Bound
Theorem 27
Casting.v
downcast_greatest_lower_bound


Downcast Preserves Subtyping
Theorem 28
Casting.v
downcast_preserves_subtyping


Downcast reverses upcast
Corollary 29
Casting.v
downcast_reverses_upcast


Upcast reverses downcast
Corollary 30
Casting.v
upcast_reverses_downcast


Evolve preserves protocol membership
Lemma 32
Evolve.v
evolve_preserves_prot


Evolve Preserves Subtyping
Theorem 33
Evolve.v
evolve_preserves_subtyping


Evolve and upcast
Theorem 34
Evolve.v
evolve_upcast


Evolve and downcast
Theorem 35
Evolve.v
evolve_downcast


Typestate Trees Well-formedness Preserved By Upcast
Theorem 40
TypestateTrees.v
wf_preserved_by_upcast


Closest correctness
Lemma 42
TypestateTrees.v
closest_correct


Typestate Trees Well-formedness Preserved By Downcast
Theorem 44
TypestateTrees.v
wf_preserved_by_downcast


Typestate Trees Well-formedness Preserved By Evolve
Theorem 46
TypestateTrees.v
wf_preserved_by_evolve


Typestate Trees Well-formedness Preserved By Merge
Theorem 51
TypestateTrees.v
wf_preserved_by_merge


Typestate Trees Soundness Preservation
Theorem 54
Soundness.v
soundness_preserved_by_upcast, soundness_preserved_by_downcast, soundness_preserved_by_evolve, soundness_preserved_by_merge






Software requirements




Docker

GNU Bash




Getting Started




Open Docker Desktop with your GUI: this will launch the daemon.

Open a shell.




Shell instructions




Import the image provided into docker:




docker load -i behavioral-casting-coq.tar




Run the docker image:




docker run -it behavioral-casting-coq:latest




A prompt of the form coq@f09e365aabf8:/proofs$ should be opened. Now run:




make




Output


A successful compilation (make) indicates all the results hold.