Cross compile to Aarch64 on Ubuntu

.github/workflows/makefile.yml

@@ -43,11 +43,22 @@ jobs:
         path: .lake
         key: ${{ runner.os }}-lake
 
-    - name: Build AWS-LC (MacOS)
-      if : ${{ runner.os == 'macOS' }}
+    - name: Setup Go (Ubuntu)
+      if: ${{ runner.os != 'macOS' }}
+      uses: actions/setup-go@v4
+      with:
+          go-version: '>=1.18'
+
+    - name: Build AWS-LC (Ubuntu)
+      if : ${{ runner.os != 'macOS' }}
       run: |
           ./scripts/build_awslc.sh
 
+    # - name: Run ELFLoader Tests for AWS-LC (MacOS)
+    #   if : ${{ runner.os == 'macOS' }}
+    #   run: |
+    #       make awslc_elftests
+
     - name: Run LNSym Makefile (Ubuntu)
       if : ${{ runner.os != 'macOS' }}
       run: |

Makefile

@@ -27,10 +27,6 @@ proofs:
 tests:
 	time -p $(LAKE) build Tests
 
-.PHONY: awslc_elftests
-awslc_elftests:
-	time -p $(LAKE) build AWSLCELFTests
-
 .PHONY: cosim
 cosim:
 	time -p lake exe lnsym $(VERBOSE) --num-tests $(NUM_TESTS)

Tests/Tests.lean

@@ -17,6 +17,11 @@ import «Tests».«AES-GCM».AESV8ProgramTests
 import «Tests».«AES-GCM».AESV8SpecTests
 import «Tests».«AES-GCM».AESGCMProgramTests
 import «Tests».«ELFParser».MiscTests
+import «Tests».«ELFParser».AWSLCCrypto
+import «Tests».«ELFParser».AWSLCSHA2
+import «Tests».«ELFParser».AWSLCGCMV8
+import «Tests».«ELFParser».AWSLCAESV8
+import «Tests».«ELFParser».AWSLCAESGCMKernel
 import «Tests».Tactics.CSE
 import «Tests».Tactics.Sym
 import «Tests».Tactics.ReduceFetchInst

scripts/build_awslc.cmake

@@ -0,0 +1,13 @@
+# Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+# Author(s): Yan Peng
+
+# https://cmake.org/cmake/help/book/mastering-cmake/chapter/Cross%20Compiling%20With%20CMake.html
+
+# the name of the target operating system
+set(CMAKE_SYSTEM_NAME Linux)
+set(CMAKE_SYSTEM_PROCESSOR aarch64)
+
+# which compilers to use for C and C++
+set(CMAKE_C_COMPILER   clang)
+set(CMAKE_CXX_COMPILER clang++)

scripts/build_awslc.sh

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 # Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # Released under Apache 2.0 license as described in the file LICENSE.
@@ -10,16 +10,31 @@ set -o xtrace
 # Remember where LNSym is
 LNSym_DIR=${PWD}
 
+MICRO_ARCH="neoverse-n1"
+TARGET="aarch64-unknown-linux-gnu"
+export LDFLAGS="-fuse-ld=lld"
+
 # Install dependencies
-brew install ninja golang
+sudo apt-get update
+sudo apt-get install -y git cmake clang ninja-build lld g++-aarch64-linux-gnu
 
-# Fetching and building AWS-LC
+# Fetching AWS-LC
 git clone https://github.com/aws/aws-lc.git $HOME/aws-lc --depth 1
-cd $HOME/aws-lc; mkdir aws-lc-build; cd aws-lc-build
-cmake -GNinja -DKEEP_ASM_LOCAL_SYMBOLS=1 -DCMAKE_BUILD_TYPE=RelWithDebInfo ../
+cd $HOME/aws-lc
+# Build AWS-LC
+mkdir aws-lc-build; cd aws-lc-build
+cmake -GNinja \
+      -DCMAKE_BUILD_TYPE=RelWithDebInfo \
+      -DKEEP_ASM_LOCAL_SYMBOLS=1 \
+      -DCMAKE_TOOLCHAIN_FILE="${LNSym_DIR}/scripts/build_awslc.cmake" \
+      -DCMAKE_C_FLAGS="-mcpu=${MICRO_ARCH}" \
+      -DCMAKE_CXX_FLAGS="-mcpu=${MICRO_ARCH}" \
+      -DCMAKE_ASM_FLAGS="-mcpu=${MICRO_ARCH}" \
+      -DCMAKE_C_COMPILER_TARGET=$TARGET \
+      -DCMAKE_CXX_COMPILER_TARGET=$TARGET \
+      -DCMAKE_ASM_COMPILER_TARGET=$TARGET \
+      ../
 ninja
 
 # Move crypto_test to LNSym
 cp -f crypto/crypto_test ${LNSym_DIR}/Tests/ELFParser/Data/crypto_test
-
-cd ${LNSym_DIR}