incorporate bytes<->words conversion from fiat-crypto

[andres-erbsen]

@jadephilipoom wrote functions to convert between bytes and words, they are in fiat-crypto branch bedrock2_examples file src/Bedrock/UnsaturatedSolinas.v :).

[samuelgruetter]

@andres-erbsen I'm not quite sure what functions you're referring to, but I have some remarks on some snippets in that file:

    Lemma scalar_to_bytes a x :
      Lift1Prop.iff1
        (array ptsto (word.of_Z 1) a
               (HList.tuple.to_list
                  (LittleEndian.split (Z.to_nat word_size_in_bytes)
                                      (word.unsigned x))))
        (scalar a x).
    Admitted.

If you replace (Z.to_nat word_size_in_bytes) by (bytes_per (width:=width) Syntax.access_size.word), this proof is just reflexivity.

    Lemma scalar_of_bytes
          a l (H : length l = Z.to_nat word_size_in_bytes) :
      Lift1Prop.iff1 (array ptsto (word.of_Z 1) a l)
                     (scalar a (word.of_Z
                                  (LittleEndian.combine
                                     _ (HList.tuple.of_list l)))).
    Admitted. (* TODO *)

I just proved this in this commit.

    Lemma Bignum_to_bytes addr x :
      list_Z_bounded_by max_bounds x ->
      Lift1Prop.iff1
        (array ptsto (word.of_Z 1) addr (encode_bytes (map word.of_Z x)))
        (Bignum addr x).
    Admitted. (* TODO *)

This looks like an anti-pattern to me: Instead of

array ptsto (word.of_Z 1) addr (encode_bytes (map word.of_Z x))

I would use

array (truncated_scalar Syntax.access_size.word) (word.of_Z word_size_in_bytes) addr x

In general, what I've learned from @andres-erbsen is that you should pass to array a specific per-element separation logic predicate corresponding to the type of list elements, rather than first converting the list element to bytes, because these conversions to byte lists will add pain to your proofs.

[andres-erbsen]

Yeah, I think I may have been responsible for some of the bytes conversion confusion there (but note that the conversion will need to happen anyway when allocating new bignums, the question is just where).

[samuelgruetter]

by "allocating new bignums", do you mean calling malloc?

[andres-erbsen]

bumping a pointer (local variable) representing the end of a data stack

[andres-erbsen]

or perhaps eventually the same but done on the actual control stack by the compiler

[samuelgruetter]

Not sure whether it's the same in fiat-crypto, but in the compiler, the only thing I put onto the stack are machine words, so I keep my assertions about the stack as array ptsto_word rather than array of ptsto_byte. But even if you do need some bytes, I'd delay going to bytes as long as possible