Ethereum -> Fabric behaviour

33488f86 · Guzmán Llambías · 9e8d9221 · 33488f86 · 33488f86 · 33488f86
Commit 33488f86 authored 1 year ago by Guzmán Llambías
--- a/BIG/Ethereum_Fabric_c2.bcc
+++ b/BIG/Ethereum_Fabric_c2.bcc
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase">
+    <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/BIG/BIG_c1.bcc|org.eventb.core.scContextFile#BIG_c1" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.extendsContext#'"/>
+    <org.eventb.core.scInternalContext name="BIG_c1">
+        <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_NmUHEKmBEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_B7Fx4KmIEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.scConstant name="gateway" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_t3pvIKo_Ee6I4bA9GxwhqQ" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_lsmHUKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_bUpUwKmAEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_kx61gapGEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_OLUJEKsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_ISeO4KmBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+    </org.eventb.core.scInternalContext>
+    <org.eventb.core.scAxiom name="BIG_c2" org.eventb.core.label="axm11;" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.axiom#_e542gK75Ee6N-vMrFZcPfQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scAxiom name="BIG_c3" org.eventb.core.label="axm12;" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.axiom#_-6gTUK75Ee6N-vMrFZcPfQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scConstant name="write" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.constant#_cent8a75Ee6N-vMrFZcPfQ" org.eventb.core.type="PERMISSIONS"/>
+    <org.eventb.core.scCarrierSet name="USERS" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.carrierSet#_51xqoK74Ee6N-vMrFZcPfQ" org.eventb.core.type="ℙ(USERS)"/>
+    <org.eventb.core.scConstant name="read" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.constant#_cent8K75Ee6N-vMrFZcPfQ" org.eventb.core.type="PERMISSIONS"/>
+    <org.eventb.core.scCarrierSet name="PERMISSIONS" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.carrierSet#_rDT64K8DEe6CsKD2nJu6WQ" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+    <org.eventb.core.scConstant name="gateway_user" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.constant#_ceoVAK75Ee6N-vMrFZcPfQ" org.eventb.core.type="USERS"/>
+</org.eventb.core.scContextFile>
--- a/BIG/Ethereum_Fabric_c2.bpo
+++ b/BIG/Ethereum_Fabric_c2.bpo
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="3">
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="3">
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.poIdentifier name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poIdentifier name="USERS" org.eventb.core.type="ℙ(USERS)"/>
+        <org.eventb.core.poIdentifier name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+        <org.eventb.core.poIdentifier name="write" org.eventb.core.type="PERMISSIONS"/>
+        <org.eventb.core.poIdentifier name="read" org.eventb.core.type="PERMISSIONS"/>
+        <org.eventb.core.poIdentifier name="gateway_user" org.eventb.core.type="USERS"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Ethereum_Fabric_c2.bpo|org.eventb.core.poFile#Ethereum_Fabric_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="3">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.axiom#_e542gK75Ee6N-vMrFZcPfQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/BIG/Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#Ethereum_Fabric_c2|org.eventb.core.axiom#_-6gTUK75Ee6N-vMrFZcPfQ"/>
+    </org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>
--- a/BIG/Ethereum_Fabric_c2.bpr
+++ b/BIG/Ethereum_Fabric_c2.bpr
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file
--- a/BIG/Ethereum_Fabric_c2.bps
+++ b/BIG/Ethereum_Fabric_c2.bps
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.psFile/>
\ No newline at end of file
--- a/BIG/Ethereum_Fabric_c2.buc
+++ b/BIG/Ethereum_Fabric_c2.buc
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_QZ84Z7RuEe6XM4m7AoCU9A" org.eventb.texttools.text_lastmodified="1705409613544" org.eventb.texttools.text_representation="context Ethereum_Fabric_c2 extends BIG_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10;  @axm11: partition(PERMISSIONS, {read}, {write}) // Two only type of permissions exist: read and write&#10;  @axm12: gateway_user ∈ USERS // The gateway has an Hyperledger Fabric user&#10;end&#10;" version="3">
+    <org.eventb.core.extendsContext name="'" org.eventb.core.target="BIG_c1"/>
+    <org.eventb.core.axiom name="_e542gK75Ee6N-vMrFZcPfQ" org.eventb.core.comment="Two only type of permissions exist: read and write" org.eventb.core.generated="false" org.eventb.core.label="axm11;" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_QZ84ZbRuEe6XM4m7AoCU9A"/>
+    <org.eventb.core.axiom name="_-6gTUK75Ee6N-vMrFZcPfQ" org.eventb.core.comment="The gateway has an Hyperledger Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12;" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_QZ84ZrRuEe6XM4m7AoCU9A"/>
+    <org.eventb.core.constant name="_cent8K75Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_QZ84YrRuEe6XM4m7AoCU9A"/>
+    <org.eventb.core.constant name="_cent8a75Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_QZ84Y7RuEe6XM4m7AoCU9A"/>
+    <org.eventb.core.constant name="_ceoVAK75Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_QZ84ZLRuEe6XM4m7AoCU9A"/>
+    <org.eventb.core.carrierSet name="_rDT64K8DEe6CsKD2nJu6WQ" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_QZ84YLRuEe6XM4m7AoCU9A"/>
+    <org.eventb.core.carrierSet name="_51xqoK74Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_QZ84YbRuEe6XM4m7AoCU9A"/>
+</org.eventb.core.contextFile>
--- a/BIG/Ethereum_Fabric_m2.bcm
+++ b/BIG/Ethereum_Fabric_m2.bcm
--- a/BIG/Ethereum_Fabric_m2.bpo
+++ b/BIG/Ethereum_Fabric_m2.bpo
--- a/BIG/Ethereum_Fabric_m2.bps
+++ b/BIG/Ethereum_Fabric_m2.bps
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.psFile>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="44" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="44" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv14;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="44" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv16;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="45" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="45" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="45" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv16;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="45" org.eventb.core.psManual="false"/>
+</org.eventb.core.psFile>
--- a/BIG/Ethereum_Fabric_m2.bum
+++ b/BIG/Ethereum_Fabric_m2.bum
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_FB8EHrO6Ee671Y_A8Y-IGw" org.eventb.texttools.text_lastmodified="1705332227795" org.eventb.texttools.text_representation="machine Ethereum_Fabric_m2 refines BIG_m1  sees Ethereum_Fabric_c2&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions&#10;received_cross_chain_transactions authenticated_users auditted_transactions write_grant&#10;&#10;invariants&#10;  @inv11; authenticated_users ⊆ USERS&#10;  @inv12; auditted_transactions ∈ received_cross_chain_transactions → authenticated_users&#10;  @inv13; ∀ tx · tx ∈ received_cross_chain_transactions ⇒ (∃ u · u ∈&#10;                  authenticated_users ∧ tx ↦ u ∈ auditted_transactions) // RQ1&#10;  @inv14; write_grant ∈ authenticated_users ↔ {write}&#10;  @inv16; auditted_transactions[received_cross_chain_transactions] ⊆ dom(write_grant) // RQ2&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;    then&#10;      @act11; authenticated_users ≔ {gateway_user} // ENV2&#10;      @act12; auditted_transactions ≔ ∅&#10;      @act13; write_grant ≔ {gateway_user ↦ write} // ENV3&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION extends SUBMIT_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION extends PROCESS_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT extends LISTEN_SMART_CONTRACT_EVENT&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION extends GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;    any&#10;    &#9;user&#10;    where&#10;      @grd11; user ∈ authenticated_users // RQ4&#10;      @grd12; user ↦ write ∈ write_grant // RQ3&#10;    then&#10;      @act11; auditted_transactions(target_smart_contract ↦ cross_chain_transaction) ≔ user //RQ1&#10;  end&#10;end&#10;" version="5">
+    <org.eventb.core.refinesMachine name="'" org.eventb.core.target="BIG_m1"/>
+    <org.eventb.core.seesContext name="_MuSzUK76Ee6N-vMrFZcPfQ" org.eventb.core.target="Ethereum_Fabric_c2"/>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqR" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_FB7dELO6Ee671Y_A8Y-IGw">
+        <org.eventb.core.action name="_ZLkMUK76Ee6N-vMrFZcPfQ" org.eventb.core.assignment="authenticated_users ≔ {gateway_user}" org.eventb.core.comment="ENV2" org.eventb.core.generated="false" org.eventb.core.label="act11;" org.eventb.emf.persistence.emf_id="_FB7dDbO6Ee671Y_A8Y-IGw"/>
+        <org.eventb.core.action name="_51HmgK78Ee6N-vMrFZcPfQ" org.eventb.core.assignment="auditted_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12;" org.eventb.emf.persistence.emf_id="_FB7dDrO6Ee671Y_A8Y-IGw"/>
+        <org.eventb.core.action name="_3tsi0K8DEe6CsKD2nJu6WQ" org.eventb.core.assignment="write_grant ≔ {gateway_user ↦ write}" org.eventb.core.comment="ENV3" org.eventb.core.generated="false" org.eventb.core.label="act13;" org.eventb.emf.persistence.emf_id="_FB7dD7O6Ee671Y_A8Y-IGw"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqS" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_FB8EELO6Ee671Y_A8Y-IGw">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqT" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_FB8EErO6Ee671Y_A8Y-IGw">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CROSS_CHAIN_TRANSACTION"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqU" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_FB8EFLO6Ee671Y_A8Y-IGw">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="PROCESS_CROSS_CHAIN_TRANSACTION"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqV" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_FB8EFrO6Ee671Y_A8Y-IGw">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_SMART_CONTRACT_EVENT"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqW" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_FB8EHLO6Ee671Y_A8Y-IGw">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION"/>
+        <org.eventb.core.action name="_OatxgK79Ee6N-vMrFZcPfQ" org.eventb.core.assignment="auditted_transactions(target_smart_contract ↦ cross_chain_transaction) ≔ user" org.eventb.core.comment="RQ1" org.eventb.core.generated="false" org.eventb.core.label="act11;" org.eventb.emf.persistence.emf_id="_FB8EG7O6Ee671Y_A8Y-IGw"/>
+        <org.eventb.core.guard name="_G79oUK76Ee6N-vMrFZcPfQ" org.eventb.core.comment="RQ4" org.eventb.core.generated="false" org.eventb.core.label="grd11;" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_FB8EGbO6Ee671Y_A8Y-IGw"/>
+        <org.eventb.core.guard name="_9p1UoK8EEe6CsKD2nJu6WQ" org.eventb.core.comment="RQ3" org.eventb.core.generated="false" org.eventb.core.label="grd12;" org.eventb.core.predicate="user ↦ write ∈ write_grant" org.eventb.emf.persistence.emf_id="_FB8EGrO6Ee671Y_A8Y-IGw"/>
+        <org.eventb.core.parameter name="_kwOZ8K8IEe6CsKD2nJu6WQ" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_FB8EGLO6Ee671Y_A8Y-IGw"/>
+    </org.eventb.core.event>
+    <org.eventb.core.invariant name="_Vz5s8K76Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.label="inv11;" org.eventb.core.predicate="authenticated_users ⊆ USERS" org.eventb.emf.persistence.emf_id="_FB7dCLO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.invariant name="_MgekUK77Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.label="inv12;" org.eventb.core.predicate="auditted_transactions ∈ received_cross_chain_transactions → authenticated_users" org.eventb.emf.persistence.emf_id="_FB7dCbO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.invariant name="_6-1AkK78Ee6N-vMrFZcPfQ" org.eventb.core.comment="RQ1" org.eventb.core.generated="false" org.eventb.core.label="inv13;" org.eventb.core.predicate="∀ tx · tx ∈ received_cross_chain_transactions ⇒ (∃ u · u ∈&#10;                  authenticated_users ∧ tx ↦ u ∈ auditted_transactions)" org.eventb.emf.persistence.emf_id="_FB7dCrO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.invariant name="_scPcsK8DEe6CsKD2nJu6WQ" org.eventb.core.generated="false" org.eventb.core.label="inv14;" org.eventb.core.predicate="write_grant ∈ authenticated_users ↔ {write}" org.eventb.emf.persistence.emf_id="_FB7dC7O6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.invariant name="_2EqLoK8HEe6CsKD2nJu6WQ" org.eventb.core.comment="RQ2" org.eventb.core.generated="false" org.eventb.core.label="inv16;" org.eventb.core.predicate="auditted_transactions[received_cross_chain_transactions] ⊆ dom(write_grant)" org.eventb.emf.persistence.emf_id="_FB7dDLO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_FB7dALO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_FB7dAbO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_FB7dArO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_FB7dA7O6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_FB7dBLO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_Vz67EK76Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_FB7dBbO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_MgfLYK77Ee6N-vMrFZcPfQ" org.eventb.core.generated="false" org.eventb.core.identifier="auditted_transactions" org.eventb.emf.persistence.emf_id="_FB7dBrO6Ee671Y_A8Y-IGw"/>
+    <org.eventb.core.variable name="_FuVEoK8HEe6CsKD2nJu6WQ" org.eventb.core.generated="false" org.eventb.core.identifier="write_grant" org.eventb.emf.persistence.emf_id="_FB7dB7O6Ee671Y_A8Y-IGw"/>
+</org.eventb.core.machineFile>