bump bedrock2 for func! Notations and clean up

output-tests/Crypto.Bedrock.Group.ScalarMult.LadderStep.ladderstep_body.expected

@@ -1,7 +1,6 @@
 ladderstep_body = 
 fun (width : Z) (BW : Bitwidth width) (word : word width) (mem : map.map word byte) (word_ok : word.ok word) (mem_ok : map.ok mem)
   (field_parameters : FieldParameters) (field_representaton : FieldRepresentation) =>
-("ladderstep",
 (["X1"; "X2"; "Z2"; "X3"; "Z3"], [],
 noreassign
   (noskips
@@ -26,8 +25,8 @@ noreassign
                                                            (cmd.seq (cmd.call [] add ["Z2"; "A"; "Z2"])
                                                               (cmd.seq (cmd.call [] mul ["Z2"; "E"; "Z2"])
                                                                  (fold_right (fun (v : string) (c : Syntax.cmd) => cmd.seq (cmd.unset v) c)
-                                                                    cmd.skip []))))))))))))))))))))))))
+                                                                    cmd.skip [])))))))))))))))))))))))
      : forall (width : Z) (BW : Bitwidth width) (word : word width) (mem : map.map word byte),
-       word.ok word -> map.ok mem -> forall field_parameters : FieldParameters, FieldRepresentation -> bedrock_func
+       word.ok word -> map.ok mem -> forall field_parameters : FieldParameters, FieldRepresentation -> Syntax.func
 
 Arguments ladderstep_body {width}%Z_scope {BW word mem word_ok mem_ok field_parameters field_representaton}

output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected

@@ -22,11 +22,11 @@
                                                                (expr.load access_size.one (expr.op bopname.add "K" (expr.op bopname.sru "_gs_i0" 3)))
                                                                (expr.op bopname.and "_gs_i0" 7)) 1))
                                                       (cmd.seq (cmd.set "swap" (expr.op bopname.xor "swap" "s_i"))
-                                                         (cmd.seq (cmd.call [] felem_cswap ["swap"; "X1"; "X2"])
-                                                            (cmd.seq (cmd.call [] felem_cswap ["swap"; "Z1"; "Z2"])
+                                                         (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "X1"; "X2"])
+                                                            (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "Z1"; "Z2"])
                                                                (cmd.seq (cmd.call [] "ladderstep" ["U"; "X1"; "Z1"; "X2"; "Z2"])
                                                                   (cmd.seq (cmd.set "swap" "s_i") (cmd.seq (cmd.unset "s_i") cmd.skip)))))))))
-                                             (cmd.seq (cmd.call [] felem_cswap ["swap"; "X1"; "X2"])
-                                                (cmd.seq (cmd.call [] felem_cswap ["swap"; "Z1"; "Z2"])
+                                             (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "X1"; "X2"])
+                                                (cmd.seq (cmd.call [] "felem_cswap" ["swap"; "Z1"; "Z2"])
                                                    (cmd.seq (cmd.call [] "fe25519_inv" ["OUT"; "Z1"]) (cmd.seq (cmd.call [] mul ["OUT"; "X1"; "OUT"]) cmd.skip))))))))))))))))))
-     : bedrock_func
+     : string * func

src/Bedrock/End2End/RupicolaCrypto/Low.v

@@ -157,7 +157,7 @@ Definition buf_pad {T} (buf: buffer_t T) (len: nat) (t: T) : buffer_t T := buf +
 Require Import bedrock2.NotationsCustomEntry.
 Section CompileBufPolymorphic.
   Import ProgramLogic.Coercions WeakestPrecondition.
-  Context (e : list Syntax.func).
+  Context (e : list (String.string * Syntax.func)).
   Context (T : Type) (sz : word) (pT : word -> T -> mem -> Prop).
 
   Declare Scope word_scope.
