Skip to content

arch-split Refine up to Invariants_H for AARCH64 (Draft) #3091

arch-split Refine up to Invariants_H for AARCH64 (Draft)

arch-split Refine up to Invariants_H for AARCH64 (Draft) #3091

Workflow file for this run

# Copyright 2021 Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
name: Proof PR
on:
push:
paths-ignore:
- '**.md'
- '**.txt'
branches:
- rt
# this action needs access to secrets.
# The actual test runs in a no-privilege VM, so it's Ok to run on untrusted PRs.
pull_request_target:
paths-ignore:
- '**.md'
- '**.txt'
workflow_dispatch:
inputs:
NUM_DOMAINS:
description: 'Number of domains to test'
type: number
default: 16
jobs:
proofs:
name: All
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
# test only most recent push to PR:
concurrency: l4v-pr-${{ github.event.number }}-idx-${{ strategy.job-index }}
steps:
- name: Proofs
uses: seL4/ci-actions/aws-proofs@master
with:
L4V_ARCH: ${{ matrix.arch }}
NUM_DOMAINS: ${{ inputs.NUM_DOMAINS }}
skip_dups: true
session: '-x AutoCorresSEL4' # exclude large AutoCorresSEL4 session for PRs
token: ${{ secrets.READ_TOKEN }}
cache_bucket: ${{ secrets.CACHE_BUCKET }}
env:
AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
AWS_SSH: ${{ secrets.AWS_SSH }}
GH_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
- name: Upload kernel builds
uses: actions/upload-artifact@v4
with:
name: kernel-builds-${{ matrix.arch }}
path: artifacts/kernel-builds
if-no-files-found: ignore
- name: Upload logs
uses: actions/upload-artifact@v4
with:
name: logs-${{ matrix.arch }}
path: logs.tar.xz