Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Preserve_Balance_Gateway_m3.bum 8.67 KiB
Newer Older
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
1 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
2 
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_BvYlnr7vEe6laZimEYihUg" org.eventb.texttools.text_lastmodified="1706564431832" 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" version="5">
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
3 
    <org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Fabric_Ethereum_m2"/>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 
    <org.eventb.core.seesContext name="_8rq0TL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Fabric_Ethereum_c2"/>
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUp" 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="_BvYlnL7vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM"/>
        <org.eventb.core.action name="_BvYlxb7vEe6laZimEYihUg" 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="_BvYlm77vEe6laZimEYihUg"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="_BvYlxr7vEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv31;" org.eventb.core.predicate="estimated_cross_chain_cost ∈ ℕ" org.eventb.emf.persistence.emf_id="_BvYlh77vEe6laZimEYihUg"/>
    <org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_BvYlgL7vEe6laZimEYihUg"/>
    <org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_BvYlgb7vEe6laZimEYihUg"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_BvYlgr7vEe6laZimEYihUg"/>
    <org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_BvYlg77vEe6laZimEYihUg"/>
    <org.eventb.core.variable name="_yREdbb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_BvYlhL7vEe6laZimEYihUg"/>
    <org.eventb.core.variable name="_8rz-D77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="accounts" org.eventb.emf.persistence.emf_id="_BvYlhb7vEe6laZimEYihUg"/>
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUh" 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="_BvYlib7vEe6laZimEYihUg">
        <org.eventb.core.action name="_BvYlx77vEe6laZimEYihUg" 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="_BvYliL7vEe6laZimEYihUg"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUi" 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="_BvYli77vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUj" 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="_BvYljb7vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CROSS_CHAIN_TRANSACTION_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUk" 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="_BvYlj77vEe6laZimEYihUg">
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
26 27 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="PROCESS_CROSS_CHAIN_TRANSACTION_IN_FABRIC"/>
    </org.eventb.core.event>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
28 29 
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUl" 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="_BvYlkb7vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_SMART_CONTRACT_EVENT_IN_FABRIC"/>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
30 
    </org.eventb.core.event>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
31 32 33 
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUm" 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="_BvYllL7vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CROSS_CHAIN_TRANSACTION_TO_ETHEREUM"/>
        <org.eventb.core.guard name="_BvYlyL7vEe6laZimEYihUg" 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="_BvYlk77vEe6laZimEYihUg"/>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
34 
    </org.eventb.core.event>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
35 36 
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUn" 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="_BvYllr7vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="CREATE_ADDRESS_IN_ETHEREUM"/>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
37 
    </org.eventb.core.event>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
38 39 40 
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUo" 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="_BvYlmb7vEe6laZimEYihUg">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM"/>
        <org.eventb.core.guard name="_BvYlyb7vEe6laZimEYihUg" 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="_BvYlmL7vEe6laZimEYihUg"/>
Guzman Llambias's avatar
Minor fixes  
Guzman Llambias committed
41 
    </org.eventb.core.event>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
42 
    <org.eventb.core.variable name="_BvYlyr7vEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="estimated_cross_chain_cost" org.eventb.emf.persistence.emf_id="_BvYlhr7vEe6laZimEYihUg"/>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
43 
</org.eventb.core.machineFile>