@@ -1039,7 +1039,7 @@ Hint Extern 8 (WeakestPrecondition.cmd _ _ _ _ _ (_ (nlet_eq _ (buf_append _ _)
        compile_buf_append; shelve : compiler.
 
 Section CompileBufByte.
-  Context (e : list Syntax.func).
+  Context (e : list (String.string * Syntax.func)).
   Context (T := byte) (sz : word := word.of_Z 1) (pT := ptsto(map:=mem)).
 
   Declare Scope word_scope.
@@ -1138,7 +1138,7 @@ Section CompileBufByte.
 End CompileBufByte.
 
 Section CompileBufWord32.
-  Context (e : list Syntax.func).
+  Context (e : list (String.string  * Syntax.func)).
   Context (T := word) (sz : word := word.of_Z 4) (pT := scalar32(word:=word)).
 
   Declare Scope word_scope.

src/Bedrock/End2End/X25519/Field25519.v

@@ -1,7 +1,8 @@
-Require Import Coq.Strings.String.
+Require Import Coq.Strings.String. Local Open Scope string_scope.
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
 Require Import coqutil.Word.Bitwidth32.
+Require Import coqutil.Macros.WithBaseName.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Bedrock.Field.Common.Names.VarnameGenerator.
 Require Import Crypto.Bedrock.Field.Interface.Representation.
@@ -61,88 +62,71 @@ Section Field.
                       spec_of_from_bytes
                         (ext_spec:=ext_spec)
                         (field_representation:=field_representation n s c)
-                        (fe25519_from_bytes :: functions))
+                        (&,fe25519_from_bytes :: functions))
          As fe25519_from_bytes_correct.
   Proof. Time derive_bedrock2_func from_bytes_op. Qed.
 
   Derive fe25519_to_bytes
          SuchThat (forall functions,
                       spec_of_to_bytes
                         (field_representation:=field_representation n s c)
-                        (fe25519_to_bytes :: functions))
+                        (&,fe25519_to_bytes :: functions))
          As fe25519_to_bytes_correct.
   Proof. Time derive_bedrock2_func to_bytes_op. Qed.
 
   Derive fe25519_copy
          SuchThat (forall functions,
                       spec_of_felem_copy
                         (field_representation:=field_representation n s c)
-                        (fe25519_copy :: functions))
+                        (&,fe25519_copy :: functions))
          As fe25519_copy_correct.
   Proof. Time derive_bedrock2_func felem_copy_op. Qed.
 
   Derive fe25519_from_word
          SuchThat (forall functions,
                       spec_of_from_word
                         (field_representation:=field_representation n s c)
-                        (fe25519_from_word :: functions))
+                        (&,fe25519_from_word :: functions))
          As fe25519_from_word_correct.
   Proof. Time derive_bedrock2_func from_word_op. Qed.
 
   Derive fe25519_mul
          SuchThat (forall functions,
                       spec_of_BinOp bin_mul
                         (field_representation:=field_representation n s c)
-                        (fe25519_mul :: functions))
+                        (&,fe25519_mul :: functions))
          As fe25519_mul_correct.
   Proof. Time derive_bedrock2_func mul_op. Qed.
 
   Derive fe25519_square
          SuchThat (forall functions,
                       spec_of_UnOp un_square
                         (field_representation:=field_representation n s c)
-                        (fe25519_square :: functions))
+                        (&,fe25519_square :: functions))
          As fe25519_square_correct.
   Proof. Time derive_bedrock2_func square_op. Qed.
 
   Derive fe25519_add
          SuchThat (forall functions,
                       spec_of_BinOp bin_add
                         (field_representation:=field_representation n s c)
-                        (fe25519_add :: functions))
+                        (&,fe25519_add :: functions))
          As fe25519_add_correct.
   Proof. Time derive_bedrock2_func add_op. Qed.
 
   Derive fe25519_sub
          SuchThat (forall functions,
                       spec_of_BinOp bin_sub
                         (field_representation:=field_representation n s c)
-                        (fe25519_sub :: functions))
+                        (&,fe25519_sub :: functions))
          As fe25519_sub_correct.
   Proof. Time derive_bedrock2_func sub_op. Qed.
 
   Derive fe25519_scmula24
          SuchThat (forall functions,
                       spec_of_UnOp un_scmula24
                         (field_representation:=field_representation n s c)
-                        (fe25519_scmula24 :: functions))
+                        (&,fe25519_scmula24 :: functions))
          As fe25519_scmula24_correct.
   Proof. Time derive_bedrock2_func scmula24_op. Qed.
 End Field.
