On this pageExamQuestion 1What is returned by the execution of a smart contract ?The current storage state when invoking the smart contractThe modified storage state after invoking the smart contractThe entrypoint that has been called (and its related parameters)The list of emitted operations produced by the execution of the smart contractThe balance of the contractThe size of the storageThe code of the smart contractThe list of users allowed to call the smart contractQuestion 2What makes the bridge between the Tezos world and the formal world of Coq ?The Michelson languageThe Coq universe (predefined Coq types)The Mi-cho-coq libraryThe Tezos protocolQuestion 3Who is Thierry Coquand ?The founder of the type theory called λ-calculusThe founder of the type theory called the calculus of constructions (CoC).The principal developer of the _Coq_ proof assistant.The founder of the intuitionistic type theory.Question 4We have seen that a Michelson script must be translated into an annotated script (i.e. a formal definition) (because Mi-Cho-Coq provides an equivalent for each Michelson instruction). In the theorem we want to prove, we specify that "the execution of the annotated script is equivalent to post-conditions". Who is responsible for the execution of this annotated script ?The Michelson interpreterThe Mi-Cho-Coq evaluatorThe Coq inference engineQuestion 5What post-conditions depends on (What post-conditions are built upon) ?The storage modification produced by the execution of the smart contractThe entrypoint parameter which is invokedThe sequence of Michelson instructions (smart contract code)Operations produced by the execution of the smart contractEnvironment variables (transaction properties such as sender, amount)Predefined Coq types and inductive types (Coq libraries)Mi-Cho-Coq library