gobra.yml

# This Source Code Form is subject to the terms of the Mozilla Public
# License, v. 2.0. If a copy of the MPL was not distributed with this
# file, You can obtain one at http://mozilla.org/MPL/2.0/.
#
# Copyright (c) 2011-2020 ETH Zurich.

name: Verify the router and its dependencies

on:
  push:
    branches:
    - master
  pull_request: # run this workflow on every pull_request

env:
  headerOnly: 1
  module: 'github.com/scionproto/scion'
  includePaths: '. verification/dependencies'
  assumeInjectivityOnInhale: '1'
  parallelizeBranches: '0'
  checkConsistency: '1'
  imageVersion: 'latest'
  mceMode: 'od'
  requireTriggers: '1'
  useZ3API: '0'
  viperBackend: 'SILICON'
  disableNL: '0'
  unsafeWildcardOptimization: '1'
  overflow: '0'

jobs:
  verify-deps:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout the VerifiedSCION repository
        uses: actions/checkout@v3
      # Skip caching for now, the Github action right now is very limited.
      # - name: Cache the verification results
      #   uses: actions/cache@v3
      #   env:
      #     cache-name: gobra-cache
      #   with:
      #     path: ${{ runner.workspace }}/.gobra/cache.json
      #     key: ${{ env.cache-name }}

      # We split the verification of the entire repository into
      # multiple steps. This provides a more fine-grained log in
      # Github Workflow's interface and it allows more fine-grained
      # control over the settings applied to each package (this last
      # point could be also be solved by adapting the action to allow
      # per package config).
      - name: Verify the packages in the 'verification' directory
        uses: viperproject/gobra-action@main
        with:
          projectLocation: 'VerifiedSCION/verification'
          recursive: 1
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: './dependencies/ ..' # relative to project location
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/addr'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/addr'
          timeout: 10m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          statsFile: '/stats/stats_addr.json'
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/experimental/epic'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/experimental/epic'
          timeout: 7m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/log'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/log'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/private/serrors'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/private/serrors'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/scrypto'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/scrypto'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/slayers'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/slayers'
          timeout: 25m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/slayers/path'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/slayers/path'
          timeout: 10m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/slayers/path/empty'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/slayers/path/empty'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/slayers/path/epic'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/slayers/path/epic'
          # timeout increased; we were having frequent timeouts before
          timeout: 10m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/slayers/path/onehop'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/slayers/path/onehop'
          timeout: 10m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'pkg/slayers/path/scion'
        uses: viperproject/gobra-action@main
        with:
          packages: 'pkg/slayers/path/scion'
          timeout: 30m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'private/topology'
        uses: viperproject/gobra-action@main
        with:
          packages: 'private/topology'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'private/topology/underlay'
        uses: viperproject/gobra-action@main
        with:
          packages: 'private/topology/underlay'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'private/underlay/conn'
        uses: viperproject/gobra-action@main
        with:
          packages: 'private/underlay/conn'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'private/underlay/sockctrl'
        uses: viperproject/gobra-action@main
        with:
          packages: 'private/underlay/sockctrl'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'router/bfd'
        uses: viperproject/gobra-action@main
        with:
          packages: 'router/bfd'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Verify package 'router/control'
        uses: viperproject/gobra-action@main
        with:
          packages: 'router/control'
          timeout: 5m
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          parallelizeBranches: ${{ env.parallelizeBranches }}
          imageVersion: ${{ env.imageVersion }}
          mceMode: ${{ env.mceMode }}
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: ${{ env.disableNL }}
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
      - name: Upload the verification report
        uses: actions/upload-artifact@v4
        with:
          name: stats_addr.json
          path: /stats/stats_addr.json
          if-no-files-found: error # could also be 'warn' or 'ignore'
  verify-router:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout the VerifiedSCION repository
        uses: actions/checkout@v3
      - name: Verify package 'router/'
        uses: viperproject/gobra-action@main
        with:
          packages: 'router/'
          timeout: 6h
          headerOnly: ${{ env.headerOnly }}
          module: ${{ env.module }}
          includePaths: ${{ env.includePaths }}
          assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
          checkConsistency: ${{ env.checkConsistency }}
          # Due to a bug introduced in https://github.com/viperproject/gobra/pull/776,
          # we must currently disable the chopper, otherwise we well-founded orders
          # for termination checking are not available at the chopped Viper parts.
          # We should reenable it whenever possible, as it reduces verification time in
          # ~8 min (20%).
          # chop: 10
          parallelizeBranches: '1'
          conditionalizePermissions: '1'
          moreJoins: 'impure'
          imageVersion: ${{ env.imageVersion }}
          mceMode: 'on'
          requireTriggers: ${{ env.requireTriggers }}
          overflow: ${{ env.overflow }}
          useZ3API: ${{ env.useZ3API }}
          disableNL: '0'
          viperBackend: ${{ env.viperBackend }}
          unsafeWildcardOptimization: '0'