certora-review-receiver.yml

name: certora-review-receiver

on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main

  workflow_dispatch:

jobs:
  verify:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v2
        with:
          submodules: recursive

      - name: Install python
        uses: actions/setup-python@v2
        with: { python-version: 3.9 }

      - name: Install java
        uses: actions/setup-java@v1
        with: { java-version: "11", java-package: jre }

      - name: Install certora cli
        run: pip3 install certora-cli==4.13.1

      - name: Install solc
        run: |
          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
          chmod +x solc-static-linux
          sudo mv solc-static-linux /usr/local/bin/solc8.19

      - name: Verify rule ${{ matrix.rule }}
        run: |
          cd security/certora
          touch applyHarness.patch
          make munged
          cd ../..
          certoraRun security/certora/confs/${{ matrix.rule }}
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}

    strategy:
      fail-fast: false
      max-parallel: 16
      matrix:
        rule:
          - verifyCrossChainControllerWithEmergency.conf
          #- verifyCrossChainReceiver.conf --rule receive_more_than__requiredConfirmations_diff_2 # TODO: uncomment when moving to cli 5.0.2 or higher
          #- verifyCrossChainReceiver.conf --rule receive_more_than__requiredConfirmations_diff_3 # TODO: uncomment when moving to cli 5.0.2 or higher
          - verifyCrossChainReceiver.conf --rule transaction_received_only_from_authorized_bridge_adapter only_owner_can_change_bridge_adapters only_owner_can_change_bridge_adapters_witness_consequent only_owner_can_change_required_confirmations only_owner_can_change_required_confirmations_witness_consequent cannot_call_IBaseReceiverPortal_receiveCrossChainMessage_twice cannot_call_IBaseReceiverPortal_receiveCrossChainMessage_twice_witness_tight_bound state_transition_to_deliver_iff_IBaseReceiverPortal_receiveCrossChainMessage_called
          - verifyCrossChainReceiver.conf --rule state_transition_to_deliver_iff_IBaseReceiverPortal_receiveCrossChainMessage_called_witness_antecedent call_deliverEnvelope_once_witness_antecedent anyone_can_call_deliverEnvelope invalidate_previous_unconfirmed_envelopes_after_updateMessagesValidityTimestamp_witness_antecedent receiveCrossChainMessage_cannot_change_state_if_requiredConfirmation_is_zero envelope_state envelope_state_witness_none_to_delivered only_single_bridge_adapter_added only_single_bridge_adapter_removed
          - verifyCrossChainReceiver.conf --rule envelope_state_witness_confirmed_to_delivered envelope_state_witness_none_to_confirmed envelope_state_witness_none_none_confirmed envelope_state_witness_none_confirmed_confirmed envelope_state_witness_confirmed_confirmed_confirmed confirmations_increments_if_received_from_msg_sender confirmations_increments_if_received_from_msg_sender_witness allowReceiverBridgeAdapters_cannot_disallow allowReceiverBridgeAdapters_cannot_disallow_witness
          - verifyCrossChainReceiver.conf --rule disallowReceiverBridgeAdapters_cannot_allow disallowReceiverBridgeAdapters_cannot_allow_witness_antecedent disallowReceiverBridgeAdapters_cannot_allow_witness_consequent requiredConfirmation_is_positive_after_updateConfirmations receive_increments_confirmations     
          - verifyCrossChainReceiver.conf --rule reachability encodeDecodeWorks encodeDecodeWorks_witness encodeDecodeWorks_witness_2 
          - verifyCrossChainReceiver.conf --rule firstBridgedAt_happened_in_the_past  
          - verifyCrossChainReceiver.conf --rule no_deliverEnvelope_after_receiveCrossChainMessage 
          #- verifyCrossChainReceiver.conf --rule call_deliverEnvelope_once # TODO: uncomment when moving to cli 5.0.2 or higher
          #- verifyCrossChainReceiver.conf --rule invalidate_previous_unconfirmed_envelopes_after_updateMessagesValidityTimestamp # TODO: uncomment when moving to cli 5.0.2 or higher
          #- verifyCrossChainReceiver.conf --rule addressSetInvariant # TODO: uncomment when moving to cli 5.0.2 or higher
          #- verifyCrossChainReceiver.conf --rule cannot_call_BaseReceiverPortal_receiveCrossChainMessage_twice # TODO: uncomment when moving to cli 5.0.2 or higher
          - verifyCrossChainReceiver.conf --rule zero_firstBridgedAt_iff_not_received_from_msg_sender