text:
(*Generated by Sail from riscv_duopod.*)
Require Import Sail2_instr_kinds.
Require Import Sail2_values.
Require Import Sail2_string.
Require Import Sail2_real.
Require Import Sail2_operators_mwords.
Require Import Sail2_prompt_monad.
Require Import Sail2_prompt.
Require Import Sail2_state.
Require Import riscv_duopod_types.
Require Import riscv_extras.
Import ListNotations.
Open Scope string.
Open Scope bool.
Section Content.

Definition is_none {a : Type} (opt : option a)
: bool :=

   match opt with | Some (_) => false | None => true end.

Definition is_some {a : Type} (opt : option a)
: bool :=

   match opt with | Some (_) => true | None => false end.

Definition eq_unit (_ : unit) (_ : unit)
: {_bool : bool & ArithFact (_bool = true)} :=

   build_ex(true).

Definition neq_int (x : Z) (y : Z)
: {_bool : bool & ArithFact (iff (_bool = true) (x <> y))} :=

   build_ex(negb (Z.eqb x y)).

Definition neq_bool (x : bool) (y : bool)  : bool :=  negb (Bool.eqb x y).

Definition __id (x : Z)  : {_retval : Z & ArithFact (_retval = x)} :=  build_ex(x).

Definition concat_str_bits {n : Z} (str : string) (x : mword n)
: string :=

   String.append str (string_of_bits x).

Definition concat_str_dec (str : string) (x : Z)  : string :=  String.append str (dec_str x).

Definition sail_mask {v0 : Z} (len : Z) (v : mword v0) `{ArithFact (len >= 0 /\ v0 >= 0)}
: mword len :=

   if sumbool_of_bool ((Z.leb len (length_mword v))) then vector_truncate v len
   else zero_extend v len.

Definition sail_ones (n : Z) `{ArithFact (n >= 0)}  : mword n :=  not_vec (zeros n).

Definition slice_mask (n : Z) (i : Z) (l : Z) `{ArithFact (n >= 0)}
: mword n :=

   if sumbool_of_bool ((Z.geb l n)) then shiftl (sail_ones n) i
   else
     let one : bits n := sail_mask n ((vec_of_bits [B1]  : mword 1)  : bits 1) in
     shiftl (sub_vec (shiftl one l) one) i.

Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)}
: read_kind :=

   let l__34 := arg_ in
   if sumbool_of_bool ((Z.eqb l__34 0)) then Read_plain
   else if sumbool_of_bool ((Z.eqb l__34 1)) then Read_reserve
   else if sumbool_of_bool ((Z.eqb l__34 2)) then Read_acquire
   else if sumbool_of_bool ((Z.eqb l__34 3)) then Read_exclusive
   else if sumbool_of_bool ((Z.eqb l__34 4)) then Read_exclusive_acquire
   else if sumbool_of_bool ((Z.eqb l__34 5)) then Read_stream
   else if sumbool_of_bool ((Z.eqb l__34 6)) then Read_RISCV_acquire
   else if sumbool_of_bool ((Z.eqb l__34 7)) then Read_RISCV_strong_acquire
   else if sumbool_of_bool ((Z.eqb l__34 8)) then Read_RISCV_reserved
   else if sumbool_of_bool ((Z.eqb l__34 9)) then Read_RISCV_reserved_acquire
   else if sumbool_of_bool ((Z.eqb l__34 10)) then Read_RISCV_reserved_strong_acquire
   else Read_X86_locked.

Definition num_of_read_kind (arg_ : read_kind)
: {e : Z & ArithFact (0 <= e /\ e <= 11)} :=

   build_ex(match arg_ with
            | Read_plain => 0
            | Read_reserve => 1
            | Read_acquire => 2
            | Read_exclusive => 3
            | Read_exclusive_acquire => 4
            | Read_stream => 5
            | Read_RISCV_acquire => 6
            | Read_RISCV_strong_acquire => 7
            | Read_RISCV_reserved => 8
            | Read_RISCV_reserved_acquire => 9
            | Read_RISCV_reserved_strong_acquire => 10
            | Read_X86_locked => 11
            end).

Definition write_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 10)}
: write_kind :=

   let l__24 := arg_ in
   if sumbool_of_bool ((Z.eqb l__24 0)) then Write_plain
   else if sumbool_of_bool ((Z.eqb l__24 1)) then Write_conditional
   else if sumbool_of_bool ((Z.eqb l__24 2)) then Write_release
   else if sumbool_of_bool ((Z.eqb l__24 3)) then Write_exclusive
   else if sumbool_of_bool ((Z.eqb l__24 4)) then Write_exclusive_release
   else if sumbool_of_bool ((Z.eqb l__24 5)) then Write_RISCV_release
   else if sumbool_of_bool ((Z.eqb l__24 6)) then Write_RISCV_strong_release
   else if sumbool_of_bool ((Z.eqb l__24 7)) then Write_RISCV_conditional
   else if sumbool_of_bool ((Z.eqb l__24 8)) then Write_RISCV_conditional_release
   else if sumbool_of_bool ((Z.eqb l__24 9)) then Write_RISCV_conditional_strong_release
   else Write_X86_locked.

Definition num_of_write_kind (arg_ : write_kind)
: {e : Z & ArithFact (0 <= e /\ e <= 10)} :=

   build_ex(match arg_ with
            | Write_plain => 0
            | Write_conditional => 1
            | Write_release => 2
            | Write_exclusive => 3
            | Write_exclusive_release => 4
            | Write_RISCV_release => 5
            | Write_RISCV_strong_release => 6
            | Write_RISCV_conditional => 7
            | Write_RISCV_conditional_release => 8
            | Write_RISCV_conditional_strong_release => 9
            | Write_X86_locked => 10
            end).

Definition a64_barrier_domain_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 3)}
: a64_barrier_domain :=

   let l__21 := arg_ in
   if sumbool_of_bool ((Z.eqb l__21 0)) then A64_FullShare
   else if sumbool_of_bool ((Z.eqb l__21 1)) then A64_InnerShare
   else if sumbool_of_bool ((Z.eqb l__21 2)) then A64_OuterShare
   else A64_NonShare.

Definition num_of_a64_barrier_domain (arg_ : a64_barrier_domain)
: {e : Z & ArithFact (0 <= e /\ e <= 3)} :=

   build_ex(match arg_ with
            | A64_FullShare => 0
            | A64_InnerShare => 1
            | A64_OuterShare => 2
            | A64_NonShare => 3
            end).

Definition a64_barrier_type_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)}
: a64_barrier_type :=

   let l__19 := arg_ in
   if sumbool_of_bool ((Z.eqb l__19 0)) then A64_barrier_all
   else if sumbool_of_bool ((Z.eqb l__19 1)) then A64_barrier_LD
   else A64_barrier_ST.

Definition num_of_a64_barrier_type (arg_ : a64_barrier_type)
: {e : Z & ArithFact (0 <= e /\ e <= 2)} :=

   build_ex(match arg_ with | A64_barrier_all => 0 | A64_barrier_LD => 1 | A64_barrier_ST => 2 end).

Definition trans_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)}
: trans_kind :=

   let l__17 := arg_ in
   if sumbool_of_bool ((Z.eqb l__17 0)) then Transaction_start
   else if sumbool_of_bool ((Z.eqb l__17 1)) then Transaction_commit
   else Transaction_abort.

Definition num_of_trans_kind (arg_ : trans_kind)
: {e : Z & ArithFact (0 <= e /\ e <= 2)} :=

   build_ex(match arg_ with
            | Transaction_start => 0
            | Transaction_commit => 1
            | Transaction_abort => 2
            end).

Definition cache_op_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 10)}
: cache_op_kind :=

   let l__7 := arg_ in
   if sumbool_of_bool ((Z.eqb l__7 0)) then Cache_op_D_IVAC
   else if sumbool_of_bool ((Z.eqb l__7 1)) then Cache_op_D_ISW
   else if sumbool_of_bool ((Z.eqb l__7 2)) then Cache_op_D_CSW
   else if sumbool_of_bool ((Z.eqb l__7 3)) then Cache_op_D_CISW
   else if sumbool_of_bool ((Z.eqb l__7 4)) then Cache_op_D_ZVA
   else if sumbool_of_bool ((Z.eqb l__7 5)) then Cache_op_D_CVAC
   else if sumbool_of_bool ((Z.eqb l__7 6)) then Cache_op_D_CVAU
   else if sumbool_of_bool ((Z.eqb l__7 7)) then Cache_op_D_CIVAC
   else if sumbool_of_bool ((Z.eqb l__7 8)) then Cache_op_I_IALLUIS
   else if sumbool_of_bool ((Z.eqb l__7 9)) then Cache_op_I_IALLU
   else Cache_op_I_IVAU.

Definition num_of_cache_op_kind (arg_ : cache_op_kind)
: {e : Z & ArithFact (0 <= e /\ e <= 10)} :=

   build_ex(match arg_ with
            | Cache_op_D_IVAC => 0
            | Cache_op_D_ISW => 1
            | Cache_op_D_CSW => 2
            | Cache_op_D_CISW => 3
            | Cache_op_D_ZVA => 4
            | Cache_op_D_CVAC => 5
            | Cache_op_D_CVAU => 6
            | Cache_op_D_CIVAC => 7
            | Cache_op_I_IALLUIS => 8
            | Cache_op_I_IALLU => 9
            | Cache_op_I_IVAU => 10
            end).

Definition neq_vec {n : Z} (x : mword n) (y : mword n)  : bool :=  negb (eq_vec x y).

Definition cast_unit_vec (b : bitU)
: M (mword 1) :=

   (match b with
    | B0 => returnm ((vec_of_bits [B0]  : mword 1)  : mword 1)
    | B1 => returnm ((vec_of_bits [B1]  : mword 1)  : mword 1)
    | _ => exit tt  : M (mword 1)
    end)
    : M (mword 1).

Definition get_config_print_instr '(tt : unit)  : bool :=  false.

Definition get_config_print_reg '(tt : unit)  : bool :=  false.

Definition get_config_print_mem '(tt : unit)  : bool :=  false.

Definition get_config_print_platform '(tt : unit)  : bool :=  false.

Definition EXTS {n : Z} (m : Z) (v : mword n) `{ArithFact (m >= n)}  : mword m :=  sign_extend v m.

