text: /*
   * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   *
   * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
   * this file except in compliance with the License. A copy of the License is
   * located at
   *
   *     http://aws.amazon.com/apache2.0/
   *
   * or in the "license" file accompanying this file. This file is distributed on an
   * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   * implied. See the License for the specific language governing permissions and
   * limitations under the License.
   */
  
  #pragma once
  
  #include <cbmc_proof/nondet.h>
  #include <crypto/s2n_hash.h>
  #include <stddef.h>
  #include <stdint.h>
  #include <stuffer/s2n_stuffer.h>
  #include <utils/s2n_blob.h>
  
  #define IMPLIES(a, b) (!(a) || (b))
  #define CBMC_ENSURE_REF(cond)    \
      do {                         \
          if (!(cond)) { return; } \
      } while (0)
  
  struct store_byte_from_buffer {
      size_t  idx;
      uint8_t byte;
  };
  
  /**
   * Reference counted keys (EVP_PKEY and EC_KEY) store the reference count
   * within the key itself, thus making it potentially unavailable after the
   * key get deallocated.
   * In the `rc_keys_from_evp_pkey_ctx`, we store the reference count outside of the key,
   * so we can assert properties on them regardless of whether keys was deallocated or not.
   */
  struct rc_keys_from_evp_pkey_ctx {
      EVP_PKEY *pkey;
      int pkey_refs;
      EC_KEY *pkey_eckey;
      int pkey_eckey_refs;
  };
  
  /**
   * In the `rc_keys_from_hash_state`, we store two `rc_keys_from_evp_pkey_ctx` objects:
   * one for the `evp` field and another for `evp_md5_secondary` field.
   */
  struct rc_keys_from_hash_state {
      struct rc_keys_from_evp_pkey_ctx evp;
      struct rc_keys_from_evp_pkey_ctx evp_md5;
  };
  
  /**
   * Asserts two s2n_stuffer instances are equivalent, except for read_cursor,
   * which might change after a read operation. In order to be considered equivalent,
   * all members (except for read_cursor) from both instances must match, including
   * all bytes from their underlying blobs (i.e., blob.data field). Prior to using
   * this function, it is necessary to select a non-deterministic byte from the
   * rhs s2n_blob instance (use save_byte_from_blob function), so it can properly
   * assert all bytes from blob.data match.
   */
  void assert_stuffer_immutable_fields_after_read(const struct s2n_stuffer *lhs, const struct s2n_stuffer *rhs,
                                                  const struct store_byte_from_buffer *stored_byte_from_rhs);
  
  /**
   * Asserts two s2n_blob instances are equivalent. In order to be considered equivalent,
   * all members from both instances must match, including all bytes from their underlying
   * buffers (i.e., *data field). Prior to using this function, it is necessary to select
   * a non-deterministic byte from the rhs s2n_blob instance (use save_byte_from_blob function),
   * so it can properly assert all bytes from *data match.
   */
  void assert_blob_equivalence(const struct s2n_blob *lhs, const struct s2n_blob *rhs,
                               const struct store_byte_from_buffer *stored_byte_from_rhs);
  
  /**
   * Asserts two s2n_stuffer instances are equivalent. In order to be considered equivalent,
   * all members from both instances must match, including all bytes from their underlying
   * blobs (i.e., blob.data field). Prior to using this function, it is necessary to select
   * a non-deterministic byte from the rhs s2n_blob instance (use save_byte_from_blob function),
   * so it can properly assert all bytes from blob.data match.
   */
  void assert_stuffer_equivalence(const struct s2n_stuffer *lhs, const struct s2n_stuffer *rhs,
                                  const struct store_byte_from_buffer *stored_byte_from_rhs);
  
  /**
   * Asserts whether all bytes from two arrays of same length match.
   */
  void assert_bytes_match(const uint8_t *const a, const uint8_t *const b, const size_t len);
  
  /**
   * Asserts whether all bytes from an array are equal to c.
   */
  void assert_all_bytes_are(const uint8_t *const a, const uint8_t c, const size_t len);
  
  /**
   * Asserts whether all bytes from an array are equal to 0.
   */
  void assert_all_zeroes(const uint8_t *const a, const size_t len);
  
  /**
   * Asserts whether the byte in storage correspond to the byte in the same position in buffer.
   */
  void assert_byte_from_buffer_matches(const uint8_t *const buffer, const struct store_byte_from_buffer *const b);
  
  /**
   * Asserts whether the byte in storage correspond to the byte in the same position in buffer.
   */
  void assert_byte_from_blob_matches(const struct s2n_blob *blob, const struct store_byte_from_buffer *const b);
  
  /**
   * Assert that the reference counts in `storage` have decremented by 1 (if they were > 1).
   * We cannot check anything if the previous reference count was 1, because the key is deallocated in that case.
   */
  void assert_rc_decrement_on_evp_pkey_ctx(struct rc_keys_from_evp_pkey_ctx *storage);
  
  /**
   * Assert that the reference counts in `storage` have decremented by 1 (if they were > 1).
   * We cannot check anything if the previous reference count was 1, because the key is deallocated in that case.
   */
  void assert_rc_unchanged_on_evp_pkey_ctx(struct rc_keys_from_evp_pkey_ctx *storage);
  
  /**
   * Assert that the reference counts in `storage` are unchanged.
   */
  void assert_rc_decrement_on_hash_state(struct rc_keys_from_hash_state *storage);
  
  /**
   * Assert that the reference counts in `storage` are unchanged.
   */
  void assert_rc_unchanged_on_hash_state(struct rc_keys_from_hash_state *storage);
  
  /**
   * Save reference-counted keys from an `EVP_PKEY_CTX`.
   * Afterwards, one can assert that keys have changed as expected (e.g. after `s2n_hash_free`), i.e.,
   * reference counts have either decreased by 1: see `assert_rc_decrement_on_evp_pkey_ctx`.
   * Additionally, one can also `free` the keys that are left with non-zero reference counts,
   * if that's expected, using `free_rc_keys_from_evp_pkey_ctx` for memory leak check to go through.
   */
  void save_rc_keys_from_evp_pkey_ctx(const EVP_PKEY_CTX *pctx, struct rc_keys_from_evp_pkey_ctx *storage);
  
  /**
   * Save reference-counted keys from an `s2n_hash_state`.
   * Afterwards, one can assert that keys have changed as expected (e.g. after `s2n_hash_free`), i.e.,
   * reference counts have either decreased by 1: see `assert_rc_decrement_on_hash_state`.
   * Additionally, one can also `free` the keys that are left with non-zero reference counts,
   * if that's expected, using `free_rc_keys_from_hash_state` for memory leak check to go through.
   */
  void save_rc_keys_from_hash_state(const struct s2n_hash_state *state, struct rc_keys_from_hash_state *storage);
  
  /**
   * Nondeterministically selects a byte from array and stores it into a store_array_list_byte
   * structure. Afterwards, one can prove using the assert_byte_from_buffer_matches function
   * whether no byte in the array has changed.
   */
  void save_byte_from_array(const uint8_t *const array, const size_t size, struct store_byte_from_buffer *const storage);
  
  /**
   * Nondeterministically selects a byte from blob and stores it into a store_array_list_byte
   * structure. Afterwards, one can prove using the assert_byte_from_blob_matches function
   * whether no byte in the blob has changed.
   */
  void save_byte_from_blob(const struct s2n_blob *blob, struct store_byte_from_buffer *storage);
  
  /**
   * Free all ref-counted keys in `storage` that earlier had a reference count != 1.
   */
  void free_rc_keys_from_evp_pkey_ctx(struct rc_keys_from_evp_pkey_ctx *pctx);
  
  /**
   * Free all ref-counted keys in `storage` that earlier had a reference count != 1.
   */
  void free_rc_keys_from_hash_state(struct rc_keys_from_hash_state *storage);
  
  /**
   * Standard stub function to compare two items.
   */
  int nondet_compare(const void *const a, const void *const b);
  
  /**
   * Standard stub function to compare two items.
   */
  int uninterpreted_compare(const void *const a, const void *const b);
  
  /**
   * Standard stub function to compare two items.
   */
  bool nondet_equals(const void *const a, const void *const b);
  
  /**
   * Standard stub function to compare two items.
   * Also enforces uninterpreted_hasher() to be equal for equal values.
   */
  bool uninterpreted_equals(const void *const a, const void *const b);
  
  /**
   * uninterpreted_equals(), but with an extra assertion that a and b are both not null
   */
  bool uninterpreted_equals_assert_inputs_nonnull(const void *const a, const void *const b);
  
  /**
   * Standard stub function to hash one item.
   */
  uint64_t nondet_hasher(const void *a);
  
  /**
   * Standard stub function to hash one item.
   */
  uint64_t uninterpreted_hasher(const void *a);
  
  /**
   * Standard stub function of a predicate.
   */
  bool uninterpreted_predicate_fn(uint8_t value);
  
  /**
   * Non-deterministically set initialized (in s2n_mem) to true.
   */
  void nondet_s2n_mem_init();
  