Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Preserve_Balance_Gateway_m3.bum 8.5 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
Change trigger for emit event  
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="_lV7wPvKVEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712243476514" 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 emitted_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_CC_TX_IN_FABRIC extends INITIATE_CC_TX_IN_FABRIC&#10;  end&#10;&#10;  event EMIT_CC_TX_EVENT_IN_FABRIC extends EMIT_CC_TX_EVENT_IN_FABRIC&#10;  end&#10;&#10;  event LISTEN_CC_TX_EVENT_IN_FABRIC extends LISTEN_CC_TX_EVENT_IN_FABRIC&#10;  end&#10;&#10;  event SUBMIT_CC_TX_TO_ETHEREUM extends SUBMIT_CC_TX_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 
    <org.eventb.core.seesContext name="_8rq0TL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Fabric_Ethereum_c2"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
5 6 7 8 9 10 11 12 13 14 
    <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="_lV7wK_KVEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_4AD2oMBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX_IN_FABRIC" org.eventb.emf.persistence.emf_id="_lV7wLfKVEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_4AD2ocBFEe6yC4BToIaAqA" org.eventb.core.target="INITIATE_CC_TX_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_jhsycfKVEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_CC_TX_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="_lV7wL_KVEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_jhsycvKVEe60CqkwWvstGA" org.eventb.core.target="EMIT_CC_TX_EVENT_IN_FABRIC"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_ZAfKoMBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_CC_TX_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="_lV7wMfKVEe60CqkwWvstGA">
Guzman Llambias's avatar
Rename abstract machine event names  
Guzman Llambias committed
15 
        <org.eventb.core.refinesEvent name="_ZAfKocBGEe6yC4BToIaAqA" org.eventb.core.target="LISTEN_CC_TX_EVENT_IN_FABRIC"/>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
16 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
17 
    <org.eventb.core.event name="_j630sMBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CC_TX_TO_ETHEREUM" org.eventb.emf.persistence.emf_id="_lV7wNPKVEe60CqkwWvstGA">
Guzman Llambias's avatar
Rename abstract machine event names  
Guzman Llambias committed
18 
        <org.eventb.core.refinesEvent name="_j630scBGEe6yC4BToIaAqA" org.eventb.core.target="SUBMIT_CC_TX_TO_ETHEREUM"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
19 
        <org.eventb.core.guard name="_ySjRNMTuEe609fto5wotHA" 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="_lV7wM_KVEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Minor changes  
Guzman Llambias committed
20 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
21 
    <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="_lV7wNvKVEe60CqkwWvstGA">
Guzman Llambias's avatar
Rename abstract machine event names  
Guzman Llambias committed
22 
        <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
23 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
24 
    <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="_lV7wOfKVEe60CqkwWvstGA">
Guzman Llambias's avatar
Rename abstract machine event names  
Guzman Llambias committed
25 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
26 
        <org.eventb.core.guard name="_ySjRNcTuEe609fto5wotHA" 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="_lV7wOPKVEe60CqkwWvstGA"/>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
27 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
28 
    <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="_lV7wPPKVEe60CqkwWvstGA">
Guzman Llambias's avatar
Rename abstract machine event names  
Guzman Llambias committed
29 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
30 31 32 33 34 35 36 37 38 39 40 41 42 
        <org.eventb.core.action name="_ySsbEMTuEe609fto5wotHA" 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="_lV7wO_KVEe60CqkwWvstGA"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="_ySjRN8TuEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv31" org.eventb.core.predicate="estimated_cross_chain_cost ∈ ℕ" org.eventb.emf.persistence.emf_id="_lV7wJ_KVEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_lV7wIPKVEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_lV7wYPKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_lV7wIfKVEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_lV7wIvKVEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_lV7wI_KVEe60CqkwWvstGA"/>
    <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="_lV7wJPKVEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_8rz-D77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="accounts" org.eventb.emf.persistence.emf_id="_lV7wJfKVEe60CqkwWvstGA"/>
    <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="_lV7wKfKVEe60CqkwWvstGA">
        <org.eventb.core.action name="_ySjRNsTuEe609fto5wotHA" 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="_lV7wKPKVEe60CqkwWvstGA"/>
    </org.eventb.core.event>
    <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="_lV7wJvKVEe60CqkwWvstGA"/>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway
Guzman Llambias committed
43 
</org.eventb.core.machineFile>