Definition EXTZ {n : Z} (m : Z) (v : mword n) `{ArithFact (m >= n)}  : mword m :=  zero_extend v m.

Definition zeros_implicit (n : Z) `{ArithFact (n >= 0)}  : mword n :=  zeros n.

Definition zeros (n : Z) `{ArithFact (n >= 0)}
: mword n :=

   autocast (replicate_bits (vec_of_bits [B0]  : mword 1) n).

Definition ones (n : Z) `{ArithFact (n >= 0)}  : mword n :=  sail_ones n.

Definition bool_to_bits (x : bool)
: mword 1 :=

   if sumbool_of_bool (x) then (vec_of_bits [B1]  : mword 1)
   else (vec_of_bits [B0]  : mword 1).

Definition bit_to_bool (b : bitU)
: M (bool) :=

   (match b with
    | B1 => returnm (projT1 (build_ex true  : {_bool : bool & ArithFact (_bool = true)}))
    | B0 => returnm (projT1 (build_ex false  : {_bool : bool & ArithFact (not (_bool = true))}))
    | _ => exit tt  : M (bool)
    end)
    : M (bool).

Definition to_bits (l : Z) (n : Z) `{ArithFact (l >= 0)}  : mword l :=  get_slice_int l n 0.

Definition zopz0zI_s {n : Z} (x : mword n) (y : mword n) `{ArithFact (n > 0)}
: bool :=

   Z.ltb (projT1 (sint x)) (projT1 (sint y)).

