CCTx_Preserve_Balance_Gateway_m3.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="__BjoK7oeEe69guM5sfZ6uQ" org.eventb.texttools.text_lastmodified="1706035273637" org.eventb.texttools.text_representation="machine CCTx_Preserve_Balance_Gateway_m3 refines CCTx_Fabric_Ethereum_m2  sees CCTx_Fabric_Ethereum_c2&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions accounts estimated_cross_chain_cost&#10;&#10;invariants&#10;  @inv31; estimated_cross_chain_cost ∈ ℕ&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;    then&#10;      @act31; estimated_cross_chain_cost ≔ 0&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC extends SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC&#10;  end&#10;&#10;  event INITIATE_CROSS_CHAIN_TRANSACTION_IN_FABRIC extends INITIATE_CROSS_CHAIN_TRANSACTION_IN_FABRIC&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION_IN_FABRIC extends PROCESS_CROSS_CHAIN_TRANSACTION_IN_FABRIC&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT_IN_FABRIC extends LISTEN_SMART_CONTRACT_EVENT_IN_FABRIC&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION_TO_ETHEREUM extends SUBMIT_CROSS_CHAIN_TRANSACTION_TO_ETHEREUM&#10;    where&#10;      @grd31; fee ≤ estimated_cross_chain_cost // Check that the estimated fee is greater or equal to the validators fee (RQ2)&#10;  end&#10;&#10;  event CREATE_ADDRESS_IN_ETHEREUM extends CREATE_ADDRESS_IN_ETHEREUM&#10;  end&#10;&#10;  event DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM extends DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM&#10;    where&#10;      @grd31; address ≠ gateway_address // The gateway cannot deposit in its own account (RQ3)&#10;  end&#10;&#10;  event SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM extends SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM&#10;    then&#10;      @act31; estimated_cross_chain_cost ≔ transfer_amount&#10;  end&#10;end&#10;" version="5">
    <org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Fabric_Ethereum_m2"/>
    <org.eventb.core.seesContext name="_wnFu0KsZEe6I4bA9GxwhqQ" org.eventb.core.target="CCTx_Fabric_Ethereum_c2"/>
    <org.eventb.core.event name="_wnFu0KsZEe6I4bA9GxwhqR" 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="__BjBGboeEe69guM5sfZ6uQ">
        <org.eventb.core.action name="_ohzhsLX5Ee6ab_EHIz4SJQ" org.eventb.core.assignment="estimated_cross_chain_cost ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act31;" org.eventb.emf.persistence.emf_id="__BjBGLoeEe69guM5sfZ6uQ"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_GToO5rX-Ee6rT6SCwCdkxA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC" org.eventb.emf.persistence.emf_id="__BjBG7oeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_OouRkLX-Ee6rT6SCwCdkxA" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_aIltcLk7Ee6otoREOj7KsQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CROSS_CHAIN_TRANSACTION_IN_FABRIC" org.eventb.emf.persistence.emf_id="__BjBHboeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_aIltcbk7Ee6otoREOj7KsQ" org.eventb.core.target="INITIATE_CROSS_CHAIN_TRANSACTION_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_wnFu0KsZEe6I4bA9GxwhqU" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION_IN_FABRIC" org.eventb.emf.persistence.emf_id="__BjBH7oeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="PROCESS_CROSS_CHAIN_TRANSACTION_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_GTo18LX-Ee6rT6SCwCdkxA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="__BjBIboeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_RDwwoLX-Ee6rT6SCwCdkxA" org.eventb.core.target="LISTEN_SMART_CONTRACT_EVENT_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_GTo18rX-Ee6rT6SCwCdkxA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION_TO_ETHEREUM" org.eventb.emf.persistence.emf_id="__BjoIboeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_N4fHcLX-Ee6rT6SCwCdkxA" org.eventb.core.target="SUBMIT_CROSS_CHAIN_TRANSACTION_TO_ETHEREUM"/>
        <org.eventb.core.guard name="_Uq128LX8Ee6rT6SCwCdkxA" org.eventb.core.comment="Check that the estimated fee is greater or equal to the validators fee (RQ2)" org.eventb.core.generated="false" org.eventb.core.label="grd31;" org.eventb.core.predicate="fee ≤ estimated_cross_chain_cost" org.eventb.emf.persistence.emf_id="__BjoILoeEe69guM5sfZ6uQ"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_GTpdALX-Ee6rT6SCwCdkxA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CREATE_ADDRESS_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="__BjoI7oeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_LO7rQLX-Ee6rT6SCwCdkxA" org.eventb.core.target="CREATE_ADDRESS_IN_ETHEREUM"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_eDb48LloEe6mA4ET_9OgqQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="__BjoJroeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_eDb48bloEe6mA4ET_9OgqQ" org.eventb.core.target="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM"/>
        <org.eventb.core.guard name="_ra8KoLX8Ee6rT6SCwCdkxA" org.eventb.core.comment="The gateway cannot deposit in its own account (RQ3)" org.eventb.core.generated="false" org.eventb.core.label="grd31;" org.eventb.core.predicate="address ≠ gateway_address" org.eventb.emf.persistence.emf_id="__BjoJboeEe69guM5sfZ6uQ"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_GTpdBLX-Ee6rT6SCwCdkxA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="__BjoKboeEe69guM5sfZ6uQ">
        <org.eventb.core.refinesEvent name="_MIB2cLX-Ee6rT6SCwCdkxA" org.eventb.core.target="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM"/>
        <org.eventb.core.action name="_uqjBkLX5Ee6ab_EHIz4SJQ" org.eventb.core.assignment="estimated_cross_chain_cost ≔ transfer_amount" org.eventb.core.generated="false" org.eventb.core.label="act31;" org.eventb.emf.persistence.emf_id="__BjoKLoeEe69guM5sfZ6uQ"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="_jJxtELX5Ee6ab_EHIz4SJQ" org.eventb.core.generated="false" org.eventb.core.label="inv31;" org.eventb.core.predicate="estimated_cross_chain_cost ∈ ℕ" org.eventb.emf.persistence.emf_id="__BjBF7oeEe69guM5sfZ6uQ"/>
    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="__BjBELoeEe69guM5sfZ6uQ"/>
    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="__BjBEboeEe69guM5sfZ6uQ"/>
    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="__BjBEroeEe69guM5sfZ6uQ"/>
    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="__BjBE7oeEe69guM5sfZ6uQ"/>
    <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="__BjBFLoeEe69guM5sfZ6uQ"/>
    <org.eventb.core.variable name="_15j2ALlnEe6mA4ET_9OgqQ" org.eventb.core.generated="false" org.eventb.core.identifier="accounts" org.eventb.emf.persistence.emf_id="__BjBFboeEe69guM5sfZ6uQ"/>
    <org.eventb.core.variable name="_g0powLX5Ee6ab_EHIz4SJQ" org.eventb.core.generated="false" org.eventb.core.identifier="estimated_cross_chain_cost" org.eventb.emf.persistence.emf_id="__BjBFroeEe69guM5sfZ6uQ"/>
</org.eventb.core.machineFile>