WIP: adapt to stack allocation returning map.of_list_byte_at

mit-plv · Feb 4, 2025 · fb97ef6 · fb97ef6
1 parent f47be1a
commit fb97ef6
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 21 deletions.
diff --git a/rupicola b/rupicola
diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v
@@ -19,6 +19,7 @@ Require Import bedrock2.Map.Separation.
 Require Import bedrock2.Map.SeparationLogic.
 Require Import bedrock2.Memory. Import WithoutTuples.
 Require Import coqutil.Map.Interface. (* coercions *)
+Require Import coqutil.Map.OfListWord.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.LittleEndianList.
 Import Word.Naive.
@@ -29,21 +30,7 @@ Section Memory.
   Context {width: Z} {word: word width} {mem: map.map word byte}.
   Context {mem_ok: map.ok mem} {word_ok: word.ok word}.
   Local Infix "$+" := map.putmany (at level 70).
-  Local Notation "xs $@ a" := (map.of_list_word_at a xs) (at level 10, format "xs $@ a").
   Local Notation unchecked_store_bytes := (unchecked_store_bytes (mem:=mem) (word:=word)).
-  Lemma unchecked_store_bytes_unchecked_store_bytes m a bs1 bs2 :
-    length bs1 = length bs2 ->
-    unchecked_store_bytes (unchecked_store_bytes m a bs1) a bs2 =
-    unchecked_store_bytes m a bs2.
-  Proof using mem_ok word_ok.
-    cbv [unchecked_store_bytes]; intros.
-    eapply map.map_ext; intros.
-    rewrite !map.get_putmany_dec, !map.get_of_list_word_at;
-      repeat (destruct_one_match; trivial).
-    epose proof proj1 (List.nth_error_Some bs1 (BinInt.Z.to_nat (word.unsigned (word.sub k a)))) ltac:(congruence).
-    rewrite H in H0.
-    eapply List.nth_error_Some in E; intuition idtac.
-  Qed.
 
   (* not sure where to put this since depends on sep *)
   Import Map.Interface Word.Interface BinInt.
@@ -58,7 +45,7 @@ Section Memory.
     (Hlen : length bs1 = length bs2)
     : sep R (bs2$@a) (unchecked_store_bytes m a bs2).
   Proof using mem_ok word_ok.
-    destruct Hsep as (?&?&(?&Hd)&HR&?);
+    destruct Hsep as (?&?&(?&Hd)&HR&?); cbv [exact] in *;
       cbv [sepclause_of_map] in *; subst.
     setoid_rewrite unchecked_store_bytes_unchecked_store_bytes; trivial.
     eexists _, _; split; split; try exact HR; try exact eq_refl.

diff --git a/src/Bedrock/Field/Interface/Compilation2.v b/src/Bedrock/Field/Interface/Compilation2.v
@@ -75,6 +75,7 @@ Section Compile.
     size_in_bytes_mod := felem_size_in_bytes_mod;
     |}.
   Proof.
+    { apply field_representation_ok. }
     {
       intros; intros m H.
       apply FElem'_from_bytes.

diff --git a/src/Bedrock/Field/Interface/Representation.v b/src/Bedrock/Field/Interface/Representation.v
@@ -59,5 +59,5 @@ Section Representation.
     }.
 
   Local Instance frep_ok : FieldRepresentation_ok.
-  Proof. split. cbn [bounded_by frep]; intros. apply relax_bounds; auto. Qed.
+  Proof. split; cbn [bounded_by frep]; intros; try apply relax_bounds; auto. Admitted.
 End Representation.
diff --git a/src/Bedrock/Specs/Field.v b/src/Bedrock/Specs/Field.v
@@ -1,4 +1,5 @@
 Require Import coqutil.Byte coqutil.Word.LittleEndianList.
+Require Import bedrock2.anybytes.
 Require Import Rupicola.Lib.Api.
 Require Import Crypto.Algebra.Hierarchy.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
@@ -65,12 +66,13 @@ Definition Placeholder
            {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}
            {field_representation : FieldRepresentation(mem:=mem)}
            (p : word) : mem -> Prop :=
-  Memory.anybytes(mem:=mem) p felem_size_in_bytes.
+  anybytes.anybytes(mem:=mem) p felem_size_in_bytes.
 
 Class FieldRepresentation_ok
       {field_parameters : FieldParameters}
       {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}
       {field_representation : FieldRepresentation} := {
+    size_fits : felem_size_in_bytes <= 2^width;
     relax_bounds :
       forall X : felem, bounded_by tight_bounds X
                         -> bounded_by loose_bounds X;
@@ -92,12 +94,12 @@ Section BignumToFieldRepresentationAdapterLemmas.
     repeat intro.
     cbv [Lift1Prop.ex1]; split; intros;
       repeat match goal with
-             | H : anybytes _ _ _ |- _ => eapply Array.anybytes_to_array_1 in H
+             | H : anybytes _ _ _ |- _ => eapply anybytes_to_array_1 in H
              | H : exists _, _ |- _ => destruct H
              | H : _ /\ _ |- _ => destruct H
              end.
       all : repeat match goal with
-             | H : anybytes _ _ _ |- _ => eapply Array.anybytes_to_array_1 in H
+             | H : anybytes _ _ _ |- _ => eapply anybytes_to_array_1 in H
              | H : exists _, _ |- _ => destruct H
              | H : _ /\ _ |- _ => destruct H
              end.
@@ -106,7 +108,7 @@ Section BignumToFieldRepresentationAdapterLemmas.
     { eapply Bignum_to_bytes in H; sepsimpl.
       let H := match goal with
                | H : Array.array _ _ _ _ _ |- _ => H end in
-      eapply Array.array_1_to_anybytes in H.
+      eapply array_1_to_anybytes in H.
       unshelve (erewrite (_:_*_=_); eassumption).
       rewrite H; destruct Bitwidth.width_cases as [W|W];
         symmetry in W; destruct W; cbn; clear; lia. }
+1 −1		bedrock2
+6 −8		src/Rupicola/Examples/Cells/Cells.v
+0 −119		src/Rupicola/Examples/Nondeterminism/StackAlloc.v
+17 −14		src/Rupicola/Lib/Alloc.v
+2 −16		src/Rupicola/Lib/Core.v
+2 −2		src/Rupicola/Lib/InlineTables.v