Definition zopz0zKzJ_s {n : Z} (x : mword n) (y : mword n) `{ArithFact (n > 0)}
: bool :=

   Z.geb (projT1 (sint x)) (projT1 (sint y)).

Definition zopz0zI_u {n : Z} (x : mword n) (y : mword n)
: bool :=

   Z.ltb (projT1 (uint x)) (projT1 (uint y)).

Definition zopz0zKzJ_u {n : Z} (x : mword n) (y : mword n)
: bool :=

   Z.geb (projT1 (uint x)) (projT1 (uint y)).

Definition zopz0zIzJ_u {n : Z} (x : mword n) (y : mword n)
: bool :=

   Z.leb (projT1 (uint x)) (projT1 (uint y)).

Definition shift_right_arith64 (v : mword 64) (shift : mword 6)
: mword 64 :=

   let v128 : bits 128 := EXTS 128 v in
   subrange_vec_dec (shift_bits_right v128 shift) 63 0.

Definition shift_right_arith32 (v : mword 32) (shift : mword 5)
: mword 32 :=

   let v64 : bits 64 := EXTS 64 v in
   subrange_vec_dec (shift_bits_right v64 shift) 31 0.

Fixpoint _rec_n_leading_spaces (s : string) (_reclimit : Z)  (_acc : Acc (Zwf 0) _reclimit)
{struct _acc} : M ({n : Z & ArithFact (n >= 0)}) :=

   assert_exp' (Z.geb _reclimit 0) "recursion limit reached" >>= fun _ =>
   let p0_ := s in
   (if ((generic_eq p0_ "")) then returnm (build_ex (0  : Z))
    else
      let p0_ := string_take s 1 in
      (if ((generic_eq p0_ " ")) then
         (_rec_n_leading_spaces (string_drop s 1) (Z.sub _reclimit 1) (_limit_reduces _acc)) >>= fun '(existT _ w__0 _ : {n : Z & ArithFact (n >=
           0)}) =>
         returnm (build_ex
         (projT1
         (build_ex
         (Z.add 1 w__0)
          : {_atom : Z & ArithFact (exists ex4231_ , _atom = (1 + ex4231_) /\ 0 <= ex4231_)})))
       else returnm (build_ex (0  : Z)))
       : M ({n : Z & ArithFact (n >= 0)}))
    : M ({n : Z & ArithFact (n >= 0)}).

Definition n_leading_spaces (s : string)
: M ({n : Z & ArithFact (n >= 0)}) :=

   (_rec_n_leading_spaces s ((projT1 (string_length s))  : Z) (Zwf_guarded _))
    : M ({n : Z & ArithFact (n >= 0)}).

Definition spc_forwards '(tt : unit)  : string :=  " ".

Definition spc_backwards (s : string)  : unit :=  tt.

Definition spc_matches_prefix (s : string)
: M (option ((unit * {n : Z & ArithFact (n >= 0)}))) :=

   (n_leading_spaces s) >>= fun '(existT _ n _) =>
   let l__6 := n in
   returnm ((if sumbool_of_bool ((Z.eqb l__6 0)) then None
             else Some ((tt, build_ex n)))
    : option ((unit * {n : Z & ArithFact (n >= 0)}))).

Definition opt_spc_forwards '(tt : unit)  : string :=  "".

Definition opt_spc_backwards (s : string)  : unit :=  tt.

Definition opt_spc_matches_prefix (s : string)
: M (option ((unit * {n : Z & ArithFact (n >= 0)}))) :=

   (n_leading_spaces s) >>= fun '(existT _ w__0 _ : {n : Z & ArithFact (n >= 0)}) =>
   returnm ((Some
               ((tt, build_ex
               w__0)))
    : option ((unit * {n : Z & ArithFact (n >= 0)}))).

Definition def_spc_forwards '(tt : unit)  : string :=  " ".

Definition def_spc_backwards (s : string)  : unit :=  tt.

Definition def_spc_matches_prefix (s : string)
: M (option ((unit * {n : Z & ArithFact (n >= 0)}))) :=

   (opt_spc_matches_prefix s)
    : M (option ((unit * {n : Z & ArithFact (n >= 0)}))).

Definition hex_bits_1_forwards_matches (bv : mword 1)  : bool :=  true.

Definition hex_bits_1_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_1_matches_prefix s) with
           | Some ((g__79, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_1_backwards (s : string)
: M (mword 1) :=

   (match (hex_bits_1_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 1)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 49:2 - 51:3" >>= fun _ =>
          exit tt)
        : M (mword 1)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 49:2 - 51:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 1).

Definition hex_bits_2_forwards_matches (bv : mword 2)  : bool :=  true.

Definition hex_bits_2_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_2_matches_prefix s) with
           | Some ((g__78, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_2_backwards (s : string)
: M (mword 2) :=

   (match (hex_bits_2_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 2)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 68:2 - 70:3" >>= fun _ =>
          exit tt)
        : M (mword 2)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 68:2 - 70:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 2).

Definition hex_bits_3_forwards_matches (bv : mword 3)  : bool :=  true.

Definition hex_bits_3_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_3_matches_prefix s) with
           | Some ((g__77, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_3_backwards (s : string)
: M (mword 3) :=

   (match (hex_bits_3_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 3)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 87:2 - 89:3" >>= fun _ =>
          exit tt)
        : M (mword 3)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 87:2 - 89:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 3).

Definition hex_bits_4_forwards_matches (bv : mword 4)  : bool :=  true.

Definition hex_bits_4_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_4_matches_prefix s) with
           | Some ((g__76, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_4_backwards (s : string)
: M (mword 4) :=

   (match (hex_bits_4_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 4)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 106:2 - 108:3" >>= fun _ =>
          exit tt)
        : M (mword 4)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 106:2 - 108:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 4).

Definition hex_bits_5_forwards_matches (bv : mword 5)  : bool :=  true.

Definition hex_bits_5_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_5_matches_prefix s) with
           | Some ((g__75, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_5_backwards (s : string)
: M (mword 5) :=

   (match (hex_bits_5_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 5)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 125:2 - 127:3" >>= fun _ =>
          exit tt)
        : M (mword 5)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 125:2 - 127:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 5).

Definition hex_bits_6_forwards_matches (bv : mword 6)  : bool :=  true.

Definition hex_bits_6_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_6_matches_prefix s) with
           | Some ((g__74, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_6_backwards (s : string)
: M (mword 6) :=

   (match (hex_bits_6_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 6)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 144:2 - 146:3" >>= fun _ =>
          exit tt)
        : M (mword 6)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 144:2 - 146:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 6).

Definition hex_bits_7_forwards_matches (bv : mword 7)  : bool :=  true.

Definition hex_bits_7_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_7_matches_prefix s) with
           | Some ((g__73, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_7_backwards (s : string)
: M (mword 7) :=

   (match (hex_bits_7_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 7)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 163:2 - 165:3" >>= fun _ =>
          exit tt)
        : M (mword 7)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 163:2 - 165:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 7).

Definition hex_bits_8_forwards_matches (bv : mword 8)  : bool :=  true.

Definition hex_bits_8_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_8_matches_prefix s) with
           | Some ((g__72, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_8_backwards (s : string)
: M (mword 8) :=

   (match (hex_bits_8_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 8)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 182:2 - 184:3" >>= fun _ =>
          exit tt)
        : M (mword 8)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 182:2 - 184:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 8).

Definition hex_bits_9_forwards_matches (bv : mword 9)  : bool :=  true.

Definition hex_bits_9_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_9_matches_prefix s) with
           | Some ((g__71, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_9_backwards (s : string)
: M (mword 9) :=

   (match (hex_bits_9_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 9)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 201:2 - 203:3" >>= fun _ =>
          exit tt)
        : M (mword 9)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 201:2 - 203:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 9).

Definition hex_bits_10_forwards_matches (bv : mword 10)  : bool :=  true.

Definition hex_bits_10_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_10_matches_prefix s) with
           | Some ((g__70, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_10_backwards (s : string)
: M (mword 10) :=

   (match (hex_bits_10_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 10)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 220:2 - 222:3" >>= fun _ =>
          exit tt)
        : M (mword 10)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 220:2 - 222:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 10).

Definition hex_bits_11_forwards_matches (bv : mword 11)  : bool :=  true.

Definition hex_bits_11_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_11_matches_prefix s) with
           | Some ((g__69, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_11_backwards (s : string)
: M (mword 11) :=

   (match (hex_bits_11_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 11)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 239:2 - 241:3" >>= fun _ =>
          exit tt)
        : M (mword 11)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 239:2 - 241:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 11).

Definition hex_bits_12_forwards_matches (bv : mword 12)  : bool :=  true.

Definition hex_bits_12_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_12_matches_prefix s) with
           | Some ((g__68, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_12_backwards (s : string)
: M (mword 12) :=

   (match (hex_bits_12_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 12)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 258:2 - 260:3" >>= fun _ =>
          exit tt)
        : M (mword 12)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 258:2 - 260:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 12).

Definition hex_bits_13_forwards_matches (bv : mword 13)  : bool :=  true.

Definition hex_bits_13_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_13_matches_prefix s) with
           | Some ((g__67, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_13_backwards (s : string)
: M (mword 13) :=

   (match (hex_bits_13_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 13)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 277:2 - 279:3" >>= fun _ =>
          exit tt)
        : M (mword 13)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 277:2 - 279:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 13).

Definition hex_bits_14_forwards_matches (bv : mword 14)  : bool :=  true.

Definition hex_bits_14_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_14_matches_prefix s) with
           | Some ((g__66, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_14_backwards (s : string)
: M (mword 14) :=

   (match (hex_bits_14_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 14)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 296:2 - 298:3" >>= fun _ =>
          exit tt)
        : M (mword 14)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 296:2 - 298:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 14).

Definition hex_bits_15_forwards_matches (bv : mword 15)  : bool :=  true.

Definition hex_bits_15_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_15_matches_prefix s) with
           | Some ((g__65, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_15_backwards (s : string)
: M (mword 15) :=

   (match (hex_bits_15_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 15)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 315:2 - 317:3" >>= fun _ =>
          exit tt)
        : M (mword 15)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 315:2 - 317:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 15).

Definition hex_bits_16_forwards_matches (bv : mword 16)  : bool :=  true.

Definition hex_bits_16_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_16_matches_prefix s) with
           | Some ((g__64, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_16_backwards (s : string)
: M (mword 16) :=

   (match (hex_bits_16_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 16)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 334:2 - 336:3" >>= fun _ =>
          exit tt)
        : M (mword 16)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 334:2 - 336:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 16).

Definition hex_bits_17_forwards_matches (bv : mword 17)  : bool :=  true.

Definition hex_bits_17_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_17_matches_prefix s) with
           | Some ((g__63, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_17_backwards (s : string)
: M (mword 17) :=

   (match (hex_bits_17_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 17)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 353:2 - 355:3" >>= fun _ =>
          exit tt)
        : M (mword 17)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 353:2 - 355:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 17).

Definition hex_bits_18_forwards_matches (bv : mword 18)  : bool :=  true.

Definition hex_bits_18_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_18_matches_prefix s) with
           | Some ((g__62, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_18_backwards (s : string)
: M (mword 18) :=

   (match (hex_bits_18_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 18)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 372:2 - 374:3" >>= fun _ =>
          exit tt)
        : M (mword 18)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 372:2 - 374:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 18).

Definition hex_bits_19_forwards_matches (bv : mword 19)  : bool :=  true.

Definition hex_bits_19_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_19_matches_prefix s) with
           | Some ((g__61, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_19_backwards (s : string)
: M (mword 19) :=

   (match (hex_bits_19_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 19)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 391:2 - 393:3" >>= fun _ =>
          exit tt)
        : M (mword 19)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 391:2 - 393:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 19).

Definition hex_bits_20_forwards_matches (bv : mword 20)  : bool :=  true.

Definition hex_bits_20_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_20_matches_prefix s) with
           | Some ((g__60, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_20_backwards (s : string)
: M (mword 20) :=

   (match (hex_bits_20_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 20)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 410:2 - 412:3" >>= fun _ =>
          exit tt)
        : M (mword 20)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 410:2 - 412:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 20).

Definition hex_bits_21_forwards_matches (bv : mword 21)  : bool :=  true.

Definition hex_bits_21_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_21_matches_prefix s) with
           | Some ((g__59, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_21_backwards (s : string)
: M (mword 21) :=

   (match (hex_bits_21_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 21)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 429:2 - 431:3" >>= fun _ =>
          exit tt)
        : M (mword 21)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 429:2 - 431:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 21).

Definition hex_bits_22_forwards_matches (bv : mword 22)  : bool :=  true.

Definition hex_bits_22_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_22_matches_prefix s) with
           | Some ((g__58, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_22_backwards (s : string)
: M (mword 22) :=

   (match (hex_bits_22_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 22)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 448:2 - 450:3" >>= fun _ =>
          exit tt)
        : M (mword 22)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 448:2 - 450:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 22).

Definition hex_bits_23_forwards_matches (bv : mword 23)  : bool :=  true.

Definition hex_bits_23_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_23_matches_prefix s) with
           | Some ((g__57, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_23_backwards (s : string)
: M (mword 23) :=

   (match (hex_bits_23_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 23)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 467:2 - 469:3" >>= fun _ =>
          exit tt)
        : M (mword 23)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 467:2 - 469:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 23).

Definition hex_bits_24_forwards_matches (bv : mword 24)  : bool :=  true.

Definition hex_bits_24_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_24_matches_prefix s) with
           | Some ((g__56, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_24_backwards (s : string)
: M (mword 24) :=

   (match (hex_bits_24_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 24)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 486:2 - 488:3" >>= fun _ =>
          exit tt)
        : M (mword 24)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 486:2 - 488:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 24).

Definition hex_bits_25_forwards_matches (bv : mword 25)  : bool :=  true.

Definition hex_bits_25_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_25_matches_prefix s) with
           | Some ((g__55, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_25_backwards (s : string)
: M (mword 25) :=

   (match (hex_bits_25_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 25)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 505:2 - 507:3" >>= fun _ =>
          exit tt)
        : M (mword 25)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 505:2 - 507:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 25).

Definition hex_bits_26_forwards_matches (bv : mword 26)  : bool :=  true.

Definition hex_bits_26_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_26_matches_prefix s) with
           | Some ((g__54, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_26_backwards (s : string)
: M (mword 26) :=

   (match (hex_bits_26_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 26)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 524:2 - 526:3" >>= fun _ =>
          exit tt)
        : M (mword 26)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 524:2 - 526:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 26).

Definition hex_bits_27_forwards_matches (bv : mword 27)  : bool :=  true.

Definition hex_bits_27_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_27_matches_prefix s) with
           | Some ((g__53, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_27_backwards (s : string)
: M (mword 27) :=

   (match (hex_bits_27_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 27)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 543:2 - 545:3" >>= fun _ =>
          exit tt)
        : M (mword 27)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 543:2 - 545:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 27).

Definition hex_bits_28_forwards_matches (bv : mword 28)  : bool :=  true.

Definition hex_bits_28_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_28_matches_prefix s) with
           | Some ((g__52, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_28_backwards (s : string)
: M (mword 28) :=

   (match (hex_bits_28_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 28)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 562:2 - 564:3" >>= fun _ =>
          exit tt)
        : M (mword 28)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 562:2 - 564:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 28).

Definition hex_bits_29_forwards_matches (bv : mword 29)  : bool :=  true.

Definition hex_bits_29_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_29_matches_prefix s) with
           | Some ((g__51, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_29_backwards (s : string)
: M (mword 29) :=

   (match (hex_bits_29_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 29)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 581:2 - 583:3" >>= fun _ =>
          exit tt)
        : M (mword 29)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 581:2 - 583:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 29).

Definition hex_bits_30_forwards_matches (bv : mword 30)  : bool :=  true.

Definition hex_bits_30_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_30_matches_prefix s) with
           | Some ((g__50, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_30_backwards (s : string)
: M (mword 30) :=

   (match (hex_bits_30_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 30)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 600:2 - 602:3" >>= fun _ =>
          exit tt)
        : M (mword 30)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 600:2 - 602:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 30).

Definition hex_bits_31_forwards_matches (bv : mword 31)  : bool :=  true.

Definition hex_bits_31_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_31_matches_prefix s) with
           | Some ((g__49, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_31_backwards (s : string)
: M (mword 31) :=

   (match (hex_bits_31_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 31)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 619:2 - 621:3" >>= fun _ =>
          exit tt)
        : M (mword 31)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 619:2 - 621:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 31).

Definition hex_bits_32_forwards_matches (bv : mword 32)  : bool :=  true.

Definition hex_bits_32_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_32_matches_prefix s) with
           | Some ((g__48, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_32_backwards (s : string)
: M (mword 32) :=

   (match (hex_bits_32_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 32)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 638:2 - 640:3" >>= fun _ =>
          exit tt)
        : M (mword 32)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 638:2 - 640:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 32).

Definition hex_bits_33_forwards_matches (bv : mword 33)  : bool :=  true.

Definition hex_bits_33_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_33_matches_prefix s) with
           | Some ((g__47, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_33_backwards (s : string)
: M (mword 33) :=

   (match (hex_bits_33_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 33)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 657:2 - 659:3" >>= fun _ =>
          exit tt)
        : M (mword 33)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 657:2 - 659:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 33).

Definition hex_bits_48_forwards_matches (bv : mword 48)  : bool :=  true.

Definition hex_bits_48_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_48_matches_prefix s) with
           | Some ((g__46, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_48_backwards (s : string)
: M (mword 48) :=

   (match (hex_bits_48_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 48)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 676:2 - 678:3" >>= fun _ =>
          exit tt)
        : M (mword 48)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 676:2 - 678:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 48).

Definition hex_bits_64_forwards_matches (bv : mword 64)  : bool :=  true.

Definition hex_bits_64_backwards_matches (s : string)
: bool :=

   match s with
   | s =>
      if ((match (hex_bits_64_matches_prefix s) with
           | Some ((g__45, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_64_backwards (s : string)
: M (mword 64) :=

   (match (hex_bits_64_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 64)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 695:2 - 697:3" >>= fun _ =>
          exit tt)
        : M (mword 64)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 695:2 - 697:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 64).

Definition default_meta : mem_meta := tt.
Hint Unfold default_meta : sail.
Definition __WriteRAM_Meta (addr : mword 64) (width : Z) (meta : unit)
: M (unit) :=

   returnm (tt
    : unit).

Definition __ReadRAM_Meta (addr : mword 64) (width : Z)  : M (unit) :=  returnm (tt  : unit).

Definition write_ram
(wk : write_kind) (addr : mword 64) (width : Z) (data : mword (8 * width)) (meta : unit)
`{ArithFact (0 < width /\ width <= 16)}
: M (bool) :=

   (write_mem wk 64 addr width data) >>= fun ret : bool =>
   (if sumbool_of_bool (ret) then (__WriteRAM_Meta addr width meta)  : M (unit)
    else returnm (tt  : unit)) >>
   returnm (ret
    : bool).

