[DO NOT MERGE] Bench garagedoor april

.github/workflows/coq-debian.yml

@@ -40,172 +40,6 @@ jobs:
     - name: chroot build params
       shell: in-debian-chroot.sh {0}
       run: CI=1 etc/ci/describe-system-config.sh
-    - name: make deps
+    - name: make garagedoor
       shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 deps
-    - name: all-except-generated-and-js-of-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml
-    - name: generated-files
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 generated-files
-    - run: tar -czvf generated-files.tgz fiat-*/
-      if: ${{ failure() }}
-    - name: upload generated files
-      uses: actions/upload-artifact@v3
-      with:
-        name: generated-files-${{ matrix.env.DEBIAN }}
-        path: generated-files.tgz
-      if: ${{ failure() }}
-    - name: install-standalone-unified-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
-    - name: standalone-js-of-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml
-    - name: install-standalone-js-of-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
-    - name: upload standalone files
-      uses: actions/upload-artifact@v3
-      with:
-        name: standalone-${{ matrix.env.DEBIAN }}
-        path: dist/fiat_crypto
-    - name: upload standalone js files
-      uses: actions/upload-artifact@v3
-      with:
-        name: standalone-html-${{ matrix.env.DEBIAN }}
-        path: fiat-html
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v3
-      with:
-        name: ExtractionOCaml-${{ matrix.env.DEBIAN }}
-        path: src/ExtractionOCaml
-      if: always ()
-    - name: upload js_of_ocaml files
-      uses: actions/upload-artifact@v3
-      with:
-        name: ExtractionJsOfOCaml-${{ matrix.env.DEBIAN }}
-        path: src/ExtractionJsOfOCaml
-      if: always ()
-    - name: standalone-haskell
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
-    - name: upload Haskell files
-      uses: actions/upload-artifact@v3
-      with:
-        name: ExtractionHaskell-${{ matrix.env.DEBIAN }}
-        path: src/ExtractionHaskell
-      if: always ()
-    - name: only-test-amd64-files-lite
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
-    - name: install
-      shell: in-debian-chroot.sh {0}
-      run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
-    - name: install-without-bedrock2
-      shell: in-debian-chroot.sh {0}
-      run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
-    - name: install-dev
-      shell: in-debian-chroot.sh {0}
-      run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
-    - name: display timing info
-      run: cat time-of-build-pretty.log
-    - name: display per-line timing info
-      run: etc/ci/github-actions-display-per-line-timing.sh
-
-  test-standalone:
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-        - debian: sid
-        #- debian: bookworm # restore once 8.17 lands in Debian stable
-    runs-on: ubuntu-latest
-    needs: build
-    steps:
-    - uses: actions/checkout@v4
-    - name: Download standalone ${{ matrix.debian }}
-      uses: actions/download-artifact@v3
-      with:
-        name: standalone-${{ matrix.debian }}
-        path: dist/
-    - name: List files
-      run: find dist
-    - run: chmod +x dist/fiat_crypto
-    - name: Test files (host)
-      run: |
-        echo "::group::file fiat_crypto"
-        file dist/fiat_crypto
-        echo "::endgroup::"
-        echo "::group::ldd fiat_crypto"
-        ldd dist/fiat_crypto
-        echo "::endgroup::"
-        etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-    - name: setup Debian chroot
-      run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}"
-    - name: Test files (container)
-      shell: in-debian-chroot.sh {0}
-      run: |
-        echo "::group::file fiat_crypto"
-        file dist/fiat_crypto
-        echo "::endgroup::"
-        echo "::group::ldd fiat_crypto"
-        ldd dist/fiat_crypto
-        echo "::endgroup::"
-        etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-
-  publish-standalone-dry-run:
-    runs-on: ubuntu-latest
-    needs: build
-#    permissions:
-#      contents: write  # IMPORTANT: mandatory for making GitHub Releases
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        fetch-depth: 0 # Fetch all history for all tags and branches
-        tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
-    - name: Download standalone sid
-      uses: actions/download-artifact@v3
-      with:
-        name: standalone-sid
-        path: dist/
-    - name: List files
-      run: find dist
-    - name: Rename files
-      run: |
-        echo "::group::find arch"
-        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
-        tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}"
-        echo "$fname"
-        mv dist/fiat_crypto "dist/$fname"
-        find dist
-#    - name: Upload artifacts to GitHub Release
-#      env:
-#        GITHUB_TOKEN: ${{ github.token }}
-#      # Upload to GitHub Release using the `gh` CLI.
-#      # `dist/` contains the built packages
-#      run: >-
-#        gh release upload
-#        '${{ github.ref_name }}' dist/**
-#        --repo '${{ github.repository }}'
-#      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
-
-  debian-check-all:
-    runs-on: ubuntu-latest
-    needs: [build, test-standalone, publish-standalone-dry-run]
-    if: always()
-    steps:
-    - run: echo 'build passed'
-      if: ${{ needs.build.result == 'success' }}
-    - run: echo 'test-standalone passed'
-      if: ${{ needs.test-standalone.result == 'success' }}
-    - run: echo 'publish-standalone-dry-run passed'
-      if: ${{ needs.publish-standalone-dry-run.result == 'success' }}
-    - run: echo 'build failed' && false
-      if: ${{ needs.build.result != 'success' }}
-    - run: echo 'test-standalone failed' && false
-      if: ${{ needs.test-standalone.result != 'success' }}
-    - run: echo 'publish-standalone-dry-run failed' && false
-      if: ${{ needs.publish-standalone-dry-run.result != 'success' }}
+      run: /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo

