From 6b3a289733afea1423388e6a05782601489dc03e Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 10 Jul 2023 21:25:59 +0000 Subject: [PATCH] remove some dead code from garagedoor funcs, tidy --- src/Bedrock/End2End/X25519/GarageDoorTop.v | 33 +++++++++++++++++----- 1 file changed, 26 insertions(+), 7 deletions(-) diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v index 51c54b4684..8829a959da 100644 --- a/src/Bedrock/End2End/X25519/GarageDoorTop.v +++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v @@ -25,6 +25,7 @@ Require Import bedrock2Examples.memconst. Require Import Rupicola.Examples.Net.IPChecksum.IPChecksum. Require Import Crypto.Bedrock.End2End.X25519.GarageDoor. Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties. +Import Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20. Local Open Scope string_scope. Import Syntax Syntax.Coercions NotationsCustomEntry. Import ListNotations. @@ -39,14 +40,29 @@ Definition memconst_pk := memconst garageowner. Definition ip_checksum := ip_checksum_br2fn. Definition funcs := - &[, init; loop; - initfn; loopfn; + &[, (* Main loop *) init; loop; initfn; loopfn; + + (* Ethernet & SPI drivers *) + lan9250_tx; recvEthernet; lan9250_init; + lan9250_wait_for_boot; lan9250_mac_write; + lan9250_writeword; lan9250_readword; + SPI.spi_xchg; SPI.spi_write; SPI.spi_read; + + (* "Standard library" of bedrock2 *) memswap; memequal; memconst_pk; - ip_checksum; - ChaCha20.chacha20_block; ChaCha20.quarter; - lan9250_tx ] - ++lightbulb.function_impls - ++MontgomeryLadder.funcs. + + (* Generated using Rupicola *) + ip_checksum; chacha20_block; quarter] + + (* X25519, generated code and handwritten wrappers *) + ++MontgomeryLadder.funcs. + +(* +Compute (length funcs-3)%nat. (* functions excluding main-loop boilerplate *) +Compute ((length MontgomeryLadder.funcs - 2 + 3))%nat. (* generated functions *) +Compute (length funcs-3 - (length MontgomeryLadder.funcs - 2 + 3))%nat. (* handwritten functions *) +Compute bedrock2.ToCString.c_module funcs. +*) Lemma chacha20_ok: forall functions, ChaCha20.spec_of_chacha20 (&,ChaCha20.chacha20_block::&,ChaCha20.quarter::functions). intros. @@ -98,6 +114,9 @@ Definition garagedoor_stack_size := snd garagedoor_compiler_result. Definition garagedoor_finfo := snd (fst garagedoor_compiler_result). Definition garagedoor_insns := fst (fst garagedoor_compiler_result). Definition garagedoor_bytes := Pipeline.instrencode garagedoor_insns. +(* +Compute length garagedoor_bytes. +*) Definition garagedoor_symbols : list byte := Symbols.symbols garagedoor_finfo. Require Import compiler.CompilerInvariant.