diff --git a/hacspec/out/Edhoc_hacspec.fst b/hacspec/out/Edhoc_hacspec.fst
new file mode 100644
index 00000000..495e7271
--- /dev/null
+++ b/hacspec/out/Edhoc_hacspec.fst
@@ -0,0 +1,1129 @@
+module Edhoc_hacspec
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+let edhoc_exporter
+      (state: Edhoc_consts.Hacspec.state_t)
+      (label: Secret_integers.u8_t)
+      (context: Edhoc_consts.Hacspec.bytesMaxContextBuffer_t)
+      (context_len length: uint_size)
+    : Core.Result.result_t (Edhoc_consts.Hacspec.state_t & Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    _x_or_y
+    _c_i
+    _gy_or_gx
+    _prk_3e2m
+    _prk_4e3m
+    _prk_out
+    prk_exporter
+    _h_message_1
+    _th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let output:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  (if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.Completed
+    then
+      let output:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+        edhoc_kdf prk_exporter label context context_len length
+      in
+      Core.Result.Ok (state, output), output
+    else Core.Result.Err Edhoc_consts.Common.WrongState, output)
+    ._1
+
+let r_process_message_1
+      (state: Edhoc_consts.Hacspec.state_t)
+      (message_1: Edhoc_consts.Hacspec.bytesMessage1_t)
+    : Core.Result.result_t Edhoc_consts.Hacspec.state_t Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    _y
+    c_i
+    g_x
+    _prk_3e2m
+    _prk_4e3m
+    _prk_out
+    _prk_exporter
+    h_message_1
+    _th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let current_state, error, h_message_1, state:(Edhoc_consts.Common.eDHOCState_t &
+    Edhoc_consts.Common.eDHOCError_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.state_t) =
+    if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.Start
+    then
+      let method, supported_suites, g_x, c_i:(Secret_integers.u8_t &
+        Edhoc_consts.Hacspec.bytesSupportedSuites_t &
+        Edhoc_consts.Hacspec.bytesP256ElemLen_t &
+        Secret_integers.u8_t) =
+        parse_message_1 message_1
+      in
+      if Secret_integers.declassify method = Edhoc_consts.Common.eDHOC_METHOD
+      then
+        if
+          Secret_integers.declassify supported_suites.[ 0uy ] =
+          Secret_integers.declassify Edhoc_consts.Hacspec.eDHOC_SUPPORTED_SUITES.[ 0uy ]
+        then
+          let h_message_1:Edhoc_consts.Hacspec.bytesHashLen_t =
+            Edhoc_crypto_hacspec.sha256_digest (Edhoc_consts.Hacspec.from_slice message_1
+                  0
+                  (Hacspec_lib_tc.len message_1))
+              (Hacspec_lib_tc.len message_1)
+          in
+          let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+          let current_state:Edhoc_consts.Common.eDHOCState_t =
+            Edhoc_consts.Common.ProcessedMessage1
+          in
+          let state:Edhoc_consts.Hacspec.state_t =
+            construct_state current_state _y c_i g_x _prk_3e2m _prk_4e3m _prk_out _prk_exporter
+              h_message_1 _th_3
+          in
+          current_state, error, h_message_1, state
+        else
+          let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnsupportedCipherSuite in
+          current_state, error, h_message_1, state
+      else
+        let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnsupportedMethod in
+        current_state, error, h_message_1, state
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.WrongState in
+      current_state, error, h_message_1, state
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok state
+  | _ -> Core.Result.Err error
+
+let r_prepare_message_2
+      (state: Edhoc_consts.Hacspec.state_t)
+      (id_cred_r: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (cred_r: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_r_len: uint_size)
+      (r y g_y: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+    : Core.Result.result_t
+      (Edhoc_consts.Hacspec.state_t & Edhoc_consts.Hacspec.bytesMessage2_t & Secret_integers.u8_t)
+      Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    _y
+    _c_i
+    g_x
+    prk_3e2m
+    _prk_4e3m
+    _prk_out
+    _prk_exporter
+    h_message_1
+    th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let message_2:Edhoc_consts.Hacspec.bytesMessage2_t = Edhoc_consts.Hacspec.new_ in
+  let c_r:Secret_integers.u8_t = Hacspec_lib_tc.secret 255uy in
+  let c_r, current_state, error, message_2, prk_3e2m, state, th_3:(Secret_integers.u8_t &
+    Edhoc_consts.Common.eDHOCState_t &
+    Edhoc_consts.Common.eDHOCError_t &
+    Edhoc_consts.Hacspec.bytesMessage2_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.state_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t) =
+    if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.ProcessedMessage1
+    then
+      let c_r:Secret_integers.u8_t = Edhoc_consts.Hacspec.c_R in
+      let th_2:Edhoc_consts.Hacspec.bytesHashLen_t = compute_th_2 g_y c_r h_message_1 in
+      let prk_2e:Edhoc_consts.Hacspec.bytesHashLen_t = compute_prk_2e y g_x th_2 in
+      let salt_3e2m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_salt_3e2m prk_2e th_2 in
+      let prk_3e2m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_prk_3e2m salt_3e2m r g_x in
+      let mac_2:Edhoc_consts.Hacspec.bytesMac2_t =
+        compute_mac_2 prk_3e2m id_cred_r cred_r cred_r_len th_2
+      in
+      let plaintext_2:Edhoc_consts.Hacspec.bytesPlaintext2_t =
+        encode_plaintext_2 id_cred_r mac_2 Edhoc_consts.Hacspec.new_
+      in
+      let th_3:Edhoc_consts.Hacspec.bytesHashLen_t =
+        compute_th_3 th_2 plaintext_2 cred_r cred_r_len
+      in
+      let ciphertext_2, ciphertext_2_len:(Edhoc_consts.Hacspec.bytesMaxBuffer_t & uint_size) =
+        encrypt_decrypt_ciphertext_2 prk_2e
+          th_2
+          (Edhoc_consts.Hacspec.from_slice plaintext_2 0 (Hacspec_lib_tc.len plaintext_2))
+      in
+      let message_2:Edhoc_consts.Hacspec.bytesMessage2_t =
+        encode_message_2 g_y (Edhoc_consts.Hacspec.from_slice ciphertext_2 0 ciphertext_2_len) c_r
+      in
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+      let current_state:Edhoc_consts.Common.eDHOCState_t = Edhoc_consts.Common.WaitMessage3 in
+      let state:Edhoc_consts.Hacspec.state_t =
+        construct_state current_state y _c_i g_x prk_3e2m _prk_4e3m _prk_out _prk_exporter
+          h_message_1 th_3
+      in
+      c_r, current_state, error, message_2, prk_3e2m, state, th_3
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.WrongState in
+      c_r, current_state, error, message_2, prk_3e2m, state, th_3
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok (state, message_2, c_r)
+  | _ -> Core.Result.Err error
+
+let r_process_message_3
+      (state: Edhoc_consts.Hacspec.state_t)
+      (message_3: Edhoc_consts.Hacspec.bytesMessage3_t)
+      (id_cred_i_expected: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (cred_i_expected: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_i_len: uint_size)
+      (g_i: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+    : Core.Result.result_t (Edhoc_consts.Hacspec.state_t & Edhoc_consts.Hacspec.bytesHashLen_t)
+      Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    y
+    _c_i
+    _g_x
+    prk_3e2m
+    prk_4e3m
+    prk_out
+    prk_exporter
+    _h_message_1
+    th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let current_state, error, prk_4e3m, prk_exporter, prk_out, state:(Edhoc_consts.Common.eDHOCState_t &
+    Edhoc_consts.Common.eDHOCError_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.state_t) =
+    if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.WaitMessage3
+    then
+      let plaintext_3:Core.Result.result_t Edhoc_consts.Hacspec.bytesPlaintext3_t
+        Edhoc_consts.Common.eDHOCError_t =
+        decrypt_message_3 prk_3e2m th_3 message_3
+      in
+      if Core.Result.is_ok plaintext_3
+      then
+        let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t = Core.Result.unwrap plaintext_3 in
+        let kid, mac_3:(Secret_integers.u8_t & Edhoc_consts.Hacspec.bytesMac3_t) =
+          decode_plaintext_3 plaintext_3
+        in
+        if
+          Secret_integers.declassify kid =
+          Secret_integers.declassify id_cred_i_expected.[ Hacspec_lib_tc.len id_cred_i_expected - 1
+            ]
+        then
+          let salt_4e3m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_salt_4e3m prk_3e2m th_3 in
+          let prk_4e3m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_prk_4e3m salt_4e3m y g_i in
+          let expected_mac_3:Edhoc_consts.Hacspec.bytesMac3_t =
+            compute_mac_3 prk_4e3m th_3 id_cred_i_expected cred_i_expected cred_i_len
+          in
+          let current_state, error, prk_exporter, prk_out, state:(Edhoc_consts.Common.eDHOCState_t &
+            Edhoc_consts.Common.eDHOCError_t &
+            Edhoc_consts.Hacspec.bytesHashLen_t &
+            Edhoc_consts.Hacspec.bytesHashLen_t &
+            Edhoc_consts.Hacspec.state_t) =
+            if Edhoc_consts.Hacspec.declassify_eq mac_3 expected_mac_3
+            then
+              let current_state, error, prk_4e3m, prk_exporter, prk_out, state:(Edhoc_consts.Common.eDHOCState_t &
+                Edhoc_consts.Common.eDHOCError_t &
+                Edhoc_consts.Hacspec.bytesHashLen_t &
+                Edhoc_consts.Hacspec.bytesHashLen_t &
+                Edhoc_consts.Hacspec.bytesHashLen_t &
+                Edhoc_consts.Hacspec.state_t) =
+                let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+                let th_4:Edhoc_consts.Hacspec.bytesHashLen_t =
+                  compute_th_4 th_3 plaintext_3 cred_i_expected cred_i_len
+                in
+                let prk_out_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+                  edhoc_kdf prk_4e3m
+                    (Hacspec_lib_tc.secret 7uy)
+                    (Edhoc_consts.Hacspec.from_slice th_4 0 (Hacspec_lib_tc.len th_4))
+                    (Hacspec_lib_tc.len th_4)
+                    Edhoc_consts.Common.sHA256_DIGEST_LEN
+                in
+                let prk_out:Edhoc_consts.Hacspec.bytesHashLen_t =
+                  Hacspec_lib_tc.update_slice prk_out
+                    0
+                    prk_out_buf
+                    0
+                    Edhoc_consts.Common.sHA256_DIGEST_LEN
+                in
+                let prk_exporter_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+                  edhoc_kdf prk_out
+                    (Hacspec_lib_tc.secret 10uy)
+                    Edhoc_consts.Hacspec.new_
+                    0
+                    Edhoc_consts.Common.sHA256_DIGEST_LEN
+                in
+                let prk_exporter:Edhoc_consts.Hacspec.bytesHashLen_t =
+                  Hacspec_lib_tc.update_slice prk_exporter
+                    0
+                    prk_exporter_buf
+                    0
+                    Edhoc_consts.Common.sHA256_DIGEST_LEN
+                in
+                let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+                let current_state:Edhoc_consts.Common.eDHOCState_t =
+                  Edhoc_consts.Common.Completed
+                in
+                let state:Edhoc_consts.Hacspec.state_t =
+                  construct_state current_state y _c_i _g_x prk_3e2m prk_4e3m prk_out prk_exporter
+                    _h_message_1 th_3
+                in
+                current_state, error, prk_4e3m, prk_exporter, prk_out, state
+              in
+              current_state, error, prk_exporter, prk_out, state
+            else
+              let current_state, error, prk_4e3m, prk_exporter, prk_out, state:(Edhoc_consts.Common.eDHOCState_t &
+                Edhoc_consts.Common.eDHOCError_t &
+                Edhoc_consts.Hacspec.bytesHashLen_t &
+                Edhoc_consts.Hacspec.bytesHashLen_t &
+                Edhoc_consts.Hacspec.bytesHashLen_t &
+                Edhoc_consts.Hacspec.state_t) =
+                let error:Edhoc_consts.Common.eDHOCError_t =
+                  Edhoc_consts.Common.MacVerificationFailed
+                in
+                current_state, error, prk_4e3m, prk_exporter, prk_out, state
+              in
+              current_state, error, prk_exporter, prk_out, state
+          in
+          current_state, error, prk_4e3m, prk_exporter, prk_out, state
+        else
+          let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownPeer in
+          current_state, error, prk_4e3m, prk_exporter, prk_out, state
+      else
+        let error:Edhoc_consts.Common.eDHOCError_t =
+          Core.Option.expect (Core.Result.err plaintext_3) "error handling error"
+        in
+        current_state, error, prk_4e3m, prk_exporter, prk_out, state
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.WrongState in
+      current_state, error, prk_4e3m, prk_exporter, prk_out, state
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok (state, prk_out)
+  | _ -> Core.Result.Err error
+
+let i_prepare_message_1
+      (state: Edhoc_consts.Hacspec.state_t)
+      (x g_x: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+    : Core.Result.result_t (Edhoc_consts.Hacspec.state_t & Edhoc_consts.Hacspec.bytesMessage1_t)
+      Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    _x
+    c_i
+    _g_y
+    _prk_3e2m
+    _prk_4e3m
+    _prk_out
+    _prk_exporter
+    h_message_1
+    _th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let message_1:Edhoc_consts.Hacspec.bytesMessage1_t = Edhoc_consts.Hacspec.new_ in
+  let c_i, current_state, error, h_message_1, message_1, state:(Secret_integers.u8_t &
+    Edhoc_consts.Common.eDHOCState_t &
+    Edhoc_consts.Common.eDHOCError_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.bytesMessage1_t &
+    Edhoc_consts.Hacspec.state_t) =
+    if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.Start
+    then
+      let selected_suites:Edhoc_consts.Hacspec.bytesSupportedSuites_t =
+        Edhoc_consts.Hacspec.eDHOC_SUPPORTED_SUITES
+      in
+      let c_i:Secret_integers.u8_t = Edhoc_consts.Hacspec.c_I in
+      let message_1:Edhoc_consts.Hacspec.bytesMessage1_t =
+        encode_message_1 (Hacspec_lib_tc.secret Edhoc_consts.Common.eDHOC_METHOD)
+          selected_suites
+          g_x
+          c_i
+      in
+      let h_message_1:Edhoc_consts.Hacspec.bytesHashLen_t =
+        Edhoc_crypto_hacspec.sha256_digest (Edhoc_consts.Hacspec.from_slice message_1
+              0
+              (Hacspec_lib_tc.len message_1))
+          (Hacspec_lib_tc.len message_1)
+      in
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+      let current_state:Edhoc_consts.Common.eDHOCState_t = Edhoc_consts.Common.WaitMessage2 in
+      let state:Edhoc_consts.Hacspec.state_t =
+        construct_state current_state x c_i _g_y _prk_3e2m _prk_4e3m _prk_out _prk_exporter
+          h_message_1 _th_3
+      in
+      c_i, current_state, error, h_message_1, message_1, state
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.WrongState in
+      c_i, current_state, error, h_message_1, message_1, state
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok (state, message_1)
+  | _ -> Core.Result.Err error
+
+let i_process_message_2
+      (state: Edhoc_consts.Hacspec.state_t)
+      (message_2: Edhoc_consts.Hacspec.bytesMessage2_t)
+      (id_cred_r_expected: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (cred_r_expected: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_r_len: uint_size)
+      (g_r i: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+    : Core.Result.result_t
+      (Edhoc_consts.Hacspec.state_t & Secret_integers.u8_t & Secret_integers.u8_t)
+      Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    x
+    _c_i
+    g_y
+    prk_3e2m
+    prk_4e3m
+    _prk_out
+    _prk_exporter
+    h_message_1
+    th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let c_r:Secret_integers.u8_t = Hacspec_lib_tc.secret 255uy in
+  let kid:Secret_integers.u8_t = Hacspec_lib_tc.secret 255uy in
+  let c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3:(Secret_integers.u8_t &
+    Edhoc_consts.Common.eDHOCState_t &
+    Edhoc_consts.Common.eDHOCError_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.state_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t) =
+    if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.WaitMessage2
+    then
+      let g_y, ciphertext_2, c_r_2:(Edhoc_consts.Hacspec.bytesP256ElemLen_t &
+        Edhoc_consts.Hacspec.bytesCiphertext2_t &
+        Secret_integers.u8_t) =
+        parse_message_2 message_2
+      in
+      let c_r:Secret_integers.u8_t = c_r_2 in
+      let th_2:Edhoc_consts.Hacspec.bytesHashLen_t = compute_th_2 g_y c_r h_message_1 in
+      let prk_2e:Edhoc_consts.Hacspec.bytesHashLen_t = compute_prk_2e x g_y th_2 in
+      let plaintext_2, plaintext_2_len:(Edhoc_consts.Hacspec.bytesMaxBuffer_t & uint_size) =
+        encrypt_decrypt_ciphertext_2 prk_2e th_2 ciphertext_2
+      in
+      let kid, mac_2, _ead_2:(Secret_integers.u8_t & Edhoc_consts.Hacspec.bytesMac2_t &
+        Edhoc_consts.Hacspec.bytesEad2_t) =
+        decode_plaintext_2 plaintext_2 plaintext_2_len
+      in
+      let salt_3e2m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_salt_3e2m prk_2e th_2 in
+      let prk_3e2m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_prk_3e2m salt_3e2m x g_r in
+      let expected_mac_2:Edhoc_consts.Hacspec.bytesMac2_t =
+        compute_mac_2 prk_3e2m id_cred_r_expected cred_r_expected cred_r_len th_2
+      in
+      let current_state, error, prk_4e3m, state, th_3:(Edhoc_consts.Common.eDHOCState_t &
+        Edhoc_consts.Common.eDHOCError_t &
+        Edhoc_consts.Hacspec.bytesHashLen_t &
+        Edhoc_consts.Hacspec.state_t &
+        Edhoc_consts.Hacspec.bytesHashLen_t) =
+        if Edhoc_consts.Hacspec.declassify_eq mac_2 expected_mac_2
+        then
+          if
+            Secret_integers.declassify kid =
+            Secret_integers.declassify id_cred_r_expected.[ Hacspec_lib_tc.len id_cred_r_expected -
+                1 ]
+          then
+            let c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3:(Secret_integers.u8_t &
+              Edhoc_consts.Common.eDHOCState_t &
+              Edhoc_consts.Common.eDHOCError_t &
+              Edhoc_consts.Hacspec.bytesHashLen_t &
+              Edhoc_consts.Hacspec.bytesHashLen_t &
+              Edhoc_consts.Hacspec.state_t &
+              Edhoc_consts.Hacspec.bytesHashLen_t) =
+              let th_3:Edhoc_consts.Hacspec.bytesHashLen_t =
+                compute_th_3 th_2
+                  (Edhoc_consts.Hacspec.from_slice plaintext_2 0 plaintext_2_len)
+                  cred_r_expected
+                  cred_r_len
+              in
+              let salt_4e3m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_salt_4e3m prk_3e2m th_3 in
+              let prk_4e3m:Edhoc_consts.Hacspec.bytesHashLen_t = compute_prk_4e3m salt_4e3m i g_y in
+              let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+              let current_state:Edhoc_consts.Common.eDHOCState_t =
+                Edhoc_consts.Common.ProcessedMessage2
+              in
+              let state:Edhoc_consts.Hacspec.state_t =
+                construct_state current_state x _c_i g_y prk_3e2m prk_4e3m _prk_out _prk_exporter
+                  h_message_1 th_3
+              in
+              c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3
+            in
+            current_state, error, prk_4e3m, state, th_3
+          else
+            let c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3:(Secret_integers.u8_t &
+              Edhoc_consts.Common.eDHOCState_t &
+              Edhoc_consts.Common.eDHOCError_t &
+              Edhoc_consts.Hacspec.bytesHashLen_t &
+              Edhoc_consts.Hacspec.bytesHashLen_t &
+              Edhoc_consts.Hacspec.state_t &
+              Edhoc_consts.Hacspec.bytesHashLen_t) =
+              let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownPeer in
+              c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3
+            in
+            current_state, error, prk_4e3m, state, th_3
+        else
+          let c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3:(Secret_integers.u8_t &
+            Edhoc_consts.Common.eDHOCState_t &
+            Edhoc_consts.Common.eDHOCError_t &
+            Edhoc_consts.Hacspec.bytesHashLen_t &
+            Edhoc_consts.Hacspec.bytesHashLen_t &
+            Edhoc_consts.Hacspec.state_t &
+            Edhoc_consts.Hacspec.bytesHashLen_t) =
+            let error:Edhoc_consts.Common.eDHOCError_t =
+              Edhoc_consts.Common.MacVerificationFailed
+            in
+            c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3
+          in
+          current_state, error, prk_4e3m, state, th_3
+      in
+      c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.WrongState in
+      c_r, current_state, error, prk_3e2m, prk_4e3m, state, th_3
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok (state, c_r, kid)
+  | _ -> Core.Result.Err error
+
+let i_prepare_message_3
+      (state: Edhoc_consts.Hacspec.state_t)
+      (id_cred_i: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (cred_i: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_i_len: uint_size)
+    : Core.Result.result_t
+      (Edhoc_consts.Hacspec.state_t & Edhoc_consts.Hacspec.bytesMessage3_t &
+        Edhoc_consts.Hacspec.bytesHashLen_t) Edhoc_consts.Common.eDHOCError_t =
+  let
+  Edhoc_consts.Hacspec.State
+    current_state
+    _x
+    _c_i
+    _g_y
+    prk_3e2m
+    prk_4e3m
+    prk_out
+    prk_exporter
+    _h_message_1
+    th_3:Edhoc_consts.Hacspec.state_t =
+    state
+  in
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let message_3:Edhoc_consts.Hacspec.bytesMessage3_t = Edhoc_consts.Hacspec.new_ in
+  let current_state, error, message_3, prk_exporter, prk_out, state:(Edhoc_consts.Common.eDHOCState_t &
+    Edhoc_consts.Common.eDHOCError_t &
+    Edhoc_consts.Hacspec.bytesMessage3_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.bytesHashLen_t &
+    Edhoc_consts.Hacspec.state_t) =
+    if Core.Cmp.PartialEq.eq current_state Edhoc_consts.Common.ProcessedMessage2
+    then
+      let mac_3:Edhoc_consts.Hacspec.bytesMac3_t =
+        compute_mac_3 prk_4e3m th_3 id_cred_i cred_i cred_i_len
+      in
+      let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t = encode_plaintext_3 id_cred_i mac_3 in
+      let message_3:Edhoc_consts.Hacspec.bytesMessage3_t =
+        encrypt_message_3 prk_3e2m th_3 plaintext_3
+      in
+      let th_4:Edhoc_consts.Hacspec.bytesHashLen_t =
+        compute_th_4 th_3 plaintext_3 cred_i cred_i_len
+      in
+      let prk_out_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+        edhoc_kdf prk_4e3m
+          (Hacspec_lib_tc.secret 7uy)
+          (Edhoc_consts.Hacspec.from_slice th_4 0 (Hacspec_lib_tc.len th_4))
+          (Hacspec_lib_tc.len th_4)
+          Edhoc_consts.Common.sHA256_DIGEST_LEN
+      in
+      let prk_out:Edhoc_consts.Hacspec.bytesHashLen_t =
+        Hacspec_lib_tc.update_slice prk_out 0 prk_out_buf 0 Edhoc_consts.Common.sHA256_DIGEST_LEN
+      in
+      let prk_exporter_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+        edhoc_kdf prk_out
+          (Hacspec_lib_tc.secret 10uy)
+          Edhoc_consts.Hacspec.new_
+          0
+          Edhoc_consts.Common.sHA256_DIGEST_LEN
+      in
+      let prk_exporter:Edhoc_consts.Hacspec.bytesHashLen_t =
+        Hacspec_lib_tc.update_slice prk_exporter
+          0
+          prk_exporter_buf
+          0
+          Edhoc_consts.Common.sHA256_DIGEST_LEN
+      in
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+      let current_state:Edhoc_consts.Common.eDHOCState_t = Edhoc_consts.Common.Completed in
+      let state:Edhoc_consts.Hacspec.state_t =
+        construct_state current_state _x _c_i _g_y prk_3e2m prk_4e3m prk_out prk_exporter
+          _h_message_1 th_3
+      in
+      current_state, error, message_3, prk_exporter, prk_out, state
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.WrongState in
+      current_state, error, message_3, prk_exporter, prk_out, state
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok (state, message_3, prk_out)
+  | _ -> Core.Result.Err error
+
+let construct_state
+      (state: Edhoc_consts.Common.eDHOCState_t)
+      (x_or_y: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+      (c_i: Secret_integers.u8_t)
+      (gx_or_gy: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+      (prk_3e2m prk_4e3m prk_out prk_exporter h_message_1 th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.state_t =
+  Edhoc_consts.Hacspec.State state
+    x_or_y
+    c_i
+    gx_or_gy
+    prk_3e2m
+    prk_4e3m
+    prk_out
+    prk_exporter
+    h_message_1
+    th_3
+
+let parse_message_1 (rcvd_message_1: Edhoc_consts.Hacspec.bytesMessage1_t)
+    : (Secret_integers.u8_t & Edhoc_consts.Hacspec.bytesSupportedSuites_t &
+      Edhoc_consts.Hacspec.bytesP256ElemLen_t &
+      Secret_integers.u8_t) =
+  let method:Secret_integers.u8_t = rcvd_message_1.[ 0l ] in
+  let selected_suite:Edhoc_consts.Hacspec.bytesSupportedSuites_t =
+    Edhoc_consts.Hacspec.from_slice rcvd_message_1 1 1
+  in
+  let g_x:Edhoc_consts.Hacspec.bytesP256ElemLen_t =
+    Edhoc_consts.Hacspec.from_slice rcvd_message_1 4 Edhoc_consts.Common.p256_ELEM_LEN
+  in
+  let c_i:Secret_integers.u8_t = rcvd_message_1.[ Edhoc_consts.Common.mESSAGE_1_LEN - 1 ] in
+  method, selected_suite, g_x, c_i
+
+let encode_message_1
+      (method: Secret_integers.u8_t)
+      (suites: Edhoc_consts.Hacspec.bytesSupportedSuites_t)
+      (g_x: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+      (c_i: Secret_integers.u8_t)
+    : Edhoc_consts.Hacspec.bytesMessage1_t =
+  let output:Edhoc_consts.Hacspec.bytesMessage1_t = Edhoc_consts.Hacspec.new_ in
+  let output:Edhoc_consts.Hacspec.bytesMessage1_t = output.[ 0l ] <- method in
+  let output:Edhoc_consts.Hacspec.bytesMessage1_t = output.[ 1l ] <- suites.[ 0l ] in
+  let output:Edhoc_consts.Hacspec.bytesMessage1_t =
+    output.[ 2l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let output:Edhoc_consts.Hacspec.bytesMessage1_t =
+    output.[ 3l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.p256_ELEM_LEN
+  in
+  let output:Edhoc_consts.Hacspec.bytesMessage1_t = Hacspec_lib_tc.update output 4 g_x in
+  output.[ 4 + Edhoc_consts.Common.p256_ELEM_LEN ] <- c_i
+
+let parse_message_2 (rcvd_message_2: Edhoc_consts.Hacspec.bytesMessage2_t)
+    : (Edhoc_consts.Hacspec.bytesP256ElemLen_t & Edhoc_consts.Hacspec.bytesCiphertext2_t &
+      Secret_integers.u8_t) =
+  let g_y:Edhoc_consts.Hacspec.bytesP256ElemLen_t =
+    Edhoc_consts.Hacspec.from_slice rcvd_message_2 2 Edhoc_consts.Common.p256_ELEM_LEN
+  in
+  let ciphertext_2:Edhoc_consts.Hacspec.bytesCiphertext2_t =
+    Edhoc_consts.Hacspec.from_slice rcvd_message_2
+      (2 + Edhoc_consts.Common.p256_ELEM_LEN)
+      Edhoc_consts.Common.cIPHERTEXT_2_LEN
+  in
+  let c_r:Secret_integers.u8_t = rcvd_message_2.[ Edhoc_consts.Common.mESSAGE_2_LEN - 1 ] in
+  g_y, ciphertext_2, c_r
+
+let encode_message_2
+      (g_y: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+      (ciphertext_2: Edhoc_consts.Hacspec.bytesCiphertext2_t)
+      (c_r: Secret_integers.u8_t)
+    : Edhoc_consts.Hacspec.bytesMessage2_t =
+  let output:Edhoc_consts.Hacspec.bytesMessage2_t = Edhoc_consts.Hacspec.new_ in
+  let output:Edhoc_consts.Hacspec.bytesMessage2_t =
+    output.[ 0l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let output:Edhoc_consts.Hacspec.bytesMessage2_t =
+    output.[ 1l ] <-
+      Hacspec_lib_tc.secret
+      (Edhoc_consts.Common.p256_ELEM_LEN + Edhoc_consts.Common.cIPHERTEXT_2_LEN)
+  in
+  let output:Edhoc_consts.Hacspec.bytesMessage2_t = Hacspec_lib_tc.update output 2 g_y in
+  let output:Edhoc_consts.Hacspec.bytesMessage2_t =
+    Hacspec_lib_tc.update output (2 + Edhoc_consts.Common.p256_ELEM_LEN) ciphertext_2
+  in
+  output.[ 2 + Edhoc_consts.Common.p256_ELEM_LEN + Edhoc_consts.Common.cIPHERTEXT_2_LEN ] <- c_r
+
+let compute_th_2
+      (g_y: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+      (c_r: Secret_integers.u8_t)
+      (h_message_1: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 0l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 1l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.p256_ELEM_LEN
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Hacspec_lib_tc.update message 2 g_y in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 2 + Edhoc_consts.Common.p256_ELEM_LEN ] <- c_r
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 3 + Edhoc_consts.Common.p256_ELEM_LEN ] <-
+      Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 4 + Edhoc_consts.Common.p256_ELEM_LEN ] <-
+      Hacspec_lib_tc.secret Edhoc_consts.Common.sHA256_DIGEST_LEN
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    Hacspec_lib_tc.update message (5 + Edhoc_consts.Common.p256_ELEM_LEN) h_message_1
+  in
+  let len:uint_size =
+    5 + Edhoc_consts.Common.p256_ELEM_LEN + Edhoc_consts.Common.sHA256_DIGEST_LEN
+  in
+  Edhoc_crypto_hacspec.sha256_digest message len
+
+let compute_th_3
+      (th_2: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (plaintext_2: Edhoc_consts.Hacspec.bytesPlaintext2_t)
+      (cred_r: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_r_len: uint_size)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 0l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 1l ] <- Hacspec_lib_tc.secret (Hacspec_lib_tc.len th_2)
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Hacspec_lib_tc.update message 2 th_2 in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    Hacspec_lib_tc.update message (2 + Hacspec_lib_tc.len th_2) plaintext_2
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    Hacspec_lib_tc.update_slice message
+      (2 + Hacspec_lib_tc.len th_2 + Hacspec_lib_tc.len plaintext_2)
+      cred_r
+      0
+      cred_r_len
+  in
+  Edhoc_crypto_hacspec.sha256_digest message
+    (Hacspec_lib_tc.len th_2 + 2 + Hacspec_lib_tc.len plaintext_2 + cred_r_len)
+
+let compute_th_4
+      (th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (plaintext_3: Edhoc_consts.Hacspec.bytesPlaintext3_t)
+      (cred_i: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_i_len: uint_size)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 0l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    message.[ 1l ] <- Hacspec_lib_tc.secret (Hacspec_lib_tc.len th_3)
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Hacspec_lib_tc.update message 2 th_3 in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    Hacspec_lib_tc.update message (2 + Hacspec_lib_tc.len th_3) plaintext_3
+  in
+  let message:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    Hacspec_lib_tc.update_slice message
+      (2 + Hacspec_lib_tc.len th_3 + Hacspec_lib_tc.len plaintext_3)
+      cred_i
+      0
+      cred_i_len
+  in
+  Edhoc_crypto_hacspec.sha256_digest message
+    (Hacspec_lib_tc.len th_3 + 2 + Hacspec_lib_tc.len plaintext_3 + cred_i_len)
+
+let edhoc_kdf
+      (prk: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (label: Secret_integers.u8_t)
+      (context: Edhoc_consts.Hacspec.bytesMaxContextBuffer_t)
+      (context_len length: uint_size)
+    : Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+  let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let info_len:uint_size = 0 in
+  let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t = info.[ 0l ] <- label in
+  let info, info_len:(Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t & uint_size) =
+    if Prims.op_LessThan context_len 24
+    then
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        info.[ 1l ] <-
+          Hacspec_lib_tc.secret
+          (Hacspec_lib.|. context_len Edhoc_consts.Common.cBOR_MAJOR_BYTE_STRING)
+      in
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        Hacspec_lib_tc.update_slice info 2 context 0 context_len
+      in
+      let info_len:uint_size = 2 + context_len in
+      info, info_len
+    else
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        info.[ 1l ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+      in
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        info.[ 2l ] <- Hacspec_lib_tc.secret context_len
+      in
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        Hacspec_lib_tc.update_slice info 3 context 0 context_len
+      in
+      let info_len:uint_size = 3 + context_len in
+      info, info_len
+  in
+  let info, info_len:(Secret_integers.u8_t & uint_size) =
+    if Prims.op_LessThan length 24
+    then
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        info.[ info_len ] <- Hacspec_lib_tc.secret length
+      in
+      let info_len:uint_size = info_len + 1 in
+      info, info_len
+    else
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        info.[ info_len ] <- Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_UINT_1BYTE
+      in
+      let info:Edhoc_consts.Hacspec.bytesMaxInfoBuffer_t =
+        info.[ info_len + 1 ] <- Hacspec_lib_tc.secret length
+      in
+      let info_len:uint_size = info_len + 2 in
+      info, info_len
+  in
+  Edhoc_crypto_hacspec.hkdf_expand prk info info_len length
+
+let decode_plaintext_3 (plaintext_3: Edhoc_consts.Hacspec.bytesPlaintext3_t)
+    : (Secret_integers.u8_t & Edhoc_consts.Hacspec.bytesMac3_t) =
+  let kid:Secret_integers.u8_t = plaintext_3.[ 0 ] in
+  let mac_3:Edhoc_consts.Hacspec.bytesMac3_t =
+    Edhoc_consts.Hacspec.from_slice plaintext_3 2 Edhoc_consts.Common.mAC_LENGTH_3
+  in
+  kid, mac_3
+
+let encode_plaintext_3
+      (id_cred_i: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (mac_3: Edhoc_consts.Hacspec.bytesMac3_t)
+    : Edhoc_consts.Hacspec.bytesPlaintext3_t =
+  let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t = Edhoc_consts.Hacspec.new_ in
+  let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t =
+    plaintext_3.[ 0l ] <- id_cred_i.[ Hacspec_lib_tc.len id_cred_i - 1 ]
+  in
+  let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t =
+    plaintext_3.[ 1l ] <-
+      Hacspec_lib_tc.secret
+      (Hacspec_lib.|. Edhoc_consts.Common.cBOR_MAJOR_BYTE_STRING Edhoc_consts.Common.mAC_LENGTH_3)
+  in
+  Hacspec_lib_tc.update plaintext_3 2 mac_3
+
+let encode_enc_structure (th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = Edhoc_consts.Hacspec.new_ in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 0l ] <- Hacspec_lib_tc.secret 69uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 1l ] <- Hacspec_lib_tc.secret 110uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 2l ] <- Hacspec_lib_tc.secret 99uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 3l ] <- Hacspec_lib_tc.secret 114uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 4l ] <- Hacspec_lib_tc.secret 121uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 5l ] <- Hacspec_lib_tc.secret 112uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 6l ] <- Hacspec_lib_tc.secret 116uy in
+  let encrypt0:Edhoc_consts.Hacspec.bytes8_t = encrypt0.[ 7l ] <- Hacspec_lib_tc.secret 48uy in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t = Edhoc_consts.Hacspec.new_ in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+    enc_structure.[ 0l ] <-
+      Hacspec_lib_tc.secret (Hacspec_lib.|. Edhoc_consts.Common.cBOR_MAJOR_ARRAY 3uy)
+  in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+    enc_structure.[ 1l ] <-
+      Hacspec_lib_tc.secret
+      (Hacspec_lib.|. Edhoc_consts.Common.cBOR_MAJOR_TEXT_STRING (Hacspec_lib_tc.len encrypt0))
+  in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+    Hacspec_lib_tc.update enc_structure 2 encrypt0
+  in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+    enc_structure.[ Hacspec_lib_tc.len encrypt0 + 2 ] <-
+      Hacspec_lib_tc.secret (Hacspec_lib.|. Edhoc_consts.Common.cBOR_MAJOR_BYTE_STRING 0uy)
+  in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+    enc_structure.[ Hacspec_lib_tc.len encrypt0 + 3 ] <-
+      Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t =
+    enc_structure.[ Hacspec_lib_tc.len encrypt0 + 4 ] <-
+      Hacspec_lib_tc.secret Edhoc_consts.Common.sHA256_DIGEST_LEN
+  in
+  Hacspec_lib_tc.update enc_structure (Hacspec_lib_tc.len encrypt0 + 5) th_3
+
+let compute_k_3_iv_3 (prk_3e2m th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : (Edhoc_consts.Hacspec.bytesCcmKeyLen_t & Edhoc_consts.Hacspec.bytesCcmIvLen_t) =
+  let k_3:Edhoc_consts.Hacspec.bytesCcmKeyLen_t =
+    Edhoc_consts.Hacspec.from_slice (edhoc_kdf prk_3e2m
+          (Hacspec_lib_tc.secret 3uy)
+          (Edhoc_consts.Hacspec.from_slice th_3 0 (Hacspec_lib_tc.len th_3))
+          (Hacspec_lib_tc.len th_3)
+          Edhoc_consts.Common.aES_CCM_KEY_LEN)
+      0
+      Edhoc_consts.Common.aES_CCM_KEY_LEN
+  in
+  let iv_3:Edhoc_consts.Hacspec.bytesCcmIvLen_t =
+    Edhoc_consts.Hacspec.from_slice (edhoc_kdf prk_3e2m
+          (Hacspec_lib_tc.secret 4uy)
+          (Edhoc_consts.Hacspec.from_slice th_3 0 (Hacspec_lib_tc.len th_3))
+          (Hacspec_lib_tc.len th_3)
+          Edhoc_consts.Common.aES_CCM_IV_LEN)
+      0
+      Edhoc_consts.Common.aES_CCM_IV_LEN
+  in
+  k_3, iv_3
+
+let encrypt_message_3
+      (prk_3e2m th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (plaintext_3: Edhoc_consts.Hacspec.bytesPlaintext3_t)
+    : Edhoc_consts.Hacspec.bytesMessage3_t =
+  let output:Edhoc_consts.Hacspec.bytesMessage3_t = Edhoc_consts.Hacspec.new_ in
+  let output:Edhoc_consts.Hacspec.bytesMessage3_t =
+    output.[ 0l ] <-
+      Hacspec_lib_tc.secret
+      (Hacspec_lib.|. Edhoc_consts.Common.cBOR_MAJOR_BYTE_STRING
+          Edhoc_consts.Common.cIPHERTEXT_3_LEN)
+  in
+  let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t = encode_enc_structure th_3 in
+  let k_3, iv_3:(Edhoc_consts.Hacspec.bytesCcmKeyLen_t & Edhoc_consts.Hacspec.bytesCcmIvLen_t) =
+    compute_k_3_iv_3 prk_3e2m th_3
+  in
+  Hacspec_lib_tc.update output
+    1
+    (Edhoc_crypto_hacspec.aes_ccm_encrypt_tag_8 k_3 iv_3 enc_structure plaintext_3)
+
+let decrypt_message_3
+      (prk_3e2m th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (message_3: Edhoc_consts.Hacspec.bytesMessage3_t)
+    : Core.Result.result_t Edhoc_consts.Hacspec.bytesPlaintext3_t Edhoc_consts.Common.eDHOCError_t =
+  let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.UnknownError in
+  let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t = Edhoc_consts.Hacspec.new_ in
+  let len:Secret_integers.u8_t =
+    message_3.[ 0 ] ^. Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_MAJOR_BYTE_STRING
+  in
+  let error, plaintext_3:(Edhoc_consts.Common.eDHOCError_t & Edhoc_consts.Hacspec.bytesPlaintext3_t)
+  =
+    if Secret_integers.declassify len = Edhoc_consts.Common.cIPHERTEXT_3_LEN
+    then
+      let ciphertext_3:Edhoc_consts.Hacspec.bytesCiphertext3_t =
+        Edhoc_consts.Hacspec.from_slice message_3 1 Edhoc_consts.Common.cIPHERTEXT_3_LEN
+      in
+      let k_3, iv_3:(Edhoc_consts.Hacspec.bytesCcmKeyLen_t & Edhoc_consts.Hacspec.bytesCcmIvLen_t) =
+        compute_k_3_iv_3 prk_3e2m th_3
+      in
+      let enc_structure:Edhoc_consts.Hacspec.bytesEncStructureLen_t = encode_enc_structure th_3 in
+      let p3:Core.Result.result_t Edhoc_consts.Hacspec.bytesPlaintext3_t
+        Edhoc_consts.Common.eDHOCError_t =
+        Edhoc_crypto_hacspec.aes_ccm_decrypt_tag_8 k_3 iv_3 enc_structure ciphertext_3
+      in
+      if Core.Result.is_ok p3
+      then
+        let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.Success in
+        let plaintext_3:Edhoc_consts.Hacspec.bytesPlaintext3_t =
+          Hacspec_lib_tc.update plaintext_3 0 (Core.Result.unwrap p3)
+        in
+        error, plaintext_3
+      else
+        let error:Edhoc_consts.Common.eDHOCError_t =
+          Core.Option.expect (Core.Result.err p3) "error handling error"
+        in
+        error, plaintext_3
+    else
+      let error:Edhoc_consts.Common.eDHOCError_t = Edhoc_consts.Common.ParsingError in
+      error, plaintext_3
+  in
+  match error with
+  | Edhoc_consts.Common.Success  -> Core.Result.Ok plaintext_3
+  | _ -> Core.Result.Err error
+
+let encode_kdf_context
+      (id_cred: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (th: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (cred: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_len: uint_size)
+    : (Edhoc_consts.Hacspec.bytesMaxContextBuffer_t & uint_size) =
+  let output:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let output:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    Hacspec_lib_tc.update output 0 id_cred
+  in
+  let output:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    output.[ Hacspec_lib_tc.len id_cred ] <-
+      Hacspec_lib_tc.secret Edhoc_consts.Common.cBOR_BYTE_STRING
+  in
+  let output:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    output.[ Hacspec_lib_tc.len id_cred + 1 ] <-
+      Hacspec_lib_tc.secret Edhoc_consts.Common.sHA256_DIGEST_LEN
+  in
+  let output:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    Hacspec_lib_tc.update output (Hacspec_lib_tc.len id_cred + 2) th
+  in
+  let output:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    Hacspec_lib_tc.update_slice output
+      (Hacspec_lib_tc.len id_cred + 2 + Edhoc_consts.Common.sHA256_DIGEST_LEN)
+      cred
+      0
+      cred_len
+  in
+  let output_len:uint_size =
+    Hacspec_lib_tc.len id_cred + 2 + Edhoc_consts.Common.sHA256_DIGEST_LEN + cred_len
+  in
+  output, output_len
+
+let compute_mac_3
+      (prk_4e3m th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (id_cred_i: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (cred_i: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_i_len: uint_size)
+    : Edhoc_consts.Hacspec.bytesMac3_t =
+  let context, context_len:(Edhoc_consts.Hacspec.bytesMaxContextBuffer_t & uint_size) =
+    encode_kdf_context id_cred_i th_3 cred_i cred_i_len
+  in
+  let output_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    edhoc_kdf prk_4e3m
+      (Hacspec_lib_tc.secret 6uy)
+      context
+      context_len
+      Edhoc_consts.Common.mAC_LENGTH_3
+  in
+  Edhoc_consts.Hacspec.from_slice output_buf 0 Edhoc_consts.Common.mAC_LENGTH_3
+
+let compute_mac_2
+      (prk_3e2m: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (id_cred_r: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (cred_r: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (cred_r_len: uint_size)
+      (th_2: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.bytesMac2_t =
+  let context, context_len:(Edhoc_consts.Hacspec.bytesMaxContextBuffer_t & uint_size) =
+    encode_kdf_context id_cred_r th_2 cred_r cred_r_len
+  in
+  Edhoc_consts.Hacspec.from_slice (edhoc_kdf prk_3e2m
+        (Hacspec_lib_tc.secret 2uy)
+        context
+        context_len
+        Edhoc_consts.Common.mAC_LENGTH_2)
+    0
+    Edhoc_consts.Common.mAC_LENGTH_2
+
+let decode_plaintext_2
+      (plaintext_2: Edhoc_consts.Hacspec.bytesMaxBuffer_t)
+      (_plaintext_2_len: uint_size)
+    : (Secret_integers.u8_t & Edhoc_consts.Hacspec.bytesMac2_t & Edhoc_consts.Hacspec.bytesEad2_t) =
+  let id_cred_r:Secret_integers.u8_t = plaintext_2.[ 0l ] in
+  let mac_2:Edhoc_consts.Hacspec.bytesMac2_t =
+    Edhoc_consts.Hacspec.from_slice plaintext_2 2 Edhoc_consts.Common.mAC_LENGTH_2
+  in
+  let ead_2:Edhoc_consts.Hacspec.bytesEad2_t = Edhoc_consts.Hacspec.new_ in
+  id_cred_r, mac_2, ead_2
+
+let encode_plaintext_2
+      (id_cred_r: Edhoc_consts.Hacspec.bytesIdCred_t)
+      (mac_2: Edhoc_consts.Hacspec.bytesMac2_t)
+      (ead_2: Edhoc_consts.Hacspec.bytesEad2_t)
+    : Edhoc_consts.Hacspec.bytesPlaintext2_t =
+  let plaintext_2:Edhoc_consts.Hacspec.bytesPlaintext2_t = Edhoc_consts.Hacspec.new_ in
+  let plaintext_2:Edhoc_consts.Hacspec.bytesPlaintext2_t =
+    plaintext_2.[ 0l ] <- id_cred_r.[ Hacspec_lib_tc.len id_cred_r - 1 ]
+  in
+  let plaintext_2:Edhoc_consts.Hacspec.bytesPlaintext2_t =
+    plaintext_2.[ 1l ] <-
+      Hacspec_lib_tc.secret
+      (Hacspec_lib.|. Edhoc_consts.Common.cBOR_MAJOR_BYTE_STRING Edhoc_consts.Common.mAC_LENGTH_2)
+  in
+  let plaintext_2:Edhoc_consts.Hacspec.bytesPlaintext2_t =
+    Hacspec_lib_tc.update plaintext_2 2 mac_2
+  in
+  Hacspec_lib_tc.update plaintext_2 (2 + Hacspec_lib_tc.len mac_2) ead_2
+
+let encrypt_decrypt_ciphertext_2
+      (prk_2e th_2: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (ciphertext_2: Edhoc_consts.Hacspec.bytesCiphertext2_t)
+    : (Edhoc_consts.Hacspec.bytesMaxBuffer_t & uint_size) =
+  let th_2_context:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    Edhoc_consts.Hacspec.from_slice th_2 0 (Hacspec_lib_tc.len th_2)
+  in
+  let keystream_2:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    edhoc_kdf prk_2e
+      (Hacspec_lib_tc.secret 0uy)
+      th_2_context
+      Edhoc_consts.Common.sHA256_DIGEST_LEN
+      Edhoc_consts.Common.cIPHERTEXT_2_LEN
+  in
+  let plaintext_2:Edhoc_consts.Hacspec.bytesMaxBuffer_t = Edhoc_consts.Hacspec.new_ in
+  let plaintext_2:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    Hacspec.Lib.foldi 0
+      Edhoc_consts.Common.cIPHERTEXT_2_LEN
+      (fun i plaintext_2 -> plaintext_2.[ i ] <- ciphertext_2.[ i ] ^. keystream_2.[ i ])
+      plaintext_2
+  in
+  plaintext_2, Edhoc_consts.Common.cIPHERTEXT_2_LEN
+
+let compute_salt_4e3m (prk_3e2m th_3: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let th_3_context:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    Edhoc_consts.Hacspec.from_slice th_3 0 (Hacspec_lib_tc.len th_3)
+  in
+  let salt_4e3m_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    edhoc_kdf prk_3e2m
+      (Hacspec_lib_tc.secret 5uy)
+      th_3_context
+      (Hacspec_lib_tc.len th_3)
+      Edhoc_consts.Common.sHA256_DIGEST_LEN
+  in
+  let salt_4e3m:Edhoc_consts.Hacspec.bytesHashLen_t = Edhoc_consts.Hacspec.new_ in
+  Hacspec_lib_tc.update_slice salt_4e3m 0 salt_4e3m_buf 0 Edhoc_consts.Common.sHA256_DIGEST_LEN
+
+let compute_prk_4e3m
+      (salt_4e3m: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (i g_y: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let g_iy:Edhoc_consts.Hacspec.bytesP256ElemLen_t = Edhoc_crypto_hacspec.p256_ecdh i g_y in
+  Edhoc_crypto_hacspec.hkdf_extract salt_4e3m g_iy
+
+let compute_salt_3e2m (prk_2e th_2: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let th_2_context:Edhoc_consts.Hacspec.bytesMaxContextBuffer_t =
+    Edhoc_consts.Hacspec.from_slice th_2 0 (Hacspec_lib_tc.len th_2)
+  in
+  let salt_3e2m_buf:Edhoc_consts.Hacspec.bytesMaxBuffer_t =
+    edhoc_kdf prk_2e
+      (Hacspec_lib_tc.secret 1uy)
+      th_2_context
+      Edhoc_consts.Common.sHA256_DIGEST_LEN
+      Edhoc_consts.Common.sHA256_DIGEST_LEN
+  in
+  let salt_3e2m:Edhoc_consts.Hacspec.bytesHashLen_t = Edhoc_consts.Hacspec.new_ in
+  Hacspec_lib_tc.update_slice salt_3e2m 0 salt_3e2m_buf 0 Edhoc_consts.Common.sHA256_DIGEST_LEN
+
+let compute_prk_3e2m
+      (salt_3e2m: Edhoc_consts.Hacspec.bytesHashLen_t)
+      (x g_r: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let g_rx:Edhoc_consts.Hacspec.bytesP256ElemLen_t = Edhoc_crypto_hacspec.p256_ecdh x g_r in
+  Edhoc_crypto_hacspec.hkdf_extract salt_3e2m g_rx
+
+let compute_prk_2e
+      (x g_y: Edhoc_consts.Hacspec.bytesP256ElemLen_t)
+      (th_2: Edhoc_consts.Hacspec.bytesHashLen_t)
+    : Edhoc_consts.Hacspec.bytesHashLen_t =
+  let g_xy:Edhoc_consts.Hacspec.bytesP256ElemLen_t = Edhoc_crypto_hacspec.p256_ecdh x g_y in
+  Edhoc_crypto_hacspec.hkdf_extract th_2 g_xy
\ No newline at end of file
diff --git a/hacspec/src/lib.rs b/hacspec/src/lib.rs
index 55359ca9..1c9a57e7 100644
--- a/hacspec/src/lib.rs
+++ b/hacspec/src/lib.rs
@@ -60,9 +60,9 @@ pub fn r_process_message_1(
         let (method, supported_suites, g_x, c_i) = parse_message_1(message_1);
 
         // verify that the method is supported
-        if method.declassify() == EDHOC_METHOD {
+        if method == EDHOC_METHOD {
             // Step 2: verify that the selected cipher suite is supported
-            if supported_suites[0u8].declassify() == EDHOC_SUPPORTED_SUITES[0u8].declassify() {
+            if supported_suites[0] == EDHOC_SUPPORTED_SUITES[0u8].declassify() {
                 // Step 3: If EAD is present make it available to the application
                 // TODO we do not support EAD for now
 
@@ -220,7 +220,7 @@ pub fn r_process_message_3(
             let (kid, mac_3) = decode_plaintext_3(&plaintext_3);
 
             // compare the kid received with the kid expected in id_cred_i
-            if kid.declassify() == id_cred_i_expected[id_cred_i_expected.len() - 1].declassify() {
+            if kid == id_cred_i_expected[id_cred_i_expected.len() - 1].declassify() {
                 // compute salt_4e3m
                 let salt_4e3m = compute_salt_4e3m(&prk_3e2m, &th_3);
                 // TODO compute prk_4e3m
@@ -420,7 +420,7 @@ pub fn i_process_message_2(
 
         // Check MAC before checking KID
         if mac_2.declassify_eq(&expected_mac_2) {
-            if kid.declassify() == id_cred_r_expected[id_cred_r_expected.len() - 1].declassify() {
+            if kid == id_cred_r_expected[id_cred_r_expected.len() - 1].declassify() {
                 // step is actually from processing of message_3
                 // but we do it here to avoid storing plaintext_2 in State
                 th_3 = compute_th_3(
@@ -571,11 +571,11 @@ pub fn construct_state(
 
 fn parse_message_1(
     rcvd_message_1: &BytesMessage1,
-) -> (U8, BytesSupportedSuites, BytesP256ElemLen, U8) {
-    let method = rcvd_message_1[0];
+) -> (u8, [u8; SUPPORTED_SUITES_LEN], BytesP256ElemLen, U8) {
+    let method = (rcvd_message_1[0] as U8).declassify();
     // FIXME as we only support a fixed-sized incoming message_1,
     // we parse directly the selected cipher suite
-    let selected_suite = BytesSupportedSuites::from_slice(rcvd_message_1, 1, 1);
+    let selected_suite = BytesSupportedSuites::from_slice(rcvd_message_1, 1, 1).to_public_array();
     let g_x = BytesP256ElemLen::from_slice(rcvd_message_1, 4, P256_ELEM_LEN);
     let c_i = rcvd_message_1[MESSAGE_1_LEN - 1];
 
@@ -717,8 +717,8 @@ fn edhoc_kdf(
     output
 }
 
-fn decode_plaintext_3(plaintext_3: &BytesPlaintext3) -> (U8, BytesMac3) {
-    let kid = plaintext_3[0usize];
+fn decode_plaintext_3(plaintext_3: &BytesPlaintext3) -> (u8, BytesMac3) {
+    let kid = (plaintext_3[0usize] as U8).declassify();
     // skip the CBOR magic byte as we know how long the MAC is
     let mac_3 = BytesMac3::from_slice(plaintext_3, 2, MAC_LENGTH_3);
 
@@ -919,8 +919,8 @@ fn compute_mac_2(
 fn decode_plaintext_2(
     plaintext_2: &BytesMaxBuffer,
     _plaintext_2_len: usize,
-) -> (U8, BytesMac2, BytesEad2) {
-    let id_cred_r = plaintext_2[0];
+) -> (u8, BytesMac2, BytesEad2) {
+    let id_cred_r = (plaintext_2[0] as U8).declassify();
     // skip cbor byte string byte as we know how long the string is
     let mac_2 = BytesMac2::from_slice(plaintext_2, 2, MAC_LENGTH_2);
     // FIXME we don't support ead_2 parsing for now
@@ -1110,14 +1110,14 @@ mod tests {
     fn test_parse_message_1() {
         let message_1_tv = BytesMessage1::from_hex(MESSAGE_1_TV);
         let method_tv = METHOD_TV;
-        let supported_suites_tv = BytesSupportedSuites::from_hex(SUITES_I_TV);
+        let supported_suites_tv = BytesSupportedSuites::from_hex(SUITES_I_TV).to_public_array();
         let g_x_tv = BytesP256ElemLen::from_hex(G_X_TV);
         let c_i_tv = U8(C_I_TV);
 
         let (method, supported_suites, g_x, c_i) = parse_message_1(&message_1_tv);
 
-        assert_eq!(method.declassify(), method_tv);
-        assert_bytes_eq!(supported_suites, supported_suites_tv);
+        assert_eq!(method, method_tv);
+        assert_eq!(supported_suites, supported_suites_tv);
         assert_bytes_eq!(g_x, g_x_tv);
         assert_eq!(c_i.declassify(), c_i_tv.declassify());
     }
@@ -1309,7 +1309,7 @@ mod tests {
         let ead_2_tv = BytesEad2::new();
 
         let (id_cred_r, mac_2, ead_2) = decode_plaintext_2(&plaintext_2_tv, PLAINTEXT_2_LEN);
-        assert_eq!(U8::declassify(id_cred_r), U8::declassify(id_cred_r_tv[3]));
+        assert_eq!(id_cred_r, U8::declassify(id_cred_r_tv[3]));
         assert_bytes_eq!(mac_2, mac_2_tv);
         assert_bytes_eq!(ead_2, ead_2_tv);
     }
@@ -1398,6 +1398,6 @@ mod tests {
         let (kid, mac_3) = decode_plaintext_3(&plaintext_3_tv);
 
         assert_bytes_eq!(mac_3, mac_3_tv);
-        assert_eq!(kid.declassify(), kid_tv.declassify());
+        assert_eq!(kid, kid_tv.declassify());
     }
 }