-
-(* Uncomment below to sanity-check that compilation works *)
-(*
-Require Import bedrock2.Syntax.
-Require Import compiler.Pipeline.
-Require Import compilerExamples.MMIO.
-
-Definition funcs : list func :=
-  [ fe25519_mul;
-    fe25519_add;
-    fe25519_sub;
-    fe25519_square;
-    fe25519_to_bytes;
-    fe25519_from_bytes ].
-
-Compute compile (compile_ext_call (funname_env:=SortedListString.map)) (map.of_list funcs).
-*)

src/Bedrock/End2End/X25519/GarageDoor.v

@@ -37,16 +37,15 @@ Local Notation ST := 0x80000000.
 Local Notation PK := 0x80000040.
 Local Notation BUF:= 0x80000060.
 
-Definition initfn : func :=
-  ("initfn", ([], [], bedrock_func_body:(
-    $(memconst "pk" garageowner)($PK);
-    output! MMIOWRITE($0x10012038, $(Z.lor (Z.shiftl (0xf) 2) (Z.shiftl 1 9)));
-    output! MMIOWRITE($0x10012008, $(Z.lor (Z.shiftl 1 11) (Z.shiftl 1 12)));
-    output! MMIOWRITE($0x10024010, $2);
-    unpack! err = lan9250_init()
-  ))).
-
-Definition loopfn : func := ("loopfn", ([], [], bedrock_func_body:(
+Definition initfn := func! {
+  memconst_pk($PK);
+  output! MMIOWRITE($0x10012038, $(Z.lor (Z.shiftl (0xf) 2) (Z.shiftl 1 9)));
+  output! MMIOWRITE($0x10012008, $(Z.lor (Z.shiftl 1 11) (Z.shiftl 1 12)));
+  output! MMIOWRITE($0x10024010, $2);
+  unpack! err = lan9250_init()
+}.
+
+Definition loopfn := func! {
   st=$ST; pk=$PK; buf=$BUF;
   unpack! l, err = recvEthernet(buf);
   require !err;
@@ -91,7 +90,7 @@ Definition loopfn : func := ("loopfn", ([], [], bedrock_func_body:(
         chacha20_block(st, st, (*nonce*)pk, $0) (* NOTE: another impl? *)
     }
   }
-))).
+}.
 
 Import TracePredicate TracePredicateNotations SPI lightbulb_spec.
 Notation OP := (lightbulb_spec.OP _).
@@ -107,7 +106,7 @@ Definition BootSeq : list OP -> Prop :=
 Import WeakestPrecondition ProgramLogic SeparationLogic.
 Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Global Instance spec_of_initfn : spec_of initfn :=
+Global Instance spec_of_initfn : spec_of "initfn" :=
   fnspec! "initfn" / bs R,
   { requires t m := m =* bs $@(word.of_Z PK) * R /\ length bs = 32%nat;
     ensures t' m' := m' =* garageowner$@(word.of_Z PK) * R /\
@@ -123,8 +122,8 @@ Ltac fwd :=
          end; trivial.
 Ltac slv := try solve [ trivial | ecancel_assumption | SepAutoArray.listZnWords | intuition idtac | reflexivity | eassumption].
 
-Local Instance spec_of_memconst_pk : spec_of "memconst_pk" := spec_of_memconst "pk" garageowner.
-Local Instance WHY_spec_of_lan9250_init : spec_of lan9250_init := spec_of_lan9250_init.
+Local Instance spec_of_memconst_pk : spec_of "memconst_pk" := spec_of_memconst "memconst_pk" garageowner.
+Local Instance WHY_spec_of_lan9250_init : spec_of "lan9250_init" := spec_of_lan9250_init.
 Lemma initfn_ok : program_logic_goal_for_function! initfn.
 Proof.
   repeat straightline.
@@ -235,7 +234,7 @@ Definition memrep bs R : state -> map.rep(map:=SortedListWord.map _ _) -> Prop :
   length sk = 32%nat /\
   length bs = 1520%nat.
 
-Global Instance spec_of_loopfn : spec_of loopfn :=
+Global Instance spec_of_loopfn : spec_of "loopfn" :=
   fnspec! "loopfn" / seed sk bs R,
   { requires t m := memrep bs R (seed, sk) m;
     ensures T M := exists SEED SK BS, memrep BS R (SEED, SK) M /\
@@ -911,22 +910,25 @@ Qed.
 
 Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties.
 Import bedrock2.Syntax.
+Import coqutil.Macros.WithBaseName.
 
 (* these wrappers exist because CompilerInvariant requires execution proofs with arbitrary locals in the starting state, which ProgramLogic does not support *)
-Definition init : func := ("init", ([], [], (cmd.call [] "initfn" []))).
-Definition loop : func := ("loop", ([], [], (cmd.call [] "loopfn" []))).
+Definition init := func! { initfn() } .
+Definition loop := func! { loopfn() } .
+Definition memconst_pk := memconst garageowner.
+Definition ip_checksum := ip_checksum_br2fn.
 
-Definition funcs : list Syntax.func :=
-  [ init; loop;
+Definition funcs :=
+  &[, init; loop;
     initfn; loopfn;
-    memswap; memequal; memconst "pk" garageowner;
-    ip_checksum_br2fn;
+    memswap; memequal; memconst_pk;
+    ip_checksum;
     chacha20_block; chacha20_quarter;
     lan9250_tx ]
     ++lightbulb.function_impls
     ++MontgomeryLadder.funcs.
 
-Lemma chacha20_ok: forall functions, spec_of_chacha20 (chacha20_block::chacha20_quarter::functions).
+Lemma chacha20_ok: forall functions, spec_of_chacha20 (&,chacha20_block::&,chacha20_quarter::functions).
 Admitted.
 
 Import SPI.
@@ -1046,8 +1048,8 @@ Proof.
   2,3:vm_compute; inversion 1.
   econstructor (* ProgramSatisfiesSpec *).
   1: vm_compute; reflexivity.
-  1: instantiate (1:=snd (snd init)).
-  3: instantiate (1:=snd (snd loop)).
+  1: instantiate (1:=snd init).
+  3: instantiate (1:=snd loop).
   1,3: exact eq_refl.
   1,2: cbv [hl_inv]; intros; eapply WeakestPreconditionProperties.sound_cmd.
   1,3: eapply Crypto.Util.Bool.Reflect.reflect_bool; vm_compute; reflexivity.

src/Bedrock/End2End/X25519/MontgomeryLadder.v

@@ -29,21 +29,21 @@ Proof. vm_compute. subst; exact eq_refl. Qed.
 
 Require Import bedrock2.NotationsCustomEntry.
 
-Definition x25519 : func := ("x25519", (["out"; "sk"; "pk"], [], bedrock_func_body:(
+Definition x25519 := func! (out, sk, pk) {
   stackalloc 40 as U;
   fe25519_from_bytes(U, pk);
   stackalloc 40 as OUT;
   montladder(OUT, sk, U);
   fe25519_to_bytes(out, OUT)
-))).
+}.
 
-Definition x25519_base : func := ("x25519_base", (["out"; "sk"], [], bedrock_func_body:(
+Definition x25519_base := func! (out, sk) {
   stackalloc 40 as U;
   fe25519_from_word(U, $9);
   stackalloc 40 as OUT;
   montladder(OUT, sk, U);
   fe25519_to_bytes(out, OUT)
-))).
+}.
 
 Import LittleEndianList.
 Local Coercion F.to_Z : F >-> Z.
@@ -54,7 +54,7 @@ Import ProgramLogic.Coercions.
 Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
 Definition x25519_gallina := montladder_gallina (Field.M_pos(FieldParameters:=field_parameters)) Field.a24 (Z.to_nat (Z.log2 (Z.pos order))).
-Global Instance spec_of_x25519 : spec_of x25519 :=
+Global Instance spec_of_x25519 : spec_of "x25519" :=
   fnspec! "x25519" out sk pk / (o s p : list Byte.byte) (R : _ -> Prop),
   { requires t m := m =* s$@sk * p$@pk * o$@out * R /\
       length s = 32%nat /\ length p = 32%nat /\ length o = 32%nat /\ byte.unsigned (nth 31 p x00) <= 0x7f;
@@ -123,7 +123,7 @@ Proof.
   use_sep_assumption; cancel. eapply RelationClasses.reflexivity.
 Qed.
 
-Global Instance spec_of_x25519_base : spec_of x25519_base :=
+Global Instance spec_of_x25519_base : spec_of "x25519_base" :=
   fnspec! "x25519_base" out sk / (o s : list Byte.byte) (R : _ -> Prop),
   { requires t m := m =* s$@sk * o$@out * R /\
       length s = 32%nat /\ length o = 32%nat;
@@ -170,25 +170,29 @@ Proof.
 Qed.
 
 Require Import coqutil.Word.Naive.
+Require Import coqutil.Macros.WithBaseName.
 
-Definition funcs : list func :=
-  [ x25519; x25519_base;
+Definition felem_cswap := CSwap.felem_cswap(word:=word32)(field_parameters:=field_parameters)(field_representaton:=field_representation n s c).
+Definition fe25519_inv := fe25519_inv(word:=word32)(field_parameters:=field_parameters).
+
+Definition funcs :=
+  &[,x25519; x25519_base;
     montladder;
     fe25519_to_bytes;
     fe25519_from_bytes;
     fe25519_from_word;
-    CSwap.cswap_body(word:=word32)(field_parameters:=field_parameters)(field_representaton:=field_representation n s c);
+    felem_cswap;
     fe25519_copy;
-    fe25519_inv(word:=word32)(field_parameters:=field_parameters);
+    fe25519_inv;
     ladderstep;
     fe25519_mul;
     fe25519_add;
     fe25519_sub;
     fe25519_square;
     fe25519_scmula24 ].
 
-
-Definition montladder_c_module := ToCString.c_module funcs.
+Require Import bedrock2.ToCString.
+Definition montladder_c_module := list_byte_of_string (ToCString.c_module funcs).
 
 #[export]
 Instance BWM_RV32IM : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl.

src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v

@@ -18,17 +18,9 @@ Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadder.
 
 Local Arguments map.rep: clear implicits.
 
-Definition fname := fst montladder.
-Definition argnames := fst (fst (snd montladder)).
-Definition retnames := snd (fst (snd montladder)).
-Definition fbody := snd (snd montladder).
-Definition f_rel_pos : Z.
-  let x := constr:(List.find (fun '(name, pos) => String.eqb name fname) montladder_finfo) in
-  let y := eval vm_compute in x in
-  match y with
-  | Some (_, ?pos) => exact pos
-  end.
-Defined.
+Definition f_rel_pos : Z := ltac:(
+  let y := eval vm_compute in (List.find (fun '(name, pos) => String.eqb name "montladder") montladder_finfo) in
+  match y with Some (_, ?pos) => exact pos end).
 
 Local Instance mem : map.map (word.rep (width:=32)) Init.Byte.byte := SortedListWord.map _ _.
 Local Existing Instance BW32.
@@ -224,8 +216,8 @@ Proof.
             (ext_spec:=FE310CSemantics.ext_spec)
             (string_keyed_map := SortedListString.map)
             (string_keyed_map_ok := SortedListString.ok))
-    with (fname:=fname).
-  all:cbn [fname montladder fst snd].
+    with (fname:="montladder").
+  all:cbn [montladder fst snd].
 
   (* fill in easy subgoals that instantiate evars *)
   all:lazymatch goal with