Definition write_ram_ea (wk : write_kind) (addr : mword 64) (width : Z)
`{ArithFact (0 < width /\ width <= 16)}
: M (unit) :=

   (write_mem_ea wk 64 addr width)
    : M (unit).

Definition read_ram (rk : read_kind) (addr : mword 64) (width : Z)
`{ArithFact (0 < width /\ width <= 16)}
: M (mword (8 * width)) :=

   (read_mem rk 64 addr width)
    : M (mword (8 * width)).

Axiom __TraceMemoryWrite : forall {m : Z} (n : Z) (_ : mword m) (_ : mword (8 * n)) , unit.

Axiom __TraceMemoryRead : forall {m : Z} (n : Z) (_ : mword m) (_ : mword (8 * n)) , unit.

Definition regbits_to_regno (b : mword 5)
: {n : Z & ArithFact (0 <= n /\ n < 32)} :=

   build_ex(let 'r := projT1 (uint b) in
   r).

Definition rX (l__5 : Z) `{ArithFact (0 <= l__5 /\ l__5 < 32)}
: M (mword 64) :=

   (if sumbool_of_bool ((Z.eqb l__5 0)) then
      returnm ((EXTZ 64 (vec_of_bits [B0;B0;B0;B0]  : mword 4))
       : mword 64)
    else if sumbool_of_bool ((Z.gtb l__5 0)) then
      read_reg Xs_ref >>= fun w__0 : vec (mword 64) 32 =>
      returnm ((vec_access_dec w__0 l__5)
       : mword 64)
    else
      assert_exp' false "Pattern match failure at model/riscv_duopod.sail 22:0 - 23:27" >>= fun _ =>
      exit tt)
    : M (mword 64).

Definition wX (r : Z) (v : mword 64) `{ArithFact (0 <= r /\ r < 32)}
: M (unit) :=

   (if sumbool_of_bool ((projT1 (neq_int r 0))) then
      read_reg Xs_ref >>= fun w__0 : vec (mword 64) 32 =>
      write_reg Xs_ref (vec_update_dec w__0 r v)
       : M (unit)
    else returnm (tt  : unit))
    : M (unit).

