search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
123 stars 20 forks source link

Modularize circuit state appearing in types #962

Closed samuelgruetter closed 2 years ago

samuelgruetter commented 2 years ago

If I run About HmacHardware.Hmac.hmac., I get

hmac :
forall {var : tvar},
Circuit
  ((Bit ** Vec (BitVec 32) hmac_register_count) ++
   (((([] ++ [] ++ []) ++ [] ++ []) ++ [] ++ []) ++
    ((([] ++ [] ++ []) ++ [] ++ []) ++ [] ++ []) ++
    ((([] ++ [] ++ []) ++ [] ++ []) ++ [] ++ []) ++
    ([] ++ []) ++
    ([] ++
     [] ++
     [] ++
     [] ++
     [] ++
     (Bit ** Bit ** BitVec 32 ** BitVec 4 ** Bit ** Bit) ++
     ((([] ++ []) ++
       (([] ++ [] ++ []) ++ [] ++ []) ++
       [] ++
       [] ++
       ([] ++ ([] ++ []) ++ []) ++
       (Bit ** BitVec 32 ** BitVec 4 ** BitVec 64 ** BitVec 4) ++
       (([] ++ [] ++ [] ++ [] ++ []) ++
        ([] ++ []) ++
        ([] ++ [] ++ []) ++
        (([] ++ [] ++ []) ++ []) ++
        ((([] ++ []) ++ ([] ++ [] ++ []) ++ []) ++ ([] ++ []) ++ []) ++
        (([] ++
          [] ++
          [] ++
          [] ++
          (([] ++ []) ++
           ((([] ++ []) ++ [] ++ []) ++ []) ++
           ((([] ++ []) ++ [] ++ []) ++ []) ++
           ((([] ++ []) ++ [] ++ []) ++ []) ++
           (([] ++ [] ++ []) ++ []) ++
           ((([] ++ []) ++ [] ++ []) ++ []) ++
           ((([] ++ []) ++ [] ++ []) ++ []) ++
           (([] ++ [] ++ []) ++ []) ++
           ((([] ++ []) ++ [] ++ []) ++ []) ++ (([] ++ [] ++ []) ++ []) ++ [] ++ []) ++
          [] ++
          (([] ++ [] ++ []) ++
           ([] ++ ([] ++ ([] ++ []) ++ []) ++ []) ++
           ([] ++ ([] ++ ([] ++ []) ++ []) ++ []) ++ [] ++ ([] ++ ([] ++ []) ++ []) ++ []) ++
          [] ++ [] ++ [] ++ []) ++ ([] ++ [] ++ []) ++ []) ++
        ([] ++ ([] ++ ([] ++ [] ++ []) ++ []) ++ []) ++ [] ++ [] ++ [] ++ [] ++ []) ++
       [] ++ [] ++ []) ++
      ([] ++
       [] ++
       (([] ++ ([] ++ []) ++ []) ++ ([] ++ []) ++ []) ++
       (Bit ** BitVec 32 ** Vec (BitVec 32) 256 ** BitVec (Nat.log2_up (256 + 1))) ++
       (([] ++ ([] ++ [] ++ []) ++ []) ++
        ([] ++ [] ++ []) ++
        (([] ++ [] ++ []) ++ [] ++ []) ++
        (([] ++ [] ++ []) ++ []) ++ ([] ++ [] ++ []) ++ ([] ++ [] ++ []) ++ []) ++
       [] ++ ([] ++ []) ++ ([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ []) ++
      ([] ++ []) ++
      ([] ++ []) ++ (([] ++ ([] ++ []) ++ []) ++ [] ++ []) ++ [] ++ [] ++ [] ++ [] ++ []) ++
     [] ++ [] ++ [] ++ [] ++ []) ++
    (Bit ** BitVec 32 ** BitVec 4 ** Bit ** Bit ** BitVec 32 ** BitVec 4 ** Bit) ++
    ((([] ++ [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ []) ++
      ([] ++ [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ []) ++
      [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ []) ++
     [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ []) ++
    ([] ++
     [] ++
     [] ++
     [] ++
     [] ++
     [] ++
     [] ++
     [] ++
     (Bit ** Bit ** Bit ** BitVec 6 ** BitVec 5 ** Vec (BitVec 32) 8 ** Bit) ++
     ((([] ++ [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ []) ++ [] ++ [] ++ [] ++ []) ++
      ([] ++ [] ++ [] ++ [] ++ []) ++
      ([] ++ [] ++ []) ++
      ([] ++ [] ++ []) ++
      (([] ++ ([] ++ [] ++ []) ++ [] ++ []) ++
       ([] ++ [] ++ [] ++ []) ++
       ([] ++ ([] ++ [] ++ []) ++ [] ++ []) ++
       ([] ++ [] ++ ([] ++ [] ++ []) ++ []) ++ [] ++ [] ++ [] ++ []) ++
      ([] ++ []) ++
      ([] ++ []) ++
      ([] ++
       [] ++
       [] ++
       [] ++
       [] ++
       (Bit ** sha_block ** sha_digest ** BitVec 6 ** Bit) ++
       (([] ++ [] ++ []) ++
        ([] ++ [] ++ []) ++
        ([] ++ [] ++ []) ++
        ([] ++
         [] ++
         [] ++
         [] ++
         [] ++
         [] ++
         (Bit ** sha_word ** Bit ** BitVec 4 ** BitVec 61 ** BitVec 4) ++
         ([] ++
          ([] ++ [] ++ [] ++ [] ++ [] ++ []) ++
          (([] ++ [] ++ []) ++ ([] ++ []) ++ ([] ++ []) ++ ([] ++ []) ++ []) ++
          (([] ++ ([] ++ []) ++ []) ++ ([] ++ [] ++ []) ++ [] ++ []) ++
          (([] ++
            ([] ++ ([] ++ []) ++ []) ++
            ([] ++ ([] ++ []) ++ []) ++ ([] ++ ([] ++ []) ++ []) ++ []) ++
           [] ++ [] ++ (((([] ++ []) ++ []) ++ []) ++ (([] ++ []) ++ []) ++ []) ++ []) ++
          ((([] ++ [] ++ []) ++ ([] ++ []) ++ []) ++ []) ++
          ([] ++ [] ++ [] ++ []) ++
          (([] ++ []) ++ ([] ++ (([] ++ [] ++ []) ++ ([] ++ [] ++ []) ++ []) ++ []) ++ []) ++
          [] ++ [] ++ [] ++ [] ++ [] ++ []) ++ [] ++ [] ++ []) ++
        ([] ++
         [] ++
         [] ++
         [] ++
         (sha_digest ** sha_block ** Bit ** sha_round) ++
         (([] ++ []) ++
          [] ++
          ([] ++ []) ++
          ([] ++ []) ++
          ([] ++ [] ++ []) ++
          (([] ++
            [] ++
            [] ++
            [] ++
            ((([] ++ ([] ++ []) ++ ([] ++ []) ++ []) ++
              ([] ++ ([] ++ []) ++ ([] ++ []) ++ []) ++ []) ++ ([] ++ []) ++ []) ++
            ((([] ++ ([] ++ []) ++ ([] ++ []) ++ []) ++
              ([] ++ ([] ++ []) ++ ([] ++ []) ++ []) ++ []) ++ ([] ++ []) ++ []) ++
            (([] ++ [] ++ []) ++ [] ++ []) ++ [] ++ []) ++ [] ++ [] ++ []) ++
          (([] ++ [] ++ []) ++ []) ++
          ((([] ++ []) ++ [] ++ []) ++ [] ++ [] ++ []) ++
          (([] ++ [] ++ []) ++ [] ++ []) ++
          (([] ++ [] ++ []) ++ []) ++
          [] ++ ([] ++ [] ++ []) ++ ([] ++ [] ++ [] ++ []) ++ [] ++ [] ++ [] ++ []) ++
         ([] ++ [] ++ []) ++ [] ++ []) ++
        (([] ++ [] ++ []) ++ []) ++
        (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
        ([] ++ [] ++ []) ++
        ([] ++ [] ++ []) ++
        [] ++ [] ++ [] ++ [] ++ [] ++ ([] ++ [] ++ []) ++ ([] ++ [] ++ []) ++ []) ++
       [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ []) ++
      ([] ++ []) ++
      ([] ++ [] ++ []) ++
      (([] ++ []) ++ ([] ++ [] ++ []) ++ []) ++
      (([] ++ []) ++ []) ++ [] ++ [] ++ [] ++ [] ++ [] ++ [] ++ []) ++ 
     [] ++ [] ++ []) ++
    ((([] ++ [] ++ [] ++ []) ++ []) ++
     (([] ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++
      (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++ (([] ++ [] ++ []) ++ [] ++ [] ++ []) ++ []) ++ []) ++
    [] ++ []) ++ [])
  [Bit; BitVec 32; BitVec 5; BitVec 4; Bit; Vec (BitVec 32) hmac_register_count]
  (Vec (BitVec 32) hmac_register_count)

hmac is not universe polymorphic
Arguments hmac {var}
hmac is transparent
Expands to: Constant HmacHardware.Hmac.hmac

That's a mouthful...

So let's try to simplify it:

Goal False.
  let t := type of HmacHardware.Hmac.hmac in let t' := eval cbn in t in idtac t'.

prints

(Circuit
   ((Bit ** Vec (BitVec 32) hmac_register_count) **
    ((Bit ** Bit ** BitVec 32 ** BitVec 4 ** Bit ** Bit) **
     (Bit ** BitVec 32 ** BitVec 4 ** BitVec 64 ** BitVec 4) **
     Bit ** BitVec 32 ** Vec (BitVec 32) 256 ** BitVec 9) **
    (Bit ** BitVec 32 ** BitVec 4 ** Bit ** Bit ** BitVec 32 ** BitVec 4 ** Bit) **
    (Bit ** Bit ** Bit ** BitVec 6 ** BitVec 5 ** Vec (BitVec 32) 8 ** Bit) **
    (Bit ** sha_block ** sha_digest ** BitVec 6 ** Bit) **
    (Bit ** sha_word ** Bit ** BitVec 4 ** BitVec 61 ** BitVec 4) **
    sha_digest ** sha_block ** Bit ** sha_round)
   [Bit; BitVec 32; BitVec 5; BitVec 4; Bit; Vec (BitVec 32) hmac_register_count]
   (Vec (BitVec 32) hmac_register_count))

That still doesn't look modular to me. Can we get hmac to have a type like, eg, the following?

(Circuit
   (state_added_by_tlul ** hmac_outer_state ** hmac_inner_state)
   [Bit; BitVec 32; BitVec 5; BitVec 4; Bit; Vec (BitVec 32) hmac_register_count]
   (Vec (BitVec 32) hmac_register_count))

Not sure how important this is right now, for the moment I'm trying not to worry about it, but just wanted to report this here.