src/Bedrock/End2End/X25519/GarageDoor.v

@@ -181,14 +181,14 @@ Goal True.
 Abort.
 
 Definition protocol_step : state -> list MMIO -> state -> Prop :=
-  fun '(Build_state seed sk) ioh '(Build_state SEED SK) =>
+  fun '(Build_state seed x25519_ephemeral_secret) ioh '(Build_state SEED SK) =>
   (lightbulb_spec.lan9250_recv_no_packet _ ioh \/
     lightbulb_spec.lan9250_recv_packet_too_long _ ioh \/
-    TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) /\ SEED=seed /\ SK=sk \/
+    TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) /\ SEED=seed /\ SK=x25519_ephemeral_secret \/
   (exists incoming, lightbulb_spec.lan9250_recv _ incoming ioh /\
   let ethertype := le_combine (rev (firstn 2 (skipn 12 incoming))) in ethertype < 1536 \/
   let ipproto := nth 23 incoming x00 in (ipproto <> x11 \/
-  length incoming <> 14+20+8 +2+16 +4 /\ length incoming <> 14+20+8 +2+32 +4)%nat) /\ SEED=seed /\ SK=sk \/
+  length incoming <> 14+20+8 +2+16 +4 /\ length incoming <> 14+20+8 +2+32 +4)%nat) /\ SEED=seed /\ SK=x25519_ephemeral_secret \/
   exists (mac_local mac_remote : tuple byte 6),
   exists (ethertype : Z) (ih_const : tuple byte 2) (ip_length : Z) (ip_idff : tuple byte 5),
   exists (ipproto := x11) (ip_checksum : Z) (ip_local ip_remote : tuple byte 4),
@@ -209,28 +209,29 @@ Definition protocol_step : state -> list MMIO -> state -> Prop :=
       (TracePredicate.one ("st", lightbulb_spec.GPIO_DATA_ADDR _, action))) ioh
    /\ (
     let m := firstn 16 garagedoor_payload in
-    let v := x25519_spec sk garageowner_P in
+    let v := x25519_spec x25519_ephemeral_secret garageowner_P in
     exists set0 set1 : Naive.word32,
     (word.unsigned set0 = 1 <-> firstn 16 v = m) /\
     (word.unsigned set1 = 1 <->  skipn 16 v = m) /\
     action = word.or (word.and doorstate (word.of_Z (Z.clearbit (Z.clearbit (2^32-1) 11) 12))) (word.slu (word.or (word.slu set1 (word.of_Z 1)) set0) (word.of_Z 11)) /\
-    (word.unsigned (word.or set0 set1) = 0 -> SEED=seed /\ SK=sk) /\
+    (word.unsigned (word.or set0 set1) = 0 -> SEED=seed /\ SK=x25519_ephemeral_secret) /\
     (word.unsigned (word.or set0 set1) <> 0 -> SEED++SK = RupicolaCrypto.Spec.chacha20_block seed (ChaCha20.le_split 4 (word.of_Z 0) ++ firstn 12 garageowner))
     )) \/
   TracePredicate.concat (lightbulb_spec.lan9250_recv _ incoming)
   (lightbulb_spec.lan9250_send _
     (let ip_length := 62 in
      let udp_length := 42 in
+
      mac_remote ++ mac_local ++ be2 ethertype ++
-     let ih C := ih_const ++ be2 ip_length ++
-                 ip_idff ++ [ipproto] ++ le_split 2 C ++
-                 ip_local ++ ip_remote in
-     ih (Spec.ip_checksum (ih 0)) ++
-     udp_local ++ udp_remote ++
-     be2 udp_length ++ be2 0 ++
+     let ip_hdr checksum := ih_const ++ be2 ip_length ++
+                            ip_idff ++ [ipproto] ++ le_split 2 checksum ++
+                            ip_local ++ ip_remote in
+     ip_hdr (IPChecksum.Spec.ip_checksum (ip_hdr 0)) ++
+     udp_local ++ udp_remote ++ be2 udp_length ++ be2 0 ++
      garagedoor_header ++
-     x25519_spec sk Curve25519.M.B))
-  ioh /\ SEED=seed /\ SK=sk.
+       x25519_spec x25519_ephemeral_secret Curve25519.M.B
+
+  )) ioh /\ SEED=seed /\ SK=x25519_ephemeral_secret.
 
 Local Instance spec_of_recvEthernet : spec_of "recvEthernet" := spec_of_recvEthernet.
 Local Instance spec_of_lan9250_tx : spec_of "lan9250_tx" := spec_of_lan9250_tx.

src/Bedrock/End2End/X25519/GarageDoorTop.v

@@ -1,4 +1,4 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Spec.Curve25519.
@@ -173,7 +173,7 @@
 Local Notation boot_seq := BootSeq.
 
 Definition protocol_spec l := exists s s', labeled_transitions protocol_step s s' l.
-Definition io_spec : list LogItem -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec).
+Definition io_spec : list _ -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec).
 
 Import ExprImpEventLoopSpec.
 Definition garagedoor_spec : ProgramSpec := {|
@@ -259,6 +259,7 @@
 Local Notation run1 := (mcomp_sat (run1 Decode.RV32IM)).
 Local Notation RiscvMachine := MetricRiscvMachine.
 Goal True.
+  pose (lan9250_writepacket (bs : list byte) : list MMIO -> Prop).
   pose (run1 : RiscvMachine -> (RiscvMachine -> Prop) -> Prop).
   pose (always(iset:=Decode.RV32IM) : (RiscvMachine -> Prop) -> RiscvMachine -> Prop).
 Abort.