Definition read_mem (addr : mword 64) (width : Z) `{ArithFact (width >= 0)}
: M (mword (8 * width)) :=

   (MEMr 64 width (EXTZ 64 (vec_of_bits [B0;B0;B0;B0]  : mword 4)) addr)
    : M (mword (8 * width)).

Definition iop_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 5)}
: iop :=

   let l__0 := arg_ in
   if sumbool_of_bool ((Z.eqb l__0 0)) then RISCV_ADDI
   else if sumbool_of_bool ((Z.eqb l__0 1)) then RISCV_SLTI
   else if sumbool_of_bool ((Z.eqb l__0 2)) then RISCV_SLTIU
   else if sumbool_of_bool ((Z.eqb l__0 3)) then RISCV_XORI
   else if sumbool_of_bool ((Z.eqb l__0 4)) then RISCV_ORI
   else RISCV_ANDI.

Definition num_of_iop (arg_ : iop)
: {e : Z & ArithFact (0 <= e /\ e <= 5)} :=

   build_ex(match arg_ with
            | RISCV_ADDI => 0
            | RISCV_SLTI => 1
            | RISCV_SLTIU => 2
            | RISCV_XORI => 3
            | RISCV_ORI => 4
            | RISCV_ANDI => 5
            end).

Definition execute_LOAD (imm : mword 12) (rs1 : mword 5) (rd : mword 5)
: M (unit) :=

   (rX (projT1 (regbits_to_regno rs1))) >>= fun w__0 : mword 64 =>
   let addr : xlenbits := add_vec w__0 (EXTS 64 imm) in
   (read_mem addr 8) >>= fun result : xlenbits =>
   (wX (projT1 (regbits_to_regno rd)) result)
    : M (unit).

Definition execute_ITYPE (arg0 : mword 12) (arg1 : mword 5) (arg2 : mword 5) (arg3 : iop)
: M (unit) :=

   let merge_var := (arg0, arg1, arg2, arg3) in
   (match merge_var with
    | (imm, rs1, rd, RISCV_ADDI) =>
       (rX (projT1 (regbits_to_regno rs1))) >>= fun rs1_val =>
       let imm_ext : xlenbits := EXTS 64 imm in
       let result := add_vec rs1_val imm_ext in
       (wX (projT1 (regbits_to_regno rd)) result)
        : M (unit)
    | _ => exit tt  : M (unit)
    end)
    : M (unit).

Definition execute (merge_var : ast)
: M (unit) :=

   (match merge_var with
    | ITYPE ((imm, rs1, rd, arg3)) => (execute_ITYPE imm rs1 rd arg3)  : M (unit)
    | LOAD ((imm, rs1, rd)) => (execute_LOAD imm rs1 rd)  : M (unit)
    end)
    : M (unit).

Definition decode (v__0 : mword 32)
: option ast :=

   if ((andb (eq_vec (subrange_vec_dec v__0 14 12) (vec_of_bits [B0;B0;B0]  : mword (14 - 12 + 1)))
          (eq_vec (subrange_vec_dec v__0 6 0)
             (vec_of_bits [B0;B0;B1;B0;B0;B1;B1]  : mword (6 - 0 + 1))))) then
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     let rs1 : regbits := subrange_vec_dec v__0 19 15 in
     let rd : regbits := subrange_vec_dec v__0 11 7 in
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     Some
       (ITYPE
          ((imm, rs1, rd, RISCV_ADDI)))
   else if ((andb
               (eq_vec (subrange_vec_dec v__0 14 12) (vec_of_bits [B0;B1;B1]  : mword (14 - 12 + 1)))
               (eq_vec (subrange_vec_dec v__0 6 0)
                  (vec_of_bits [B0;B0;B0;B0;B0;B1;B1]  : mword (6 - 0 + 1))))) then
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     let rs1 : regbits := subrange_vec_dec v__0 19 15 in
     let rd : regbits := subrange_vec_dec v__0 11 7 in
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     Some
       (LOAD
          ((imm, rs1, rd)))
   else None.

Definition initial_regstate : regstate :=
{| Xs :=
     (vec_of_list_len [(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0]
                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0]
                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0]
                                                     : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0]
                                                                   : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);
                       (vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0]
                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0]
                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0]
                                                     : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0]
                                                                   : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                B0]
                                                                                : mword 64)]);
   nextPC :=
     (vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0]
       : mword 64);
   PC :=
     (vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0]
       : mword 64) |}.
Hint Unfold initial_regstate : sail.

End Content.

author: danceos

repo: sail-riscv

save_path: github-repos/coq/danceos-sail-riscv


text:
(** * Pushouts from coequalizers and bincoproducts

The pushout
<<
A ---> B
|
|
|
V
C
>>
is defined as the coequalizer of
<<
A --> B + C
>>

 *)
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.limits.pushouts.
Require Import UniMath.CategoryTheory.limits.initial.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.equalizers.
Require Import UniMath.CategoryTheory.limits.graphs.coequalizers.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.pushouts.

Local Open Scope cat.
Section d.
  Context {C : category} {g : graph}
          (bc : BinCoproducts C)
          (coeq : Coequalizers C).

  Definition pushouts_from_coeq_bincoprod : Pushouts C.
    intros a b c u v.
    use make_Pushout.
    - unshelve eapply CoequalizerObject; revgoals.
      + red in coeq.
        specialize (coeq a (bc b c)).
        apply coeq.
      + eapply compose; [exact v|apply BinCoproductIn2].
      + eapply compose; [exact u|apply BinCoproductIn1].
    - cbn.
      eapply compose;[apply BinCoproductIn1|apply CoequalizerArrow].
    - cbn.
      eapply compose;[apply BinCoproductIn2|apply CoequalizerArrow].
    - cbn.
      repeat rewrite assoc.
      apply CoequalizerArrowEq.
    - intros e h k eq.
      cbn.
      use unique_exists.
      + use CoequalizerOut.
        * apply BinCoproductArrow; assumption.
        * do 2 rewrite <- assoc.
          rewrite BinCoproductIn1Commutes,BinCoproductIn2Commutes.
          exact eq.
      + split.
        * etrans.
          { etrans;[apply pathsinv0,assoc|].
            apply cancel_precomposition.
            apply CoequalizerArrowComm.
          }
          apply BinCoproductIn1Commutes.
        * etrans.
          { etrans;[apply pathsinv0,assoc|].
            apply cancel_precomposition.
            apply CoequalizerArrowComm.
          }
          apply BinCoproductIn2Commutes.
      + cbn -[isaprop].
        intros.
        apply isapropdirprod; apply homset_property.
      + cbn.
        intros w eq'.
        apply CoequalizerOutUnique.
        apply BinCoproductArrowUnique.
        * etrans;[apply assoc|exact (pr1 eq')].
        * etrans;[apply assoc|exact (pr2 eq')].
  Defined.

End d.

author: UniMath

repo: largecatmodules


text:
(* Time-stamp: "2018-02-08 18:18:31 pierre" *)
(****************************************************************)
(*                      finite_Horizon.v                        *)
(*                                                              *)
(**          © Pierre Lescanne  (December 2015)                 *)
(*                                                              *)
(*              LIP (ENS-Lyon, CNRS, INRIA)                     *)
(*                                                              *)
(*                                                              *)
(*  Developed in  V8.4pl4              January May 20016        *)
(****************************************************************)
Section FiniteHistory.

Add LoadPath ".".

Require Import games_Choice_Dependent.

Inductive AliceBob : Set := Alice | Bob.
Definition Choice :(AliceBob -> Set) :=
  fun a:AliceBob  => match a with Alice => nat | Bob => unit end.
(* Utility is unit *)

Notation "<| f |>" := (gLeaf AliceBob unit Choice f).
Notation "<| a , next |>" := (gNode AliceBob unit Choice a next).

(* A finite threadlike game of length n *)
Fixpoint  ThreadlikeGame (n:nat): (Game AliceBob unit Choice) :=
  match n with
    | 0 => <|fun (a:AliceBob) => match a with | Alice => tt
                                              | Bob => tt end|>
    | (S n) => <|Bob,fun c:Choice Bob
                     => match c with tt=>ThreadlikeGame n end|>
  end.

(* A game with a finite horizon *)
Definition GameWFH:(Game AliceBob unit Choice)  :=
  <| Alice, fun n:Choice Alice => ThreadlikeGame n |>.

Proposition FiniteHistoryGameWFH: FiniteHistoryGame AliceBob unit Choice GameWFH.
Proof.
  unfold GameWFH; apply finHorGNode; intro; elim c';
  [apply finHorGLeaf |
   intros; apply finHorGNode; induction c'0; assumption].
Qed.

End FiniteHistory.

author: PierreLescanne

repo: DependentTypesForExtensiveGames


text:
Require Import Program.Tactics.
Require Import Program.

Require Import TypeSyntax TypeSpec.

Require Import Lemmas_subtype Lemmas_abstrstate_order.

Section LEMMA_4_6.
    Variable C : constraints.
    Variables T T1 T2 : annotatedtype.
    Variables D1 D2 : lockenv.

    Lemma Lemma_4_6:
        subtype C T (at_Arrow T1 (EffectIntro D1 D2) T2) ->

        exists T1' T2' D1' D2',
            T = (at_Arrow T1' (EffectIntro D1' D2') T2') /\
            subtype C T1 T1' /\
            subtype C T2' T2 /\
            abstrstate_order C D1 D1' /\
            abstrstate_order C D2' D2.

    Proof.
        Local Hint Constructors subtype abstrstate_order.
        intro H; dependent induction H.
        - do 4 eexists; eauto.
        - destruct IHsubtype2 as [T1' [T2' [D1' [D2' IH2]]]].
          specialize (IHsubtype1 T1' T2' D1' D2' (proj1 IH2)).
          destruct IHsubtype1 as [T1'' [T2'' [D1'' [D2'' IH1]]]].
          exists T1'' T2'' D1'' D2'';
            intuition; eauto using subtype_trans, abstrstate_order_trans.
        - exists AT_1 AT_2 D_1 D_2; intuition.
    Qed.

End LEMMA_4_6.

author: peterbb

repo: formal-dlraces

save_path: github-repos/coq/peterbb-formal-dlraces


text:
(*** Introduction to Computational Logic, Coq part of Assignment 11 ***)

Require Import List.
Import ListNotations.
Notation "x 'el' A" := (In x A) (at level 70).
Notation "x 'nel' A" := (~ In x A) (at level 70).
Require Import Lia.
From Equations Require Import Equations.
Definition dec X := {X} + {~X}.

(*** Exercise 11.2 ***)

Section Basics.

  Variable X : Type.
  Implicit Types (x y z : X) (A B C : list X).

  Lemma disjointness x A :
    x::A <> nil.
  Proof.
    discriminate.
  Qed.

  Lemma injectivity x y A B :
    x::A = y::B -> x = y /\ A = B.
  Proof.
    now intros [= H].
  Qed.

  Lemma progression x A :
    x::A <> A.
  Proof.
    induction A as [|y A IH].
    - intros [= H].
    - intros [= <- H]. auto.
  Qed.

  Lemma associativity A B C :
    (A ++ B) ++ C = A ++ (B ++ C).
  Proof.
    induction A as [|x A IH].
    - reflexivity.
    - cbn. now rewrite IH.
  Qed.

  Lemma length_add A B :
    length (A ++ B) = length A + length B.
  Proof.
    induction A as [|x A IH]; cbn.
    - reflexivity.
    - now rewrite IH.
  Qed.

End Basics.

(*** Exercise 11.3 ***)

Definition match_list X (p : list X -> Type) :
  p [] -> (forall x A, p (x :: A)) -> forall A, p A :=
  fun a f A => match A with [] => a | (x :: A) => f x A end.

Definition elim_list X (p : list X -> Type) :
  p [] -> (forall x A, p A -> p (x :: A)) -> forall A, p A :=
  fun a f => fix F A := match A with [] => a | (x :: A) => f x A (F A) end.

Definition match_list' X (p : list X -> Type) :
  p [] -> (forall x A, p (x :: A)) -> forall A, p A :=
  fun a f => elim_list X p a (fun x A _ => f x A).

(*** Exercise 11.4 ***)

Section Membership.

  Variable X : Type.
  Implicit Types (x y z : X) (A B C : list X).

  Inductive mem x : list X -> Prop :=
  | memB A : mem x (x::A)
  | memC y A : mem x A -> mem x (y::A).

  Goal forall x A, x el A <-> mem x A.
  Proof.
    split.
    - induction A as [|y A IH]; cbn.
      + now intros.
      + intros [H|H].
        * rewrite H. constructor.
        * constructor. apply IH, H.
    - intros H. induction H; cbn.
      + now left.
      + now right.
  Qed.

  Goal forall x A, x el A <-> exists A1 A2, A = A1 ++ x::A2.
  Proof.
    intros x A. split.
    - induction A as [|y A IH]; cbn.
      + now intros H.
      + intros [->|H].
        * now exists [], A.
        * apply IH in H. destruct H as [A1 [A2 ->]]. now exists (y :: A1), A2.
    - intros [A1 [A2 ->]]. induction A1 as [|y A1 IH]; cbn.
      + now left.
      + now right.
  Qed.

End Membership.

(*** Exercise 11.5 ***)

Section Decidability.

  Variable X : Type.
  Implicit Types (x y z : X) (A B C : list X).

  Lemma dec_eq A B (d : forall x y, dec (x = y)) :
    dec (A = B).
  Proof.
    induction A as [|x A IH] in B |-*; cbn.
    - destruct B.
      + now left.
      + right. discriminate.
    - destruct B.
      + right. discriminate.
      + specialize (IH B) as [<-|IH].
        * specialize (d x x0) as [<-|H].
          -- now left.
          -- right. contradict H. now injection H.
        * right. contradict IH. now injection IH.
  Qed.

  Lemma dec_mem x A (d : forall x y, dec (x = y)) :
    dec (x el A).
  Proof.
    induction A as [|y A IH] in x |-*; cbn.
    - now right.
    - specialize (IH x) as [IH|IH].
      + left. now right.
      + specialize (d x y) as [d|d].
        * left. now left.
        * right. intros [H|H].
          -- now apply d.
          -- now apply IH.
  Qed.

  Lemma dec_forall A f :
    dec (forall x, x el A -> f x = true).
  Proof.
    induction A as [|y A [IH|IH]].
    - now left.
    - destruct (f y) eqn:H.
      + left. intros x [H2|H2].
        * now rewrite <- H2.
        * now apply IH.
      + right. intros H2. specialize (H2 y). assert (y el y :: A) by (now left).
        apply H2 in H0. congruence.
    - right. contradict IH. intros x H. apply IH. now right.
  Qed.

  Lemma dec_exists A f :
    dec (exists x, x el A /\ f x = true).
  Proof.
    induction A as [|y A [IH|IH]].
    - right. now intros [x [H1 H2]].
    - destruct (f y) eqn:H.
      + left. destruct IH as [x [IH1 IH2]]. exists x. split.
        * now right.
        * exact IH2.
      + left. destruct IH as [x [IH1 IH2]]. exists x. split.
        * now right.
        * exact IH2.
    - destruct (f y) eqn:H.
      + left. exists y. split.
        * now left.
        * exact H.
      + right. contradict IH. destruct IH as [x [IH1 IH2]]. exists x. split.
        * destruct IH1 as [IH1|IH1].
          -- rewrite IH1 in H. congruence.
          -- exact IH1.
        * exact IH2.
  Qed.

End Decidability.

(*** Exercise 11.6 ***)

Goal (forall X, list X -> nat -> X) -> False.
Proof.
  intros H. specialize (H False). apply (H [] 0).
Qed.

(*** Exercise 11.7 ***)

Section Subscript.

  Variable X : Type.
  Implicit Types (x y z : X) (A B C : list X).

  Fixpoint sub A n : option X :=
    match A, n with
    | [], _ => None
    | x::A, 0 => Some x
    | x::A, S n => sub A n
    end.

  Arguments sub : simpl nomatch.

  Lemma opt_inject x y :
    Some x = Some y -> x = y.
  Proof.
    now intros [= H].
  Qed.

  Lemma sub_mem x A :
    x el A <-> exists n, sub A n = Some x.
  Proof.
    split.
    - induction A as [|y A IH].
      + now cbn.
      + intros [H|H].
        * exists 0. cbn. now rewrite H.
        * specialize (IH H) as [n IH]. exists (S n). now cbn.
    - intros [n H]. induction A as [|y A IH] in n,H |-*; cbn.
      + discriminate.
      + destruct n.
        * left. cbn in H. now apply opt_inject.
        * right. apply (IH n). now cbn in H.
  Qed.

  Lemma sub_le n A :
    n < length A <-> exists x, sub A n = Some x.
  Proof.
    split.
    - intros H. induction A as [|y A IH] in n,H |-*; cbn.
      + cbn in H. lia.
      + destruct n.
        * now exists y.
        * destruct (IH n).
          -- cbn in H. lia.
          -- exists x. now cbn.
    - intros [x H]. induction A as [|y A IH] in n,H |-*; cbn.
      + discriminate.
      + destruct n.
        * lia.
        * apply Lt.lt_n_S, (IH n). now cbn in H.
  Qed.

End Subscript.

(*** Exercise 11.8 ***)

Section Inclusion.

  Variable X : Type.
  Implicit Types (x y z : X) (A B C : list X).

  Notation "A <<= B" := (incl A B) (at level 70).
  Notation "A == B" := (A <<= B /\ B <<= A) (at level 70).

  Goal forall A, A <<= [] <-> A = [].
  Proof.
    intros A. split.
    - intros H. induction A as [|y A IH]; cbn.
      + reflexivity.
      + unfold incl in H. specialize (H y). exfalso. apply H. now left.
    - intros H. unfold incl. intros a H2. now rewrite H in H2.
  Qed.

  Goal forall x A B, A <<= B -> x::A <<= x::B.
  Proof.
    unfold incl. intros x A B.
    intros H a [H2|H2].
    - now left.
    - specialize (H a H2). now right.
  Qed.

  Goal forall x A, x el A -> A == x::A.
  Proof.
    intros x A H. split.
    - unfold incl. intros a H2. cbn. now right.
    - unfold incl. intros a [H2|H2].
      + now rewrite <- H2.
      + exact H2.
  Qed.

  Goal forall x A B, A == B -> x::A == x::B.
  Proof.
    unfold incl.
    intros x A B [H1 H2]. split; intros a [H|H].
    - now left.
    - specialize (H1 a H). now right.
    - now left.
    - specialize (H2 a H). now right.
  Qed.

End Inclusion.

(*** Exercise 11.9 ***)

Section Repeating.

  Variable X : Type.
  Implicit Types (x y z : X) (A B C : list X).

  Inductive rep : list X -> Prop :=
  | repB x A : x el A -> rep (x::A)
  | repS x A : rep A -> rep (x::A).

  Inductive nrep : list X -> Prop :=
  | nrepN : nrep nil
  | nrepC x A : x nel A -> nrep A -> nrep (x::A).

  Derive Signature for rep nrep.

  Goal forall x A, rep (x::A) -> x el A \/ rep A.
  Proof.
    intros x A H. inversion H.
    - now left.
    - now right.
  Qed.

  Goal forall x A, rep (x::A) -> x el A \/ rep A.
  Proof.
    intros x A H. depelim H.
    - now left.
    - now right.
  Qed.

  Goal forall x A, nrep (x::A) -> x nel A /\ nrep A.
  Proof.
    intros x A H. inversion H. split; auto.
  Qed.

  Goal forall x A, nrep (x::A) -> x nel A /\ nrep A.
  Proof.
    intros x A H. depelim H. split; auto.
  Qed.

  Lemma el_ex : forall x A, x el A -> exists A1 A2, A = A1 ++ x::A2.
  Proof.
    induction A as [|y A IH]; cbn.
    - now intros H.
    - intros [->|H].
      + now exists [], A.
      + apply IH in H. destruct H as [A1 [A2 ->]]. now exists (y :: A1), A2.
  Qed.

  Goal forall x A, rep A -> exists x A1 A2 A3, A = A1 ++ (x :: A2) ++ (x :: A3).
  Proof.
    intros x A H. induction H.
    - apply el_ex in H as [A1 [A2 ->]]. now exists x0, [], A1, A2.
    - destruct IHrep as [y [A1 [A2 [A3 H2]]]]. exists y, (x0 :: A1), A2, A3. now rewrite H2.
  Qed.

(*** Exercise 11.10 ***)

  Hypothesis d : forall x y, dec (x = y).

  Fixpoint card A : nat :=
    match A with
    | [] => 0
    | x:: A' => if dec_mem _ x A' d then card A' else S (card A')
    end.

  Fact card_length A :
    card A <= length A.
  Proof.
    induction A as [|x A IH]; cbn.
    - lia.
    - destruct (dec_mem _ x A d) as [H|H]; lia.
  Qed.

  Fact rep_card_length A :
    rep A <-> card A < length A.
  Proof.
    split.
    - intros H. depelim H; cbn.
      + destruct (dec_mem _ x A d) as [H1|H1]; cbn.
        * apply le_n_S, card_length.
        * congruence.
      + destruct (dec_mem _ x A d) as [H1|H1]; cbn.
        * apply le_n_S, card_length.
        * Admitted.

  Fact nrep_card_length A :
    nrep A <-> card A = length A.
  Proof.
    split.
    - intros H. depelim H.
      + reflexivity.
      + induction A as [|y A IH]; cbn.
        * destruct (dec_mem _ x [] d) as [H1|H1]; cbn.
          -- congruence.
          -- reflexivity.
        * destruct (dec_mem _ x (y :: A)) as [H1|H1]; cbn.
          -- Admitted.

End Repeating.

(*** Exercise 11.11 ***)

Lemma partition_dec (P Q : Prop) :
  (P -> Q -> False) -> (P + Q) -> (dec P) * (P <-> ~ Q).
Proof.
  intros H [H1|H1].
  - split.
    + now left.
    + tauto.
  - split.
    + right. intros H2. now apply H.
    + tauto.
Qed.

(*** Exercise 11.12 ***)

(* Define sum and formulate and prove the pigeon hole principle. *)

Fixpoint sum A : nat :=
  match A with
  | nil => 0
  | x :: A => x + sum A
  end.

Lemma pigeonhole (A : list nat) :
  sum A > length A -> exists x, x el A /\ x >= 2.
Proof.
  intros H. induction A as [|y A IH] in H |-*; cbn.
  - now cbn.
  - exists y. split.
    + now left.
    + Admitted.

(*** Exercise 11.13 ***)

(* Formulate and prove the realistic drinker paradox. *)

(*** Exercise 11.14 ***)

(* Define map and filter and formulate and prove their specs. *)

Fixpoint map X Y (f : X -> Y) (A : list X) : list Y :=
  match A with
  | nil => nil
  | x :: A => f x :: map X Y f A
  end.

Lemma map_spec X Y f y A :
  y el (map X Y f A) <-> exists x, x el A /\ f x = y.
Proof.
  split.
  - induction A as [|z A IH]; cbn.
    + now intros.
    + intros [H|H].
      * exists z; auto.
      * specialize (IH H). destruct IH as [x [IH1 IH2]]. exists x; auto.
  - intros [x [H1 H2]]. induction A as [|z A IH]; cbn.
    + exact H1.
    + destruct H1 as [H1|H1].
      * left. now rewrite H1.
      * specialize (IH H1). now right.
Qed.

Fixpoint filter X (f : X -> bool) (A : list X) : list X :=
  match A with
  | nil => nil
  | x :: A => if f x then x :: filter X f A else filter X f A
  end.

Lemma filter_spec X f A :
  forall y, y el (filter X f A) <-> y el A /\ f y = true.
Proof.
  intros y. split.
  - induction A as [|x A IH] in y |-*; cbn.
    + now intros.
    + intros H. split.
      * destruct (f x).
        -- Admitted.

author: archbung