Add an LLBC backend

.github/workflows/deny.yml

@@ -18,6 +18,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
+        with:
+          submodules: recursive
       - uses: EmbarkStudios/cargo-deny-action@v2
         with:
           arguments: --all-features --workspace

.github/workflows/format-check.yml

@@ -47,7 +47,7 @@ jobs:
 
       - name: 'Run Clippy'
         run: |
-          cargo clippy --all -- -D warnings
+          cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings
 
       - name: 'Print Clippy Statistics'
         run: |

.github/workflows/kani.yml

@@ -98,6 +98,8 @@ jobs:
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
+        with:
+          submodules: recursive
 
       - name: Install book dependencies
         run: ./scripts/setup/ubuntu/install_doc_deps.sh

.gitignore

@@ -77,6 +77,9 @@ package-lock.json
 ## Rustdoc GUI tests
 tests/rustdoc-gui/src/**.lock
 
+## Charon/Aeneas LLBC files
+*.llbc
+
 # Before adding new lines, see the comment at the top.
 /.ninja_deps
 /.ninja_log

.gitmodules

@@ -5,3 +5,6 @@
 	path = tests/perf/s2n-quic
 	url = https://github.com/aws/s2n-quic
 	branch = main
+[submodule "charon"]
+	path = charon
+	url = https://github.com/AeneasVerif/charon