From f80784d0aaba88c1f5bd078b1d7bbe60e05424b0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 14 May 2018 13:29:15 +0100 Subject: Add missing HOL4 files (and disable overzealous cleaning) --- snapshots/hol4/sail/lib/hol/Holmakefile | 2 +- snapshots/hol4/sail/lib/hol/promptScript.sml | 15 + snapshots/hol4/sail/lib/hol/prompt_monadScript.sml | 24 + .../hol4/sail/lib/hol/sail_instr_kindsScript.sml | 473 ++++++++ .../hol4/sail/lib/hol/sail_operatorsScript.sml | 367 ++++++ .../sail/lib/hol/sail_operators_bitlistsScript.sml | 792 +++++++++++++ .../sail/lib/hol/sail_operators_mwordsScript.sml | 612 ++++++++++ snapshots/hol4/sail/lib/hol/sail_valuesScript.sml | 1238 ++++++++++++++++++++ snapshots/hol4/sail/lib/hol/stateScript.sml | 119 ++ snapshots/hol4/sail/lib/hol/state_monadScript.sml | 348 ++++++ 10 files changed, 3989 insertions(+), 1 deletion(-) create mode 100644 snapshots/hol4/sail/lib/hol/promptScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/prompt_monadScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/sail_valuesScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/stateScript.sml create mode 100644 snapshots/hol4/sail/lib/hol/state_monadScript.sml (limited to 'snapshots') diff --git a/snapshots/hol4/sail/lib/hol/Holmakefile b/snapshots/hol4/sail/lib/hol/Holmakefile index 45ed41ff..d7df9bcb 100644 --- a/snapshots/hol4/sail/lib/hol/Holmakefile +++ b/snapshots/hol4/sail/lib/hol/Holmakefile @@ -2,7 +2,7 @@ SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript. sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml -EXTRA_CLEANS = $(SCRIPTS) +#EXTRA_CLEANS = $(SCRIPTS) THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) diff --git a/snapshots/hol4/sail/lib/hol/promptScript.sml b/snapshots/hol4/sail/lib/hol/promptScript.sml new file mode 100644 index 00000000..95d6e752 --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/promptScript.sml @@ -0,0 +1,15 @@ +(*Generated by Lem from prompt.lem.*) +open HolKernel Parse boolLib bossLib; +open prompt_monadTheory state_monadTheory stateTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "prompt" + +(*open import Prompt_monad*) +(*open import State_monad*) +(*open import State*) +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/prompt_monadScript.sml b/snapshots/hol4/sail/lib/hol/prompt_monadScript.sml new file mode 100644 index 00000000..627620ff --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/prompt_monadScript.sml @@ -0,0 +1,24 @@ +(*Generated by Lem from prompt_monad.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory sail_valuesTheory sail_instr_kindsTheory state_monadTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "prompt_monad" + +(*open import Pervasives_extra*) +(*open import Sail_instr_kinds*) +(*open import Sail_values*) +(*open import State_monad*) + +(* Fake interface of the prompt monad by redirecting to the state monad, since + the former is not currently supported by HOL4 *) + +val _ = type_abbrev((* ( 'a_rv, 'b_a, 'c_e) *) "monad" , ``:('a_rv,'b_a,'c_e) state_monad$monadS``); +val _ = type_abbrev((* ( 'a_rv, 'b_a, 'c_e, 'd_r) *) "monadR" , ``:('a_rv,'b_a,'c_e,'d_r) state_monad$monadRS``); +val _ = Define ` + ((barrier:'c -> 'a state_monad$sequential_state ->(((unit),'b)state_monad$result#'a state_monad$sequential_state)set) _= (returnS () ))`; +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml b/snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml new file mode 100644 index 00000000..cfe0ac60 --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml @@ -0,0 +1,473 @@ +(*Generated by Lem from ../../src/lem_interp/sail_instr_kinds.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "sail_instr_kinds" + +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +(*open import Pervasives_extra*) + + +val _ = Hol_datatype ` +(* 'a *) EnumerationType_class= <| + toNat_method : 'a -> num +|>`; + + + +(*val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> Basic_classes.ordering*) +val _ = Define ` + ((enumeration_typeCompare:'a EnumerationType_class -> 'a -> 'a -> lem_basic_classes$ordering)dict_Sail_instr_kinds_EnumerationType_a e1 e2= +(genericCompare (<) (=) ( + dict_Sail_instr_kinds_EnumerationType_a.toNat_method e1) (dict_Sail_instr_kinds_EnumerationType_a.toNat_method e2)))`; + + + +val _ = Define ` +((instance_Basic_classes_Ord_var_dict:'a EnumerationType_class -> 'a lem_basic_classes$Ord_class)dict_Sail_instr_kinds_EnumerationType_a= (<| + + compare_method := + (enumeration_typeCompare dict_Sail_instr_kinds_EnumerationType_a); + + isLess_method := (\ r1 r2. (enumeration_typeCompare + dict_Sail_instr_kinds_EnumerationType_a r1 r2) = LT); + + isLessEqual_method := (\ r1 r2. (enumeration_typeCompare + dict_Sail_instr_kinds_EnumerationType_a r1 r2) <> GT); + + isGreater_method := (\ r1 r2. (enumeration_typeCompare + dict_Sail_instr_kinds_EnumerationType_a r1 r2) = GT); + + isGreaterEqual_method := (\ r1 r2. (enumeration_typeCompare + dict_Sail_instr_kinds_EnumerationType_a r1 r2) <> LT)|>))`; + + + +(* Data structures for building up instructions *) + +(* careful: changes in the read/write/barrier kinds have to be + reflected in deep_shallow_convert *) +val _ = Hol_datatype ` + read_kind = + (* common reads *) + Read_plain + (* Power reads *) + | Read_reserve + (* AArch64 reads *) + | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream + (* RISC-V reads *) + | Read_RISCV_acquire | Read_RISCV_strong_acquire + | Read_RISCV_reserved | Read_RISCV_reserved_acquire + | Read_RISCV_reserved_strong_acquire + (* x86 reads *) + | Read_X86_locked`; + (* the read part of a lock'd instruction (rmw) *) + +val _ = Define ` +((instance_Show_Show_Sail_instr_kinds_read_kind_dict:(read_kind)lem_show$Show_class)= (<| + + show_method := (\x . + (case x of + Read_plain => "Read_plain" + | Read_reserve => "Read_reserve" + | Read_acquire => "Read_acquire" + | Read_exclusive => "Read_exclusive" + | Read_exclusive_acquire => "Read_exclusive_acquire" + | Read_stream => "Read_stream" + | Read_RISCV_acquire => "Read_RISCV_acquire" + | Read_RISCV_strong_acquire => "Read_RISCV_strong_acquire" + | Read_RISCV_reserved => "Read_RISCV_reserved" + | Read_RISCV_reserved_acquire => "Read_RISCV_reserved_acquire" + | Read_RISCV_reserved_strong_acquire => "Read_RISCV_reserved_strong_acquire" + | Read_X86_locked => "Read_X86_locked" + ))|>))`; + + +val _ = Hol_datatype ` + write_kind = + (* common writes *) + Write_plain + (* Power writes *) + | Write_conditional + (* AArch64 writes *) + | Write_release | Write_exclusive | Write_exclusive_release + (* RISC-V *) + | Write_RISCV_release | Write_RISCV_strong_release + | Write_RISCV_conditional | Write_RISCV_conditional_release + | Write_RISCV_conditional_strong_release + (* x86 writes *) + | Write_X86_locked`; + (* the write part of a lock'd instruction (rmw) *) + +val _ = Define ` +((instance_Show_Show_Sail_instr_kinds_write_kind_dict:(write_kind)lem_show$Show_class)= (<| + + show_method := (\x . + (case x of + Write_plain => "Write_plain" + | Write_conditional => "Write_conditional" + | Write_release => "Write_release" + | Write_exclusive => "Write_exclusive" + | Write_exclusive_release => "Write_exclusive_release" + | Write_RISCV_release => "Write_RISCV_release" + | Write_RISCV_strong_release => "Write_RISCV_strong_release" + | Write_RISCV_conditional => "Write_RISCV_conditional" + | Write_RISCV_conditional_release => "Write_RISCV_conditional_release" + | Write_RISCV_conditional_strong_release => "Write_RISCV_conditional_strong_release" + | Write_X86_locked => "Write_X86_locked" + ))|>))`; + + +val _ = Hol_datatype ` + barrier_kind = + (* Power barriers *) + Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + (* AArch64 barriers *) + | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB + | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB + | Barrier_TM_COMMIT + (* MIPS barriers *) + | Barrier_MIPS_SYNC + (* RISC-V barriers *) + | Barrier_RISCV_rw_rw + | Barrier_RISCV_r_rw + | Barrier_RISCV_r_r + | Barrier_RISCV_rw_w + | Barrier_RISCV_w_w + | Barrier_RISCV_i + (* X86 *) + | Barrier_x86_MFENCE`; + + + +val _ = Define ` +((instance_Show_Show_Sail_instr_kinds_barrier_kind_dict:(barrier_kind)lem_show$Show_class)= (<| + + show_method := (\x . + (case x of + Barrier_Sync => "Barrier_Sync" + | Barrier_LwSync => "Barrier_LwSync" + | Barrier_Eieio => "Barrier_Eieio" + | Barrier_Isync => "Barrier_Isync" + | Barrier_DMB => "Barrier_DMB" + | Barrier_DMB_ST => "Barrier_DMB_ST" + | Barrier_DMB_LD => "Barrier_DMB_LD" + | Barrier_DSB => "Barrier_DSB" + | Barrier_DSB_ST => "Barrier_DSB_ST" + | Barrier_DSB_LD => "Barrier_DSB_LD" + | Barrier_ISB => "Barrier_ISB" + | Barrier_TM_COMMIT => "Barrier_TM_COMMIT" + | Barrier_MIPS_SYNC => "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw => "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw => "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r => "Barrier_RISCV_r_r" + | Barrier_RISCV_rw_w => "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w => "Barrier_RISCV_w_w" + | Barrier_RISCV_i => "Barrier_RISCV_i" + | Barrier_x86_MFENCE => "Barrier_x86_MFENCE" + ))|>))`; + + +val _ = Hol_datatype ` + trans_kind = + (* AArch64 *) + Transaction_start | Transaction_commit | Transaction_abort`; + + +val _ = Define ` +((instance_Show_Show_Sail_instr_kinds_trans_kind_dict:(trans_kind)lem_show$Show_class)= (<| + + show_method := (\x . + (case x of + Transaction_start => "Transaction_start" + | Transaction_commit => "Transaction_commit" + | Transaction_abort => "Transaction_abort" + ))|>))`; + + +val _ = Hol_datatype ` + instruction_kind = + IK_barrier of barrier_kind + | IK_mem_read of read_kind + | IK_mem_write of write_kind + | IK_mem_rmw of (read_kind # write_kind) + | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), + indirect/computed-branch (single nia of kind NIA_indirect_address) + and branch/jump (single nia of kind NIA_concrete_address) *) + | IK_trans of trans_kind + | IK_simple`; + + + +val _ = Define ` +((instance_Show_Show_Sail_instr_kinds_instruction_kind_dict:(instruction_kind)lem_show$Show_class)= (<| + + show_method := (\x . + (case x of + IK_barrier barrier_kind => STRCAT "IK_barrier " + (((\x . (case x of + Barrier_Sync => "Barrier_Sync" + | Barrier_LwSync => "Barrier_LwSync" + | Barrier_Eieio => "Barrier_Eieio" + | Barrier_Isync => "Barrier_Isync" + | Barrier_DMB => "Barrier_DMB" + | Barrier_DMB_ST => "Barrier_DMB_ST" + | Barrier_DMB_LD => "Barrier_DMB_LD" + | Barrier_DSB => "Barrier_DSB" + | Barrier_DSB_ST => "Barrier_DSB_ST" + | Barrier_DSB_LD => "Barrier_DSB_LD" + | Barrier_ISB => "Barrier_ISB" + | Barrier_TM_COMMIT => + "Barrier_TM_COMMIT" + | Barrier_MIPS_SYNC => + "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw => + "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw => + "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r => + "Barrier_RISCV_r_r" + | Barrier_RISCV_rw_w => + "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w => + "Barrier_RISCV_w_w" + | Barrier_RISCV_i => + "Barrier_RISCV_i" + | Barrier_x86_MFENCE => + "Barrier_x86_MFENCE" + )) barrier_kind)) + | IK_mem_read read_kind => STRCAT "IK_mem_read " + (((\x . (case x of + Read_plain => "Read_plain" + | Read_reserve => "Read_reserve" + | Read_acquire => "Read_acquire" + | Read_exclusive => "Read_exclusive" + | Read_exclusive_acquire => + "Read_exclusive_acquire" + | Read_stream => "Read_stream" + | Read_RISCV_acquire => "Read_RISCV_acquire" + | Read_RISCV_strong_acquire => + "Read_RISCV_strong_acquire" + | Read_RISCV_reserved => + "Read_RISCV_reserved" + | Read_RISCV_reserved_acquire => + "Read_RISCV_reserved_acquire" + | Read_RISCV_reserved_strong_acquire => + "Read_RISCV_reserved_strong_acquire" + | Read_X86_locked => "Read_X86_locked" + )) read_kind)) + | IK_mem_write write_kind => STRCAT "IK_mem_write " + (((\x . (case x of + Write_plain => "Write_plain" + | Write_conditional => + "Write_conditional" + | Write_release => "Write_release" + | Write_exclusive => "Write_exclusive" + | Write_exclusive_release => + "Write_exclusive_release" + | Write_RISCV_release => + "Write_RISCV_release" + | Write_RISCV_strong_release => + "Write_RISCV_strong_release" + | Write_RISCV_conditional => + "Write_RISCV_conditional" + | Write_RISCV_conditional_release => + "Write_RISCV_conditional_release" + | Write_RISCV_conditional_strong_release => + "Write_RISCV_conditional_strong_release" + | Write_X86_locked => "Write_X86_locked" + )) write_kind)) + | IK_mem_rmw (r, w) => STRCAT "IK_mem_rmw " + (STRCAT + (((\x . (case x of + Read_plain => "Read_plain" + | Read_reserve => "Read_reserve" + | Read_acquire => "Read_acquire" + | Read_exclusive => "Read_exclusive" + | Read_exclusive_acquire => + "Read_exclusive_acquire" + | Read_stream => "Read_stream" + | Read_RISCV_acquire => "Read_RISCV_acquire" + | Read_RISCV_strong_acquire => + "Read_RISCV_strong_acquire" + | Read_RISCV_reserved => "Read_RISCV_reserved" + | Read_RISCV_reserved_acquire => + "Read_RISCV_reserved_acquire" + | Read_RISCV_reserved_strong_acquire => + "Read_RISCV_reserved_strong_acquire" + | Read_X86_locked => "Read_X86_locked" + )) r)) + (STRCAT " " + (((\x . (case x of + Write_plain => "Write_plain" + | Write_conditional => + "Write_conditional" + | Write_release => "Write_release" + | Write_exclusive => "Write_exclusive" + | Write_exclusive_release => + "Write_exclusive_release" + | Write_RISCV_release => + "Write_RISCV_release" + | Write_RISCV_strong_release => + "Write_RISCV_strong_release" + | Write_RISCV_conditional => + "Write_RISCV_conditional" + | Write_RISCV_conditional_release => + "Write_RISCV_conditional_release" + | Write_RISCV_conditional_strong_release => + "Write_RISCV_conditional_strong_release" + | Write_X86_locked => "Write_X86_locked" + )) w)))) + | IK_branch => "IK_branch" + | IK_trans trans_kind => STRCAT "IK_trans " + (((\x . (case x of + Transaction_start => "Transaction_start" + | Transaction_commit => "Transaction_commit" + | Transaction_abort => "Transaction_abort" + )) trans_kind)) + | IK_simple => "IK_simple" + ))|>))`; + + + +val _ = Define ` + ((read_is_exclusive:read_kind -> bool)= + (\x . (case x of + Read_plain => F + | Read_reserve => T + | Read_acquire => F + | Read_exclusive => T + | Read_exclusive_acquire => T + | Read_stream => F + | Read_RISCV_acquire => F + | Read_RISCV_strong_acquire => F + | Read_RISCV_reserved => T + | Read_RISCV_reserved_acquire => T + | Read_RISCV_reserved_strong_acquire => T + | Read_X86_locked => T + )))`; + + + + +val _ = Define ` +((instance_Sail_instr_kinds_EnumerationType_Sail_instr_kinds_read_kind_dict:(read_kind)EnumerationType_class)= (<| + + toNat_method := (\x . + (case x of + Read_plain =>( 0 : num) + | Read_reserve =>( 1 : num) + | Read_acquire =>( 2 : num) + | Read_exclusive =>( 3 : num) + | Read_exclusive_acquire =>( 4 : num) + | Read_stream =>( 5 : num) + | Read_RISCV_acquire =>( 6 : num) + | Read_RISCV_strong_acquire =>( 7 : num) + | Read_RISCV_reserved =>( 8 : num) + | Read_RISCV_reserved_acquire =>( 9 : num) + | Read_RISCV_reserved_strong_acquire =>( 10 : num) + | Read_X86_locked =>( 11 : num) + ))|>))`; + + +val _ = Define ` +((instance_Sail_instr_kinds_EnumerationType_Sail_instr_kinds_write_kind_dict:(write_kind)EnumerationType_class)= (<| + + toNat_method := (\x . + (case x of + Write_plain =>( 0 : num) + | Write_conditional =>( 1 : num) + | Write_release =>( 2 : num) + | Write_exclusive =>( 3 : num) + | Write_exclusive_release =>( 4 : num) + | Write_RISCV_release =>( 5 : num) + | Write_RISCV_strong_release =>( 6 : num) + | Write_RISCV_conditional =>( 7 : num) + | Write_RISCV_conditional_release =>( 8 : num) + | Write_RISCV_conditional_strong_release =>( 9 : num) + | Write_X86_locked =>( 10 : num) + ))|>))`; + + +val _ = Define ` +((instance_Sail_instr_kinds_EnumerationType_Sail_instr_kinds_barrier_kind_dict:(barrier_kind)EnumerationType_class)= (<| + + toNat_method := (\x . + (case x of + Barrier_Sync =>( 0 : num) + | Barrier_LwSync =>( 1 : num) + | Barrier_Eieio =>( 2 : num) + | Barrier_Isync =>( 3 : num) + | Barrier_DMB =>( 4 : num) + | Barrier_DMB_ST =>( 5 : num) + | Barrier_DMB_LD =>( 6 : num) + | Barrier_DSB =>( 7 : num) + | Barrier_DSB_ST =>( 8 : num) + | Barrier_DSB_LD =>( 9 : num) + | Barrier_ISB =>( 10 : num) + | Barrier_TM_COMMIT =>( 11 : num) + | Barrier_MIPS_SYNC =>( 12 : num) + | Barrier_RISCV_rw_rw =>( 13 : num) + | Barrier_RISCV_r_rw =>( 14 : num) + | Barrier_RISCV_r_r =>( 15 : num) + | Barrier_RISCV_rw_w =>( 16 : num) + | Barrier_RISCV_w_w =>( 17 : num) + | Barrier_RISCV_i =>( 18 : num) + | Barrier_x86_MFENCE =>( 19 : num) + ))|>))`; + +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml b/snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml new file mode 100644 index 00000000..f1f0c8d4 --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml @@ -0,0 +1,367 @@ +(*Generated by Lem from ../../src/gen_lib/sail_operators.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "sail_operators" + +(*open import Pervasives_extra*) +(*open import Machine_word*) +(*open import Sail_values*) + +(*** Bit vector operations *) + +(*val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list Sail_values.bitU*) +val _ = Define ` + ((concat_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'a -> 'b ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b l r= ( + dict_Sail_values_Bitvector_a.bits_of_method l ++ dict_Sail_values_Bitvector_b.bits_of_method r))`; + + +(*val cons_bv : forall 'a. Bitvector 'a => Sail_values.bitU -> 'a -> list Sail_values.bitU*) +val _ = Define ` + ((cons_bv:'a sail_values$Bitvector_class -> sail_values$bitU -> 'a ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a b v= (b :: + dict_Sail_values_Bitvector_a.bits_of_method v))`; + + +(*val cast_unit_bv : Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((cast_unit_bv:sail_values$bitU ->(sail_values$bitU)list) b= ([b]))`; + + +(*val bv_of_bit : Num.integer -> Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((bv_of_bit:int -> sail_values$bitU ->(sail_values$bitU)list) len b= (extz_bits len [b]))`; + + +val _ = Define ` + ((most_significant:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU)dict_Sail_values_Bitvector_a v= ((case + dict_Sail_values_Bitvector_a.bits_of_method v of + b :: _ => b + | _ => B0 (* Treat empty bitvector as all zeros *) + )))`; + + +val _ = Define ` + ((get_max_representable_in:bool -> int -> int) sign (n : int) : int= + (if (n =( 64 : int)) then (case sign of T => max_64 | F => max_64u ) + else if (n=( 32 : int)) then (case sign of T => max_32 | F => max_32u ) + else if (n=( 8 : int)) then max_8 + else if (n=( 5 : int)) then max_5 + else (case sign of T => (( 2 : int))** ((Num (ABS (I n))) -( 1 : num)) + | F => (( 2 : int))** (Num (ABS (I n))) + )))`; + + +val _ = Define ` + ((get_min_representable_in:'a -> int -> int) _ (n : int) : int= + (if n =( 64 : int) then min_64 + else if n =( 32 : int) then min_32 + else if n =( 8 : int) then min_8 + else if n =( 5 : int) then min_5 + else( 0 : int) - ((( 2 : int))** (Num (ABS (I n))))))`; + + +(*val arith_op_bv_int : forall 'a 'b. Bitvector 'a => + (Num.integer -> Num.integer -> Num.integer) -> bool -> 'a -> Num.integer -> 'a*) +val _ = Define ` + ((arith_op_bv_int:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> int -> 'a)dict_Sail_values_Bitvector_a op sign l r= + (let r' = (dict_Sail_values_Bitvector_a.of_int_method (dict_Sail_values_Bitvector_a.length_method l) r) in dict_Sail_values_Bitvector_a.arith_op_bv_method op sign l r'))`; + + +(*val arith_op_int_bv : forall 'a 'b. Bitvector 'a => + (Num.integer -> Num.integer -> Num.integer) -> bool -> Num.integer -> 'a -> 'a*) +val _ = Define ` + ((arith_op_int_bv:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> int -> 'a -> 'a)dict_Sail_values_Bitvector_a op sign l r= + (let l' = (dict_Sail_values_Bitvector_a.of_int_method (dict_Sail_values_Bitvector_a.length_method r) l) in dict_Sail_values_Bitvector_a.arith_op_bv_method op sign l' r))`; + + +val _ = Define ` + ((arith_op_bv_bool:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a op sign l r= (arith_op_bv_int + dict_Sail_values_Bitvector_a op sign l (if r then( 1 : int) else( 0 : int))))`; + +val _ = Define ` + ((arith_op_bv_bit:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a op sign l r= (OPTION_MAP (arith_op_bv_bool + dict_Sail_values_Bitvector_a op sign l) (bool_of_bitU r)))`; + + +(* TODO (or just omit and define it per spec if needed) +val arith_op_overflow_bv : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU) +let arith_op_overflow_bv op sign size l r = + let len = length l in + let act_size = len * size in + match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with + | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) -> + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size = of_int act_size n in + let one_more_size_u = bits_of_int (act_size + 1) n_unsign in + let overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then B0 else B1 in + let c_out = most_significant one_more_size_u in + (correct_size,overflow,c_out) + | (_, _, _, _) -> + (repeat [BU] act_size, BU, BU) + end + +let add_overflow_bv = arith_op_overflow_bv integerAdd false 1 +let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1 +let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1 +let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1 +let mult_overflow_bv = arith_op_overflow_bv integerMult false 2 +let mults_overflow_bv = arith_op_overflow_bv integerMult true 2 + +val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU) +let arith_op_overflow_bv_bit op sign size l r_bit = + let act_size = length l * size in + match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with + | (Just l', Just l_u, false) -> + let (n, nu, changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l', l_u, false) + | BU -> (* unreachable due to check above *) + failwith "arith_op_overflow_bv_bit applied to undefined bit" + end in + let correct_size = of_int act_size n in + let one_larger = bits_of_int (act_size + 1) nu in + let overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then B0 else B1 + else B0 in + (correct_size, overflow, most_significant one_larger) + | (_, _, _) -> + (repeat [BU] act_size, BU, BU) + end + +let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1 +let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1 +let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1 +let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*) + +val _ = Hol_datatype ` + shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot`; + + +val _ = Define ` + ((invert_shift:shift -> shift)= + (\x . (case x of + LL_shift => RR_shift + | RR_shift => LL_shift + | RR_shift_arith => LL_shift + | LL_rot => RR_rot + | RR_rot => LL_rot + )))`; + + +(*val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((shift_op_bv:'a sail_values$Bitvector_class -> shift -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a op v n= + (let v = (dict_Sail_values_Bitvector_a.bits_of_method v) in + if n =( 0 : int) then v else + let (op, n) = (if n >( 0 : int) then (op, n) else (invert_shift op, ~ n)) in + (case op of + LL_shift => + subrange_list T v n (int_of_num (LENGTH v) -( 1 : int)) ++ repeat [B0] n + | RR_shift => + repeat [B0] n ++ subrange_list T v(( 0 : int)) ((int_of_num (LENGTH v) - n) -( 1 : int)) + | RR_shift_arith => + repeat [most_significant + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) v] n ++ subrange_list T v(( 0 : int)) ((int_of_num (LENGTH v) - n) -( 1 : int)) + | LL_rot => + subrange_list T v n (int_of_num (LENGTH v) -( 1 : int)) ++ subrange_list T v(( 0 : int)) (n -( 1 : int)) + | RR_rot => + subrange_list F v(( 0 : int)) (n -( 1 : int)) ++ subrange_list F v n (int_of_num (LENGTH v) -( 1 : int)) + )))`; + + +val _ = Define ` + ((shiftl_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a= (shift_op_bv + dict_Sail_values_Bitvector_a LL_shift))`; + (*"<<"*) +val _ = Define ` + ((shiftr_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a= (shift_op_bv + dict_Sail_values_Bitvector_a RR_shift))`; + (*">>"*) +val _ = Define ` + ((arith_shiftr_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a= (shift_op_bv + dict_Sail_values_Bitvector_a RR_shift_arith))`; + +val _ = Define ` + ((rotl_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a= (shift_op_bv + dict_Sail_values_Bitvector_a LL_rot))`; + (*"<<<"*) +val _ = Define ` + ((rotr_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a= (shift_op_bv + dict_Sail_values_Bitvector_a LL_rot))`; + (*">>>"*) + +val _ = Define ` + ((shiftl_mword:'a words$word -> int -> 'a words$word) w n= (words$word_lsl w (nat_of_int n)))`; + +val _ = Define ` + ((shiftr_mword:'a words$word -> int -> 'a words$word) w n= (words$word_lsr w (nat_of_int n)))`; + +val _ = Define ` + ((arith_shiftr_mword:'a words$word -> int -> 'a words$word) w n= (words$word_asr w (nat_of_int n)))`; + +val _ = Define ` + ((rotl_mword:'a words$word -> int -> 'a words$word) w n= (words$word_rol w (nat_of_int n)))`; + +val _ = Define ` + ((rotr_mword:'a words$word -> int -> 'a words$word) w n= (words$word_ror w (nat_of_int n)))`; + + + val _ = Define ` + ((arith_op_no0:(int -> int -> int) -> int -> int ->(int)option) (op : int -> int -> int) l r= + (if r =( 0 : int) + then NONE + else SOME (op l r)))`; + + +(*val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (Num.integer -> Num.integer -> Num.integer) -> bool -> Num.integer -> 'a -> 'a -> Maybe.maybe 'b*) +val _ = Define ` + ((arith_op_bv_no0:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class ->(int -> int -> int) -> bool -> int -> 'a -> 'a -> 'b option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b op sign size1 l r= + (OPTION_BIND (int_of_bv + dict_Sail_values_Bitvector_a sign l) (\ l' . + OPTION_BIND (int_of_bv + dict_Sail_values_Bitvector_a sign r) (\ r' . + if r' =( 0 : int) then NONE else SOME ( + dict_Sail_values_Bitvector_b.of_int_method (dict_Sail_values_Bitvector_a.length_method l * size1) (op l' r'))))))`; + + +val _ = Define ` + ((mod_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> 'b -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b= (arith_op_bv_no0 + dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_mod F(( 1 : int))))`; + +val _ = Define ` + ((quot_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> 'b -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b= (arith_op_bv_no0 + dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_quot F(( 1 : int))))`; + +val _ = Define ` + ((quots_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> 'b -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b= (arith_op_bv_no0 + dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_quot T(( 1 : int))))`; + + +val _ = Define ` + ((mod_mword:'a words$word -> 'a words$word -> 'a words$word)= words$word_mod)`; + +val _ = Define ` + ((quot_mword:'a words$word -> 'a words$word -> 'a words$word)= words$word_div)`; + +val _ = Define ` + ((quots_mword:'a words$word -> 'a words$word -> 'a words$word)= words$word_quot)`; + + +val _ = Define ` + ((arith_op_bv_int_no0:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class ->(int -> int -> int) -> bool -> int -> 'a -> int -> 'b option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b op sign size1 l r= + (arith_op_bv_no0 dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b op sign size1 l (dict_Sail_values_Bitvector_a.of_int_method (dict_Sail_values_Bitvector_a.length_method l) r)))`; + + +val _ = Define ` + ((quot_bv_int:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> int -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b= (arith_op_bv_int_no0 + dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_quot F(( 1 : int))))`; + +val _ = Define ` + ((mod_bv_int:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> int -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b= (arith_op_bv_int_no0 + dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_mod F(( 1 : int))))`; + + +val _ = Define ` + ((mod_mword_int:'a words$word -> int -> 'a words$word) l r= (words$word_mod l (integer_word$i2w r)))`; + +val _ = Define ` + ((quot_mword_int:'a words$word -> int -> 'a words$word) l r= (words$word_div l (integer_word$i2w r)))`; + +val _ = Define ` + ((quots_mword_int:'a words$word -> int -> 'a words$word) l r= (words$word_quot l (integer_word$i2w r)))`; + + +val _ = Define ` + ((replicate_bits_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a v count1= (repeat ( + dict_Sail_values_Bitvector_a.bits_of_method v) count1))`; + +val _ = Define ` + ((duplicate_bit_bv:'a sail_values$BitU_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_BitU_a bit len= (replicate_bits_bv + (instance_Sail_values_Bitvector_list_dict dict_Sail_values_BitU_a) [bit] len))`; + + +(*val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*) +val _ = Define ` + ((eq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= ( + dict_Sail_values_Bitvector_a.bits_of_method l = dict_Sail_values_Bitvector_a.bits_of_method r))`; + + +(*val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*) +val _ = Define ` + ((neq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= (~ (eq_bv + dict_Sail_values_Bitvector_a l r)))`; + + +(*val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*) +val _ = Define ` + ((ult_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= (lexicographic_less (\ l r. (compare_bitU l r) = LT) (\ l r. (compare_bitU l r) <> GT) (REVERSE ( + dict_Sail_values_Bitvector_a.bits_of_method l)) (REVERSE (dict_Sail_values_Bitvector_a.bits_of_method r))))`; + +val _ = Define ` + ((ulteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= ((eq_bv + dict_Sail_values_Bitvector_a l r) \/ (ult_bv dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((ugt_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= (~ (ulteq_bv + dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((ugteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= ((eq_bv + dict_Sail_values_Bitvector_a l r) \/ (ugt_bv dict_Sail_values_Bitvector_a l r)))`; + + +(*val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*) +val _ = Define ` + ((slt_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= + ((case (most_significant + dict_Sail_values_Bitvector_a l, most_significant dict_Sail_values_Bitvector_a r) of + (B0, B0) => ult_bv + dict_Sail_values_Bitvector_a l r + | (B0, B1) => F + | (B1, B0) => T + | (B1, B1) => + let l' = (add_one_bit_ignore_overflow ( + dict_Sail_values_Bitvector_a.bits_of_method l)) in + let r' = (add_one_bit_ignore_overflow ( + dict_Sail_values_Bitvector_a.bits_of_method r)) in + ugt_bv (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l' r' + | (BU, BU) => ult_bv + dict_Sail_values_Bitvector_a l r + | (BU, _) => T + | (_, BU) => F + )))`; + +val _ = Define ` + ((slteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= ((eq_bv + dict_Sail_values_Bitvector_a l r) \/ (slt_bv dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((sgt_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= (~ (slteq_bv + dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((sgteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r= ((eq_bv + dict_Sail_values_Bitvector_a l r) \/ (sgt_bv dict_Sail_values_Bitvector_a l r)))`; + + +(*val ucmp_mword : forall 'a. Size 'a => (Num.integer -> Num.integer -> bool) -> Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) + +(*val scmp_mword : forall 'a. Size 'a => (Num.integer -> Num.integer -> bool) -> Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml b/snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml new file mode 100644 index 00000000..5d2978bb --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml @@ -0,0 +1,792 @@ +(*Generated by Lem from ../../src/gen_lib/sail_operators_bitlists.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory sail_operatorsTheory prompt_monadTheory promptTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "sail_operators_bitlists" + +(*open import Pervasives_extra*) +(*open import Machine_word*) +(*open import Sail_values*) +(*open import Sail_operators*) +(*open import Prompt_monad*) +(*open import Prompt*) + +(* Specialisation of operators to bit lists *) + +(*val uint_maybe : list Sail_values.bitU -> Maybe.maybe Num.integer*) +val _ = Define ` + ((uint_maybe0:(sail_values$bitU)list ->(int)option) v= (unsigned_of_bits (MAP (\ b. b) v)))`; + +val _ = Define ` + ((uint_fail0:'a sail_values$Bitvector_class -> 'a -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set)dict_Sail_values_Bitvector_a v= (state_monad$maybe_failS "uint" ( + dict_Sail_values_Bitvector_a.unsigned_method v)))`; + +val _ = Define ` + ((uint_oracle0:(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) v= (state_monad$bindS +(state$bools_of_bits_oracleS v) (\ bs . + state_monad$returnS (int_of_bools F bs))))`; + +val _ = Define ` + ((uint:(sail_values$bitU)list -> int) v= (maybe_failwith (uint_maybe0 v)))`; + + +(*val sint_maybe : list Sail_values.bitU -> Maybe.maybe Num.integer*) +val _ = Define ` + ((sint_maybe0:(sail_values$bitU)list ->(int)option) v= (signed_of_bits (MAP (\ b. b) v)))`; + +val _ = Define ` + ((sint_fail0:'a sail_values$Bitvector_class -> 'a -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set)dict_Sail_values_Bitvector_a v= (state_monad$maybe_failS "sint" ( + dict_Sail_values_Bitvector_a.signed_method v)))`; + +val _ = Define ` + ((sint_oracle0:(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) v= (state_monad$bindS +(state$bools_of_bits_oracleS v) (\ bs . + state_monad$returnS (int_of_bools T bs))))`; + +val _ = Define ` + ((sint:(sail_values$bitU)list -> int) v= (maybe_failwith (sint_maybe0 v)))`; + + +(*val extz_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((extz_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)= + (extz_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val exts_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((exts_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)= + (exts_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val zero_extend : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((zero_extend0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) bits len= (extz_bits len bits))`; + + +(*val sign_extend : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((sign_extend0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) bits len= (exts_bits len bits))`; + + +(*val vector_truncate : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((vector_truncate0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) bs len= (extz_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) len bs))`; + + +(*val vec_of_bits_maybe : list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*) +(*val vec_of_bits_fail : forall 'rv 'e. list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val vec_of_bits_oracle : forall 'rv 'e. list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val vec_of_bits_failwith : list Sail_values.bitU -> list Sail_values.bitU*) +(*val vec_of_bits : list Sail_values.bitU -> list Sail_values.bitU*) + +(*val access_vec_inc : list Sail_values.bitU -> Num.integer -> Sail_values.bitU*) +val _ = Define ` + ((access_vec_inc0:(sail_values$bitU)list -> int -> sail_values$bitU)= + (access_bv_inc + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val access_vec_dec : list Sail_values.bitU -> Num.integer -> Sail_values.bitU*) +val _ = Define ` + ((access_vec_dec0:(sail_values$bitU)list -> int -> sail_values$bitU)= + (access_bv_dec + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val update_vec_inc : list Sail_values.bitU -> Num.integer -> Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((update_vec_inc0:(sail_values$bitU)list -> int -> sail_values$bitU ->(sail_values$bitU)list)= + (update_bv_inc + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((update_vec_inc_maybe0:(sail_values$bitU)list -> int -> sail_values$bitU ->((sail_values$bitU)list)option) v i b= (SOME (update_vec_inc0 v i b)))`; + +val _ = Define ` + ((update_vec_inc_fail0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b= (state_monad$returnS (update_vec_inc0 v i b)))`; + +val _ = Define ` + ((update_vec_inc_oracle0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b= (state_monad$returnS (update_vec_inc0 v i b)))`; + + +(*val update_vec_dec : list Sail_values.bitU -> Num.integer -> Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((update_vec_dec0:(sail_values$bitU)list -> int -> sail_values$bitU ->(sail_values$bitU)list)= + (update_bv_dec + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((update_vec_dec_maybe0:(sail_values$bitU)list -> int -> sail_values$bitU ->((sail_values$bitU)list)option) v i b= (SOME (update_vec_dec0 v i b)))`; + +val _ = Define ` + ((update_vec_dec_fail0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b= (state_monad$returnS (update_vec_dec0 v i b)))`; + +val _ = Define ` + ((update_vec_dec_oracle0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b= (state_monad$returnS (update_vec_dec0 v i b)))`; + + +(*val subrange_vec_inc : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((subrange_vec_inc0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list)= + (subrange_bv_inc + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val subrange_vec_dec : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((subrange_vec_dec0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list)= + (subrange_bv_dec + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val update_subrange_vec_inc : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((update_subrange_vec_inc0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list ->(sail_values$bitU)list)= + (update_subrange_bv_inc + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val update_subrange_vec_dec : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((update_subrange_vec_dec0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list ->(sail_values$bitU)list)= + (update_subrange_bv_dec + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val concat_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((concat_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= + (concat_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val cons_vec : Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((cons_vec0:sail_values$bitU ->(sail_values$bitU)list ->(sail_values$bitU)list)= + (cons_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((cons_vec_maybe0:sail_values$bitU ->(sail_values$bitU)list ->((sail_values$bitU)list)option) b v= (SOME (cons_vec0 b v)))`; + +val _ = Define ` + ((cons_vec_fail0:sail_values$bitU ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b v= (state_monad$returnS (cons_vec0 b v)))`; + +val _ = Define ` + ((cons_vec_oracle0:sail_values$bitU ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b v= (state_monad$returnS (cons_vec0 b v)))`; + + +(*val cast_unit_vec : Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((cast_unit_vec0:sail_values$bitU ->(sail_values$bitU)list)= cast_unit_bv)`; + +val _ = Define ` + ((cast_unit_vec_maybe0:sail_values$bitU ->((sail_values$bitU)list)option) b= (SOME (cast_unit_vec0 b)))`; + +val _ = Define ` + ((cast_unit_vec_fail0:sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b= (state_monad$returnS (cast_unit_vec0 b)))`; + +val _ = Define ` + ((cast_unit_vec_oracle0:sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b= (state_monad$returnS (cast_unit_vec0 b)))`; + + +(*val vec_of_bit : Num.integer -> Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((vec_of_bit0:int -> sail_values$bitU ->(sail_values$bitU)list)= bv_of_bit)`; + +val _ = Define ` + ((vec_of_bit_maybe0:int -> sail_values$bitU ->((sail_values$bitU)list)option) len b= (SOME (vec_of_bit0 len b)))`; + +val _ = Define ` + ((vec_of_bit_fail0:int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) len b= (state_monad$returnS (vec_of_bit0 len b)))`; + +val _ = Define ` + ((vec_of_bit_oracle0:int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) len b= (state_monad$returnS (vec_of_bit0 len b)))`; + + +(*val msb : list Sail_values.bitU -> Sail_values.bitU*) +val _ = Define ` + ((msb0:(sail_values$bitU)list -> sail_values$bitU)= + (most_significant + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val int_of_vec_maybe : bool -> list Sail_values.bitU -> Maybe.maybe Num.integer*) +val _ = Define ` + ((int_of_vec_maybe0:bool ->(sail_values$bitU)list ->(int)option)= + (int_of_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((int_of_vec_fail0:bool ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) sign v= (state_monad$maybe_failS "int_of_vec" (int_of_vec_maybe0 sign v)))`; + +val _ = Define ` + ((int_of_vec_oracle:bool ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) sign v= (state_monad$bindS (state$bools_of_bits_oracleS v) (\ v . state_monad$returnS (int_of_bools sign v))))`; + +val _ = Define ` + ((int_of_vec0:bool ->(sail_values$bitU)list -> int) sign v= (maybe_failwith (int_of_vec_maybe0 sign v)))`; + + +(*val string_of_vec : list Sail_values.bitU -> string*) +val _ = Define ` + ((string_of_vec0:(sail_values$bitU)list -> string)= + (string_of_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val and_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val or_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val xor_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val not_vec : list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((and_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (binop_list and_bit))`; + +val _ = Define ` + ((or_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (binop_list or_bit))`; + +val _ = Define ` + ((xor_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (binop_list xor_bit))`; + +val _ = Define ` + ((not_vec0:(sail_values$bitU)list ->(sail_values$bitU)list)= (MAP not_bit))`; + + +(*val arith_op_double_bl : forall 'a 'b. Bitvector 'a => + (Num.integer -> Num.integer -> Num.integer) -> bool -> 'a -> 'a -> list Sail_values.bitU*) +val _ = Define ` + ((arith_op_double_bl:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> 'a ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a op sign l r= + (let len =(( 2 : int) * + dict_Sail_values_Bitvector_a.length_method l) in + let l' = (if sign then exts_bv + dict_Sail_values_Bitvector_a len l else extz_bv dict_Sail_values_Bitvector_a len l) in + let r' = (if sign then exts_bv + dict_Sail_values_Bitvector_a len r else extz_bv dict_Sail_values_Bitvector_a len r) in + MAP (\ b. b) (arith_op_bits op sign (MAP (\ b. b) l') (MAP (\ b. b) r'))))`; + + +(*val add_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val adds_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val sub_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val subs_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val mult_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val mults_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((add_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (\ l r. MAP (\ b. b) (arith_op_bits (+) F (MAP (\ b. b) l) (MAP (\ b. b) r))))`; + +val _ = Define ` + ((adds_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (\ l r. MAP (\ b. b) (arith_op_bits (+) T (MAP (\ b. b) l) (MAP (\ b. b) r))))`; + +val _ = Define ` + ((sub_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (\ l r. MAP (\ b. b) (arith_op_bits (-) F (MAP (\ b. b) l) (MAP (\ b. b) r))))`; + +val _ = Define ` + ((subs_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (\ l r. MAP (\ b. b) (arith_op_bits (-) T (MAP (\ b. b) l) (MAP (\ b. b) r))))`; + +val _ = Define ` + ((mult_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (arith_op_double_bl + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) F))`; + +val _ = Define ` + ((mults_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= (arith_op_double_bl + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) T))`; + + +(*val add_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val adds_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val sub_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val subs_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val mult_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val mults_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((add_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (arith_op_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (+) F l r))`; + +val _ = Define ` + ((adds_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (arith_op_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (+) T l r))`; + +val _ = Define ` + ((sub_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (arith_op_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (-) F l r))`; + +val _ = Define ` + ((subs_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (arith_op_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (-) T l r))`; + +val _ = Define ` + ((mult_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (arith_op_double_bl + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) F l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`; + +val _ = Define ` + ((mults_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (arith_op_double_bl + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) T l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`; + + +(*val add_int_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val adds_int_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val sub_int_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val subs_int_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val mult_int_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val mults_int_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((add_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (arith_op_int_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (+) F l r))`; + +val _ = Define ` + ((adds_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (arith_op_int_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (+) T l r))`; + +val _ = Define ` + ((sub_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (arith_op_int_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (-) F l r))`; + +val _ = Define ` + ((subs_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (arith_op_int_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (-) T l r))`; + +val _ = Define ` + ((mult_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (arith_op_double_bl + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) F (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`; + +val _ = Define ` + ((mults_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (arith_op_double_bl + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) T (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`; + + +(*val add_vec_bit : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*) +(*val adds_vec_bit : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*) +(*val sub_vec_bit : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*) +(*val subs_vec_bit : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*) + +val _ = Define ` + ((add_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bool + dict_Sail_values_Bitvector_a (+) F l r))`; + +val _ = Define ` + ((add_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bit + dict_Sail_values_Bitvector_a (+) F l r))`; + +val _ = Define ` + ((add_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$maybe_failS "add_vec_bit" (add_vec_bit_maybe0 + dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((add_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (add_vec_bool0 + dict_Sail_values_Bitvector_a l r))))`; + +val _ = Define ` + ((add_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list) l r= (option_CASE (add_vec_bit_maybe0 + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + + +val _ = Define ` + ((adds_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bool + dict_Sail_values_Bitvector_a (+) T l r))`; + +val _ = Define ` + ((adds_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bit + dict_Sail_values_Bitvector_a (+) T l r))`; + +val _ = Define ` + ((adds_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$maybe_failS "adds_vec_bit" (adds_vec_bit_maybe0 + dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((adds_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (adds_vec_bool0 + dict_Sail_values_Bitvector_a l r))))`; + +val _ = Define ` + ((adds_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list) l r= (option_CASE (adds_vec_bit_maybe0 + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + + +val _ = Define ` + ((sub_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bool + dict_Sail_values_Bitvector_a (-) F l r))`; + +val _ = Define ` + ((sub_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bit + dict_Sail_values_Bitvector_a (-) F l r))`; + +val _ = Define ` + ((sub_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$maybe_failS "sub_vec_bit" (sub_vec_bit_maybe0 + dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((sub_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (sub_vec_bool0 + dict_Sail_values_Bitvector_a l r))))`; + +val _ = Define ` + ((sub_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list) l r= (option_CASE (sub_vec_bit_maybe0 + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + + +val _ = Define ` + ((subs_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bool + dict_Sail_values_Bitvector_a (-) T l r))`; + +val _ = Define ` + ((subs_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a l r= (arith_op_bv_bit + dict_Sail_values_Bitvector_a (-) T l r))`; + +val _ = Define ` + ((subs_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$maybe_failS "sub_vec_bit" (subs_vec_bit_maybe0 + dict_Sail_values_Bitvector_a l r)))`; + +val _ = Define ` + ((subs_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (subs_vec_bool0 + dict_Sail_values_Bitvector_a l r))))`; + +val _ = Define ` + ((subs_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list) l r= (option_CASE (subs_vec_bit_maybe0 + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + + +(*val add_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) +val add_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) +val mult_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) +val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) +let add_overflow_vec = add_overflow_bv +let add_overflow_vec_signed = add_overflow_bv_signed +let sub_overflow_vec = sub_overflow_bv +let sub_overflow_vec_signed = sub_overflow_bv_signed +let mult_overflow_vec = mult_overflow_bv +let mult_overflow_vec_signed = mult_overflow_bv_signed + +val add_overflow_vec_bit : list bitU -> bitU -> (list bitU * bitU * bitU) +val add_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec_bit : list bitU -> bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU) +let add_overflow_vec_bit = add_overflow_bv_bit +let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed +let sub_overflow_vec_bit = sub_overflow_bv_bit +let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*) + +(*val shiftl : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val shiftr : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val arith_shiftr : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val rotl : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val rotr : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((shiftl0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= + (shiftl_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((shiftr0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= + (shiftr_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((arith_shiftr0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= + (arith_shiftr_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((rotl0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= + (rotl_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((rotr0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= + (rotr_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val mod_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val mod_vec_maybe : list Sail_values.bitU -> list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*) +(*val mod_vec_fail : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val mod_vec_oracle : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +val _ = Define ` + ((mod_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (option_CASE (mod_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + +val _ = Define ` + ((mod_vec_maybe0:(sail_values$bitU)list ->(sail_values$bitU)list ->((sail_values$bitU)list)option) l r= (mod_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`; + +val _ = Define ` + ((mod_vec_fail0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "mod_vec" (mod_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`; + +val _ = Define ` + ((mod_vec_oracle0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state$of_bits_oracleS + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (mod_vec0 l r)))`; + + +(*val quot_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val quot_vec_maybe : list Sail_values.bitU -> list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*) +(*val quot_vec_fail : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val quot_vec_oracle : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +val _ = Define ` + ((quot_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (option_CASE (quot_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + +val _ = Define ` + ((quot_vec_maybe0:(sail_values$bitU)list ->(sail_values$bitU)list ->((sail_values$bitU)list)option) l r= (quot_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`; + +val _ = Define ` + ((quot_vec_fail0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "quot_vec" (quot_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`; + +val _ = Define ` + ((quot_vec_oracle0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state$of_bits_oracleS + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (quot_vec0 l r)))`; + + +(*val quots_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*) +(*val quots_vec_maybe : list Sail_values.bitU -> list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*) +(*val quots_vec_fail : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val quots_vec_oracle : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +val _ = Define ` + ((quots_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list) l r= (option_CASE (quots_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + +val _ = Define ` + ((quots_vec_maybe0:(sail_values$bitU)list ->(sail_values$bitU)list ->((sail_values$bitU)list)option) l r= (quots_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`; + +val _ = Define ` + ((quots_vec_fail0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "quots_vec" (quots_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`; + +val _ = Define ` + ((quots_vec_oracle0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state$of_bits_oracleS + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (quots_vec0 l r)))`; + + +(*val mod_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val mod_vec_int_maybe : list Sail_values.bitU -> Num.integer -> Maybe.maybe (list Sail_values.bitU)*) +(*val mod_vec_int_fail : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val mod_vec_int_oracle : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +val _ = Define ` + ((mod_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (option_CASE (mod_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + +val _ = Define ` + ((mod_vec_int_maybe0:(sail_values$bitU)list -> int ->((sail_values$bitU)list)option) l r= (mod_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`; + +val _ = Define ` + ((mod_vec_int_fail0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "mod_vec_int" (mod_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`; + +val _ = Define ` + ((mod_vec_int_oracle0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state$of_bits_oracleS + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (mod_vec_int0 l r)))`; + + +(*val quot_vec_int : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +(*val quot_vec_int_maybe : list Sail_values.bitU -> Num.integer -> Maybe.maybe (list Sail_values.bitU)*) +(*val quot_vec_int_fail : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +(*val quot_vec_int_oracle : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*) +val _ = Define ` + ((quot_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r= (option_CASE (quot_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`; + +val _ = Define ` + ((quot_vec_int_maybe0:(sail_values$bitU)list -> int ->((sail_values$bitU)list)option) l r= (quot_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`; + +val _ = Define ` + ((quot_vec_int_fail0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "quot_vec_int" (quot_bv_int + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`; + +val _ = Define ` + ((quot_vec_int_oracle0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state$of_bits_oracleS + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict) (quot_vec_int0 l r)))`; + + +(*val replicate_bits : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((replicate_bits0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= + (replicate_bits_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + + +(*val duplicate : Sail_values.bitU -> Num.integer -> list Sail_values.bitU*) +val _ = Define ` + ((duplicate0:sail_values$bitU -> int ->(sail_values$bitU)list)= + (duplicate_bit_bv instance_Sail_values_BitU_Sail_values_bitU_dict))`; + +val _ = Define ` + ((duplicate_maybe0:sail_values$bitU -> int ->((sail_values$bitU)list)option) b n= (SOME (duplicate0 b n)))`; + +val _ = Define ` + ((duplicate_fail0:sail_values$bitU -> int -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b n= (state_monad$returnS (duplicate0 b n)))`; + +val _ = Define ` + ((duplicate_oracle0:sail_values$bitU -> int -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b n= (state_monad$bindS +(state$bool_of_bitU_oracleS b) (\ b . + state_monad$returnS (duplicate0 (bitU_of_bool b) n))))`; + + +(*val reverse_endianness : list Sail_values.bitU -> list Sail_values.bitU*) +val _ = Define ` + ((reverse_endianness0:(sail_values$bitU)list ->(sail_values$bitU)list) v= (reverse_endianness_list v))`; + + +(*val eq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val neq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val ult_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val slt_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val ugt_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val sgt_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val ulteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val slteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val ugteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +(*val sgteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*) +val _ = Define ` + ((eq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (eq_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((neq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (neq_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((ult_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (ult_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((slt_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (slt_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((ugt_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (ugt_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((sgt_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (sgt_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((ulteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (ulteq_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((slteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (slteq_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((ugteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (ugteq_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = Define ` + ((sgteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= + (sgteq_bv + (instance_Sail_values_Bitvector_list_dict + instance_Sail_values_BitU_Sail_values_bitU_dict)))`; + +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml b/snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml new file mode 100644 index 00000000..bd0a68ef --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml @@ -0,0 +1,612 @@ +(*Generated by Lem from ../../src/gen_lib/sail_operators_mwords.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory sail_operatorsTheory prompt_monadTheory promptTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "sail_operators_mwords" + +(*open import Pervasives_extra*) +(*open import Machine_word*) +(*open import Sail_values*) +(*open import Sail_operators*) +(*open import Prompt_monad*) +(*open import Prompt*) +val _ = Define ` + ((uint_maybe:'a words$word ->(int)option) v= (SOME (lem$w2ui v)))`; + +val _ = Define ` + ((uint_fail:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v= (state_monad$returnS (lem$w2ui v)))`; + +val _ = Define ` + ((uint_oracle:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v= (state_monad$returnS (lem$w2ui v)))`; + +val _ = Define ` + ((sint_maybe:'a words$word ->(int)option) v= (SOME (integer_word$w2i v)))`; + +val _ = Define ` + ((sint_fail:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v= (state_monad$returnS (integer_word$w2i v)))`; + +val _ = Define ` + ((sint_oracle:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v= (state_monad$returnS (integer_word$w2i v)))`; + + +(*val vec_of_bits_maybe : forall 'a. Size 'a => list Sail_values.bitU -> Maybe.maybe (Machine_word.mword 'a)*) +(*val vec_of_bits_fail : forall 'rv 'a 'e. Size 'a => list Sail_values.bitU -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val vec_of_bits_oracle : forall 'rv 'a 'e. Size 'a => list Sail_values.bitU -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val vec_of_bits_failwith : forall 'a. Size 'a => list Sail_values.bitU -> Machine_word.mword 'a*) +(*val vec_of_bits : forall 'a. Size 'a => list Sail_values.bitU -> Machine_word.mword 'a*) +val _ = Define ` + ((vec_of_bits_maybe:(sail_values$bitU)list ->('a words$word)option) bits= (OPTION_MAP bitstring$v2w (just_list (MAP bool_of_bitU bits))))`; + +val _ = Define ` + ((vec_of_bits_fail:(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) bits= (state$of_bits_failS + instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`; + +val _ = Define ` + ((vec_of_bits_oracle:(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) bits= (state$of_bits_oracleS + instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`; + +val _ = Define ` + ((vec_of_bits_failwith:(sail_values$bitU)list -> 'a words$word) bits= (of_bits_failwith + instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`; + +val _ = Define ` + ((vec_of_bits:(sail_values$bitU)list -> 'a words$word) bits= (of_bits_failwith + instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`; + + +(*val access_vec_inc : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Sail_values.bitU*) +val _ = Define ` + ((access_vec_inc:'a words$word -> int -> sail_values$bitU)= + (access_bv_inc instance_Sail_values_Bitvector_Machine_word_mword_dict))`; + + +(*val access_vec_dec : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Sail_values.bitU*) +val _ = Define ` + ((access_vec_dec:'a words$word -> int -> sail_values$bitU)= + (access_bv_dec instance_Sail_values_Bitvector_Machine_word_mword_dict))`; + + +val _ = Define ` + ((update_vec_dec_maybe:'a words$word -> int -> sail_values$bitU ->('a words$word)option) w i b= (update_mword_dec w i b))`; + +val _ = Define ` + ((update_vec_dec_fail:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b= (state_monad$bindS +(state$bool_of_bitU_fail b) (\ b . + state_monad$returnS (update_mword_bool_dec w i b))))`; + +val _ = Define ` + ((update_vec_dec_oracle:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b= (state_monad$bindS +(state$bool_of_bitU_oracleS b) (\ b . + state_monad$returnS (update_mword_bool_dec w i b))))`; + +val _ = Define ` + ((update_vec_dec:'a words$word -> int -> sail_values$bitU -> 'a words$word) w i b= (maybe_failwith (update_vec_dec_maybe w i b)))`; + + +val _ = Define ` + ((update_vec_inc_maybe:'a words$word -> int -> sail_values$bitU ->('a words$word)option) w i b= (update_mword_inc w i b))`; + +val _ = Define ` + ((update_vec_inc_fail:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b= (state_monad$bindS +(state$bool_of_bitU_fail b) (\ b . + state_monad$returnS (update_mword_bool_inc w i b))))`; + +val _ = Define ` + ((update_vec_inc_oracle:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b= (state_monad$bindS +(state$bool_of_bitU_oracleS b) (\ b . + state_monad$returnS (update_mword_bool_inc w i b))))`; + +val _ = Define ` + ((update_vec_inc:'a words$word -> int -> sail_values$bitU -> 'a words$word) w i b= (maybe_failwith (update_vec_inc_maybe w i b)))`; + + +(*val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((subrange_vec_dec:'a words$word -> int -> int -> 'b words$word) w i j= (words$word_extract (nat_of_int i) (nat_of_int j) w))`; + + +(*val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((subrange_vec_inc:'a words$word -> int -> int -> 'b words$word) w i j= (subrange_vec_dec w ((int_of_num (words$word_len w) -( 1 : int)) - i) ((int_of_num (words$word_len w) -( 1 : int)) - j)))`; + + +(*val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*) +val _ = Define ` + ((update_subrange_vec_dec:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'= (words$bit_field_insert (nat_of_int i) (nat_of_int j) w' w))`; + + +(*val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*) +val _ = Define ` + ((update_subrange_vec_inc:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'= (update_subrange_vec_dec w ((int_of_num (words$word_len w) -( 1 : int)) - i) ((int_of_num (words$word_len w) -( 1 : int)) - j) w'))`; + + +(*val extz_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*) +val _ = Define ` + ((extz_vec:int -> 'a words$word -> 'b words$word) _ w= (words$w2w w))`; + + +(*val exts_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*) +val _ = Define ` + ((exts_vec:int -> 'a words$word -> 'b words$word) _ w= (words$sw2sw w))`; + + +(*val zero_extend : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((zero_extend:'a words$word -> int -> 'b words$word) w _= (words$w2w w))`; + + +(*val sign_extend : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((sign_extend:'a words$word -> int -> 'b words$word) w _= (words$sw2sw w))`; + + +(*val vector_truncate : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((vector_truncate:'a words$word -> int -> 'b words$word) w _= (words$w2w w))`; + + +(*val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => Machine_word.mword 'a -> Machine_word.mword 'b -> Machine_word.mword 'c*) +val _ = Define ` + ((concat_vec:'a words$word -> 'b words$word -> 'c words$word)= words$word_concat)`; + + +(*val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> Machine_word.mword 'a -> Machine_word.mword 'b*) +val _ = Define ` + ((cons_vec_bool:bool -> 'a words$word -> 'b words$word) b w= (bitstring$v2w (b :: bitstring$w2v w)))`; + +val _ = Define ` + ((cons_vec_maybe:sail_values$bitU -> 'c words$word ->('b words$word)option) b w= (OPTION_MAP (\ b . cons_vec_bool b w) (bool_of_bitU b)))`; + +val _ = Define ` + ((cons_vec_fail:sail_values$bitU -> 'c words$word -> 'd state_monad$sequential_state ->((('b words$word),'e)state_monad$result#'d state_monad$sequential_state)set) b w= (state_monad$bindS (state$bool_of_bitU_fail b) (\ b . state_monad$returnS (cons_vec_bool b w))))`; + +val _ = Define ` + ((cons_vec_oracle:sail_values$bitU -> 'c words$word -> 'd state_monad$sequential_state ->((('b words$word),'e)state_monad$result#'d state_monad$sequential_state)set) b w= (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b . state_monad$returnS (cons_vec_bool b w))))`; + +val _ = Define ` + ((cons_vec:sail_values$bitU -> 'a words$word -> 'b words$word) b w= (maybe_failwith (cons_vec_maybe b w)))`; + + +(*val vec_of_bool : forall 'a. Size 'a => Num.integer -> bool -> Machine_word.mword 'a*) +val _ = Define ` + ((vec_of_bool:int -> bool -> 'a words$word) _ b= (bitstring$v2w [b]))`; + +val _ = Define ` + ((vec_of_bit_maybe:int -> sail_values$bitU ->('a words$word)option) len b= (OPTION_MAP (vec_of_bool len) (bool_of_bitU b)))`; + +val _ = Define ` + ((vec_of_bit_fail:int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) len b= (state_monad$bindS (state$bool_of_bitU_fail b) (\ b . state_monad$returnS (vec_of_bool len b))))`; + +val _ = Define ` + ((vec_of_bit_oracle:int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) len b= (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b . state_monad$returnS (vec_of_bool len b))))`; + +val _ = Define ` + ((vec_of_bit:int -> sail_values$bitU -> 'a words$word) len b= (maybe_failwith (vec_of_bit_maybe len b)))`; + + +(*val cast_bool_vec : bool -> Machine_word.mword Machine_word.ty1*) +val _ = Define ` + ((cast_bool_vec:bool ->(1)words$word) b= (vec_of_bool(( 1 : int)) b))`; + +val _ = Define ` + ((cast_unit_vec_maybe:sail_values$bitU ->('a words$word)option) b= (vec_of_bit_maybe(( 1 : int)) b))`; + +val _ = Define ` + ((cast_unit_vec_fail:sail_values$bitU -> 'a state_monad$sequential_state ->((((1)words$word),'b)state_monad$result#'a state_monad$sequential_state)set) b= (state_monad$bindS (state$bool_of_bitU_fail b) (\ b . state_monad$returnS (cast_bool_vec b))))`; + +val _ = Define ` + ((cast_unit_vec_oracle:sail_values$bitU -> 'a state_monad$sequential_state ->((((1)words$word),'b)state_monad$result#'a state_monad$sequential_state)set) b= (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b . state_monad$returnS (cast_bool_vec b))))`; + +val _ = Define ` + ((cast_unit_vec:sail_values$bitU -> 'a words$word) b= (maybe_failwith (cast_unit_vec_maybe b)))`; + + +(*val msb : forall 'a. Size 'a => Machine_word.mword 'a -> Sail_values.bitU*) +val _ = Define ` + ((msb:'a words$word -> sail_values$bitU)= + (most_significant instance_Sail_values_Bitvector_Machine_word_mword_dict))`; + + +(*val int_of_vec : forall 'a. Size 'a => bool -> Machine_word.mword 'a -> Num.integer*) +val _ = Define ` + ((int_of_vec:bool -> 'a words$word -> int) sign w= + (if sign + then integer_word$w2i w + else lem$w2ui w))`; + +val _ = Define ` + ((int_of_vec_maybe:bool -> 'a words$word ->(int)option) sign w= (SOME (int_of_vec sign w)))`; + +val _ = Define ` + ((int_of_vec_fail:bool -> 'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) sign w= (state_monad$returnS (int_of_vec sign w)))`; + + +(*val string_of_vec : forall 'a. Size 'a => Machine_word.mword 'a -> string*) +val _ = Define ` + ((string_of_vec:'a words$word -> string)= + (string_of_bv instance_Sail_values_Bitvector_Machine_word_mword_dict))`; + + +(*val and_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val or_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val xor_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val not_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a*) +val _ = Define ` + ((and_vec:'a words$word -> 'a words$word -> 'a words$word)= words$word_and)`; + +val _ = Define ` + ((or_vec:'a words$word -> 'a words$word -> 'a words$word)= words$word_or)`; + +val _ = Define ` + ((xor_vec:'a words$word -> 'a words$word -> 'a words$word)= words$word_xor)`; + +val _ = Define ` + ((not_vec:'a words$word -> 'a words$word)= words$word_1comp)`; + + +(*val add_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val adds_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val sub_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val subs_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val mult_vec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'b*) +(*val mults_vec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'b*) +val _ = Define ` + ((add_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (integer_word$i2w ((int_of_mword F l) + (int_of_mword F r))))`; + +val _ = Define ` + ((adds_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (integer_word$i2w ((int_of_mword T l) + (int_of_mword T r))))`; + +val _ = Define ` + ((sub_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (integer_word$i2w ((int_of_mword F l) - (int_of_mword F r))))`; + +val _ = Define ` + ((subs_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (integer_word$i2w ((int_of_mword T l) - (int_of_mword T r))))`; + +val _ = Define ` + ((mult_vec:'a words$word -> 'a words$word -> 'b words$word) l r= (integer_word$i2w ((int_of_mword F (words$w2w l : 'b words$word)) * (int_of_mword F (words$w2w r : 'b words$word)))))`; + +val _ = Define ` + ((mults_vec:'a words$word -> 'a words$word -> 'b words$word) l r= (integer_word$i2w ((int_of_mword T (words$sw2sw l : 'b words$word)) * (int_of_mword T (words$sw2sw r : 'b words$word)))))`; + + +(*val add_vec_int : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val adds_vec_int : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val sub_vec_int : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val subs_vec_int : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*) +(*val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((add_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict (+) F l r))`; + +val _ = Define ` + ((adds_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict (+) T l r))`; + +val _ = Define ` + ((sub_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict (-) F l r))`; + +val _ = Define ` + ((subs_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict (-) T l r))`; + +val _ = Define ` + ((mult_vec_int:'a words$word -> int -> 'b words$word) l r= (arith_op_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict ( * ) F (words$w2w l : 'b words$word) r))`; + +val _ = Define ` + ((mults_vec_int:'a words$word -> int -> 'b words$word) l r= (arith_op_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict ( * ) T (words$sw2sw l : 'b words$word) r))`; + + +(*val add_int_vec : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val adds_int_vec : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val sub_int_vec : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val subs_int_vec : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*) +(*val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*) +val _ = Define ` + ((add_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict (+) F l r))`; + +val _ = Define ` + ((adds_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict (+) T l r))`; + +val _ = Define ` + ((sub_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict (-) F l r))`; + +val _ = Define ` + ((subs_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict (-) T l r))`; + +val _ = Define ` + ((mult_int_vec:int -> 'a words$word -> 'b words$word) l r= (arith_op_int_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict ( * ) F l (words$w2w r : 'b words$word)))`; + +val _ = Define ` + ((mults_int_vec:int -> 'a words$word -> 'b words$word) l r= (arith_op_int_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict ( * ) T l (words$sw2sw r : 'b words$word)))`; + + +(*val add_vec_bool : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*) +(*val adds_vec_bool : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*) +(*val sub_vec_bool : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*) +(*val subs_vec_bool : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*) + +val _ = Define ` + ((add_vec_bool:'a words$word -> bool -> 'a words$word) l r= (arith_op_bv_bool + instance_Sail_values_Bitvector_Machine_word_mword_dict (+) F l r))`; + +val _ = Define ` + ((add_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option) l r= (OPTION_MAP (add_vec_bool l) (bool_of_bitU r)))`; + +val _ = Define ` + ((add_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_fail r) (\ r . state_monad$returnS (add_vec_bool l r))))`; + +val _ = Define ` + ((add_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (add_vec_bool l r))))`; + +val _ = Define ` + ((add_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word) l r= (maybe_failwith (add_vec_bit_maybe l r)))`; + + +val _ = Define ` + ((adds_vec_bool:'a words$word -> bool -> 'a words$word) l r= (arith_op_bv_bool + instance_Sail_values_Bitvector_Machine_word_mword_dict (+) T l r))`; + +val _ = Define ` + ((adds_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option) l r= (OPTION_MAP (adds_vec_bool l) (bool_of_bitU r)))`; + +val _ = Define ` + ((adds_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_fail r) (\ r . state_monad$returnS (adds_vec_bool l r))))`; + +val _ = Define ` + ((adds_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (adds_vec_bool l r))))`; + +val _ = Define ` + ((adds_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word) l r= (maybe_failwith (adds_vec_bit_maybe l r)))`; + + +val _ = Define ` + ((sub_vec_bool:'a words$word -> bool -> 'a words$word) l r= (arith_op_bv_bool + instance_Sail_values_Bitvector_Machine_word_mword_dict (-) F l r))`; + +val _ = Define ` + ((sub_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option) l r= (OPTION_MAP (sub_vec_bool l) (bool_of_bitU r)))`; + +val _ = Define ` + ((sub_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_fail r) (\ r . state_monad$returnS (sub_vec_bool l r))))`; + +val _ = Define ` + ((sub_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (sub_vec_bool l r))))`; + +val _ = Define ` + ((sub_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word) l r= (maybe_failwith (sub_vec_bit_maybe l r)))`; + + +val _ = Define ` + ((subs_vec_bool:'a words$word -> bool -> 'a words$word) l r= (arith_op_bv_bool + instance_Sail_values_Bitvector_Machine_word_mword_dict (-) T l r))`; + +val _ = Define ` + ((subs_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option) l r= (OPTION_MAP (subs_vec_bool l) (bool_of_bitU r)))`; + +val _ = Define ` + ((subs_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_fail r) (\ r . state_monad$returnS (subs_vec_bool l r))))`; + +val _ = Define ` + ((subs_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r= (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r . state_monad$returnS (subs_vec_bool l r))))`; + +val _ = Define ` + ((subs_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word) l r= (maybe_failwith (subs_vec_bit_maybe l r)))`; + + +(* TODO +val maybe_mword_of_bits_overflow : forall 'a. Size 'a => (list bitU * bitU * bitU) -> maybe (mword 'a * bitU * bitU) +let maybe_mword_of_bits_overflow (bits, overflow, carry) = + Maybe.map (fun w -> (w, overflow, carry)) (of_bits bits) + +val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val adds_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val subs_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val mults_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +let add_overflow_vec l r = maybe_mword_of_bits_overflow (add_overflow_bv l r) +let adds_overflow_vec l r = maybe_mword_of_bits_overflow (adds_overflow_bv l r) +let sub_overflow_vec l r = maybe_mword_of_bits_overflow (sub_overflow_bv l r) +let subs_overflow_vec l r = maybe_mword_of_bits_overflow (subs_overflow_bv l r) +let mult_overflow_vec l r = maybe_mword_of_bits_overflow (mult_overflow_bv l r) +let mults_overflow_vec l r = maybe_mword_of_bits_overflow (mults_overflow_bv l r) + +val add_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) +val add_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) +val sub_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) +val sub_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) +let add_overflow_vec_bit = add_overflow_bv_bit +let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed +let sub_overflow_vec_bit = sub_overflow_bv_bit +let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*) + +(*val shiftl : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val shiftr : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val arith_shiftr : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val rotl : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val rotr : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +val _ = Define ` + ((shiftl:'a words$word -> int -> 'a words$word)= shiftl_mword)`; + +val _ = Define ` + ((shiftr:'a words$word -> int -> 'a words$word)= shiftr_mword)`; + +val _ = Define ` + ((arith_shiftr:'a words$word -> int -> 'a words$word)= arith_shiftr_mword)`; + +val _ = Define ` + ((rotl:'a words$word -> int -> 'a words$word)= rotl_mword)`; + +val _ = Define ` + ((rotr:'a words$word -> int -> 'a words$word)= rotr_mword)`; + + +(*val mod_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val mod_vec_maybe : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Maybe.maybe (Machine_word.mword 'a)*) +(*val mod_vec_fail : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val mod_vec_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +val _ = Define ` + ((mod_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (mod_mword l r))`; + +val _ = Define ` + ((mod_vec_maybe:'a words$word -> 'a words$word ->('a words$word)option) l r= (mod_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`; + +val _ = Define ` + ((mod_vec_fail:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "mod_vec" (mod_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`; + +val _ = Define ` + ((mod_vec_oracle:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= + ((case (mod_bv instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of + SOME w => state_monad$returnS w + | NONE => state$mword_oracleS () + )))`; + + +(*val quot_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val quot_vec_maybe : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Maybe.maybe (Machine_word.mword 'a)*) +(*val quot_vec_fail : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val quot_vec_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +val _ = Define ` + ((quot_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (quot_mword l r))`; + +val _ = Define ` + ((quot_vec_maybe:'a words$word -> 'a words$word ->('a words$word)option) l r= (quot_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`; + +val _ = Define ` + ((quot_vec_fail:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "quot_vec" (quot_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`; + +val _ = Define ` + ((quot_vec_oracle:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= + ((case (quot_bv instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of + SOME w => state_monad$returnS w + | NONE => state$mword_oracleS () + )))`; + + +(*val quots_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*) +(*val quots_vec_maybe : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Maybe.maybe (Machine_word.mword 'a)*) +(*val quots_vec_fail : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val quots_vec_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +val _ = Define ` + ((quots_vec:'a words$word -> 'a words$word -> 'a words$word) l r= (quots_mword l r))`; + +val _ = Define ` + ((quots_vec_maybe:'a words$word -> 'a words$word ->('a words$word)option) l r= (quots_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`; + +val _ = Define ` + ((quots_vec_fail:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "quots_vec" (quots_bv + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`; + +val _ = Define ` + ((quots_vec_oracle:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= + ((case (quots_bv instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of + SOME w => state_monad$returnS w + | NONE => state$mword_oracleS () + )))`; + + +(*val mod_vec_int : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val mod_vec_int_maybe : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Maybe.maybe (Machine_word.mword 'a)*) +(*val mod_vec_int_fail : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val mod_vec_int_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +val _ = Define ` + ((mod_vec_int:'a words$word -> int -> 'a words$word) l r= (mod_mword_int l r))`; + +val _ = Define ` + ((mod_vec_int_maybe:'a words$word -> int ->('a words$word)option) l r= (mod_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`; + +val _ = Define ` + ((mod_vec_int_fail:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "mod_vec_int" (mod_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`; + +val _ = Define ` + ((mod_vec_int_oracle:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= + ((case (mod_bv_int instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of + SOME w => state_monad$returnS w + | NONE => state$mword_oracleS () + )))`; + + +(*val quot_vec_int : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*) +(*val quot_vec_int_maybe : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Maybe.maybe (Machine_word.mword 'a)*) +(*val quot_vec_int_fail : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +(*val quot_vec_int_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*) +val _ = Define ` + ((quot_vec_int:'a words$word -> int -> 'a words$word) l r= (quot_mword_int l r))`; + +val _ = Define ` + ((quot_vec_int_maybe:'a words$word -> int ->('a words$word)option) l r= (quot_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`; + +val _ = Define ` + ((quot_vec_int_fail:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= (state_monad$maybe_failS "quot_vec_int" (quot_bv_int + instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`; + +val _ = Define ` + ((quot_vec_int_oracle:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r= + ((case (quot_bv_int instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of + SOME w => state_monad$returnS w + | NONE => state$mword_oracleS () + )))`; + + +(*val replicate_bits : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((replicate_bits:'a words$word -> int -> 'b words$word) v count1= (bitstring$v2w (repeat (bitstring$w2v v) count1)))`; + + +(*val duplicate_bool : forall 'a. Size 'a => bool -> Num.integer -> Machine_word.mword 'a*) +val _ = Define ` + ((duplicate_bool:bool -> int -> 'a words$word) b n= (bitstring$v2w (repeat [b] n)))`; + +val _ = Define ` + ((duplicate_maybe:sail_values$bitU -> int ->('a words$word)option) b n= (OPTION_MAP (\ b . duplicate_bool b n) (bool_of_bitU b)))`; + +val _ = Define ` + ((duplicate_fail:sail_values$bitU -> int -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) b n= (state_monad$bindS (state$bool_of_bitU_fail b) (\ b . state_monad$returnS (duplicate_bool b n))))`; + +val _ = Define ` + ((duplicate_oracle:sail_values$bitU -> int -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) b n= (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b . state_monad$returnS (duplicate_bool b n))))`; + +val _ = Define ` + ((duplicate:sail_values$bitU -> int -> 'a words$word) b n= (maybe_failwith (duplicate_maybe b n)))`; + + +(*val reverse_endianness : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a*) +val _ = Define ` + ((reverse_endianness:'a words$word -> 'a words$word) v= (bitstring$v2w (reverse_endianness_list (bitstring$w2v v))))`; + + +(*val eq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val neq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val ult_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val slt_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val ugt_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val sgt_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val ulteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val slteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val ugteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +(*val sgteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*) +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/sail_valuesScript.sml b/snapshots/hol4/sail/lib/hol/sail_valuesScript.sml new file mode 100644 index 00000000..2d6c019a --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/sail_valuesScript.sml @@ -0,0 +1,1238 @@ +(*Generated by Lem from ../../src/gen_lib/sail_values.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory lem_machine_wordTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "sail_values" + +(*open import Pervasives_extra*) +(*open import Machine_word*) +(*open import Sail_impl_base*) + + +val _ = type_abbrev( "ii" , ``: int``); +val _ = type_abbrev( "nn" , ``: num``); + +(*val nat_of_int : Num.integer -> nat*) +val _ = Define ` + ((nat_of_int:int -> num) i= (if i <( 0 : int) then( 0 : num) else Num (ABS (I i))))`; + + +(*val pow : Num.integer -> Num.integer -> Num.integer*) +val _ = Define ` + ((pow0:int -> int -> int) m n= (m ** (nat_of_int n)))`; + + +val _ = Define ` + ((pow2:int -> int) n= (pow0(( 2 : int)) n))`; + + +(*val eq : forall 'a. Eq 'a => 'a -> 'a -> bool*) + +(*val neq : forall 'a. Eq 'a => 'a -> 'a -> bool*) + +(*let add_int l r = integerAdd l r +let add_signed l r = integerAdd l r +let sub_int l r = integerMinus l r +let mult_int l r = integerMult l r +let div_int l r = integerDiv l r +let div_nat l r = natDiv l r +let power_int_nat l r = integerPow l r +let power_int_int l r = integerPow l (nat_of_int r) +let negate_int i = integerNegate i +let min_int l r = integerMin l r +let max_int l r = integerMax l r + +let add_real l r = realAdd l r +let sub_real l r = realMinus l r +let mult_real l r = realMult l r +let div_real l r = realDiv l r +let negate_real r = realNegate r +let abs_real r = realAbs r +let power_real b e = realPowInteger b e*) + +(*val prerr_endline : string -> unit*) +val _ = Define ` + ((prerr_endline:string -> unit) _= () )`; + + +(*val print_int : string -> Num.integer -> unit*) +val _ = Define ` + ((print_int:string -> int -> unit) msg i= (prerr_endline ( STRCAT msg (stringFromInteger i))))`; + + +(*val putchar : Num.integer -> unit*) +val _ = Define ` + ((putchar:int -> unit) _= () )`; + + +(*val shr_int : ii -> ii -> ii*) + val shr_int_defn = Hol_defn "shr_int" ` + ((shr_int:int -> int -> int) x s= (if s >( 0 : int) then shr_int (x /( 2 : int)) (s -( 1 : int)) else x))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn shr_int_defn; + +(*val shl_int : Num.integer -> Num.integer -> Num.integer*) + val shl_int_defn = Hol_defn "shl_int" ` + ((shl_int:int -> int -> int) i shift= (if shift >( 0 : int) then( 2 : int) * shl_int i (shift -( 1 : int)) else i))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn shl_int_defn; +val _ = Define ` + ((take_list:int -> 'a list -> 'a list) n xs= (TAKE (nat_of_int n) xs))`; + +val _ = Define ` + ((drop_list:int -> 'a list -> 'a list) n xs= (DROP (nat_of_int n) xs))`; + + +(*val repeat : forall 'a. list 'a -> Num.integer -> list 'a*) + val repeat_defn = Hol_defn "repeat" ` + ((repeat:'a list -> int -> 'a list) xs n= + (if n <=( 0 : int) then [] + else xs ++ repeat xs (n -( 1 : int))))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn repeat_defn; + +val _ = Define ` + ((duplicate_to_list:'a -> int -> 'a list) bit length= (repeat [bit] length))`; + + + val replace_defn = Hol_defn "replace" ` + ((replace:'a list -> int -> 'a -> 'a list) bs (n : int) b'= ((case bs of + [] => [] + | b :: bs => + if n =( 0 : int) then b' :: bs + else b :: replace bs (n -( 1 : int)) b' + )))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn replace_defn; + +val _ = Define ` + ((upper:'a -> 'a) n= n)`; + + +(* Modulus operation corresponding to quot below -- result + has sign of dividend. *) +val _ = Define ` + ((hardware_mod:int -> int -> int) (a: int) (b:int) : int= + (let m = ((ABS a) % (ABS b)) in + if a <( 0 : int) then ~ m else m))`; + + +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) +val _ = Define ` + ((hardware_quot:int -> int -> int) (a:int) (b:int) : int= + (let q = ((ABS a) / (ABS b)) in + if ((a<( 0 : int)) <=> (b<( 0 : int))) then + q (* same sign -- result positive *) + else + ~ q))`; + (* different sign -- result negative *) + +val _ = Define ` + ((max_64u:int)= (((( 2 : int))**(( 64 : num))) -( 1 : int)))`; + +val _ = Define ` + ((max_64:int)= (((( 2 : int))**(( 63 : num))) -( 1 : int)))`; + +val _ = Define ` + ((min_64:int)= (( 0 : int) - ((( 2 : int))**(( 63 : num)))))`; + +val _ = Define ` + ((max_32u:int)= ((( 4294967295 : int) : int)))`; + +val _ = Define ` + ((max_32:int)= ((( 2147483647 : int) : int)))`; + +val _ = Define ` + ((min_32:int)= ((( 0 : int) -( 2147483648 : int) : int)))`; + +val _ = Define ` + ((max_8:int)= ((( 127 : int) : int)))`; + +val _ = Define ` + ((min_8:int)= ((( 0 : int) -( 128 : int) : int)))`; + +val _ = Define ` + ((max_5:int)= ((( 31 : int) : int)))`; + +val _ = Define ` + ((min_5:int)= ((( 0 : int) -( 32 : int) : int)))`; + + +(* just_list takes a list of maybes and returns Just xs if all elements have + a value, and Nothing if one of the elements is Nothing. *) +(*val just_list : forall 'a. list (Maybe.maybe 'a) -> Maybe.maybe (list 'a)*) + val just_list_defn = Hol_defn "just_list" ` + ((just_list:('a option)list ->('a list)option) l= ((case l of + [] => SOME [] + | (x :: xs) => + (case (x, just_list xs) of + (SOME x, SOME xs) => SOME (x :: xs) + | (_, _) => NONE + ) + )))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn just_list_defn; + +(*val maybe_failwith : forall 'a. Maybe.maybe 'a -> 'a*) +val _ = Define ` + ((maybe_failwith:'a option -> 'a)= + (\x . (case x of SOME a => a | NONE => failwith "maybe_failwith" )))`; + + +(*** Bits *) +val _ = Hol_datatype ` + bitU = B0 | B1 | BU`; + + +val _ = Define ` + ((showBitU:bitU -> string)= + (\x . (case x of B0 => "O" | B1 => "I" | BU => "U" )))`; + + +val _ = Define ` + ((bitU_char:bitU -> char)= + (\x . (case x of B0 => #"0" | B1 => #"1" | BU => #"?" )))`; + + +val _ = Define ` +((instance_Show_Show_Sail_values_bitU_dict:(bitU)lem_show$Show_class)= (<| + + show_method := showBitU|>))`; + + +(*val compare_bitU : bitU -> bitU -> Basic_classes.ordering*) +val _ = Define ` + ((compare_bitU:bitU -> bitU -> lem_basic_classes$ordering) l r= ((case (l, r) of + (BU, BU) => EQ + | (B0, B0) => EQ + | (B1, B1) => EQ + | (BU, _) => LT + | (_, BU) => GT + | (B0, _) => LT + | (_, _) => GT +)))`; + + +val _ = Define ` +((instance_Basic_classes_Ord_Sail_values_bitU_dict:(bitU)lem_basic_classes$Ord_class)= (<| + + compare_method := compare_bitU; + + isLess_method := (\ l r. (compare_bitU l r) = LT); + + isLessEqual_method := (\ l r. (compare_bitU l r) <> GT); + + isGreater_method := (\ l r. (compare_bitU l r) = GT); + + isGreaterEqual_method := (\ l r. (compare_bitU l r) <> LT)|>))`; + + +val _ = Hol_datatype ` +(* 'a *) BitU_class= <| + to_bitU_method : 'a -> bitU; + of_bitU_method : bitU -> 'a +|>`; + + +val _ = Define ` +((instance_Sail_values_BitU_Sail_values_bitU_dict:(bitU)BitU_class)= (<| + + to_bitU_method := (\ b. b); + + of_bitU_method := (\ b. b)|>))`; + + +val _ = Define ` + ((bool_of_bitU:bitU ->(bool)option)= + (\x . (case x of B0 => SOME F | B1 => SOME T | BU => NONE )))`; + + +val _ = Define ` + ((bitU_of_bool:bool -> bitU) b= (if b then B1 else B0))`; + + +(*instance (BitU bool) + let to_bitU = bitU_of_bool + let of_bitU = bool_of_bitU +end*) + +val _ = Define ` + ((cast_bit_bool:bitU ->(bool)option)= bool_of_bitU)`; + + +val _ = Define ` + ((not_bit:bitU -> bitU)= + (\x . (case x of B1 => B0 | B0 => B1 | BU => BU )))`; + + +(*val is_one : Num.integer -> bitU*) +val _ = Define ` + ((is_one:int -> bitU) i= + (if i =( 1 : int) then B1 else B0))`; + + +(*val and_bit : bitU -> bitU -> bitU*) +val _ = Define ` + ((and_bit:bitU -> bitU -> bitU) x y= + ((case (x, y) of + (B0, _) => B0 + | (_, B0) => B0 + | (B1, B1) => B1 + | (_, _) => BU + )))`; + + +(*val or_bit : bitU -> bitU -> bitU*) +val _ = Define ` + ((or_bit:bitU -> bitU -> bitU) x y= + ((case (x, y) of + (B1, _) => B1 + | (_, B1) => B1 + | (B0, B0) => B0 + | (_, _) => BU + )))`; + + +(*val xor_bit : bitU -> bitU -> bitU*) +val _ = Define ` + ((xor_bit:bitU -> bitU -> bitU) x y= +((case (x, y) of + (B0, B0) => B0 + | (B0, B1) => B1 + | (B1, B0) => B1 + | (B1, B1) => B0 + | (_, _) => BU + )))`; + + +(*val &. : bitU -> bitU -> bitU*) + +(*val |. : bitU -> bitU -> bitU*) + +(*val +. : bitU -> bitU -> bitU*) + + +(*** Bool lists ***) + +(*val bools_of_nat_aux : Num.integer -> Num.natural -> list bool -> list bool*) + val bools_of_nat_aux_defn = Hol_defn "bools_of_nat_aux" ` + ((bools_of_nat_aux:int -> num ->(bool)list ->(bool)list) len x acc= + (if len <=( 0 : int) then acc + else bools_of_nat_aux (len -( 1 : int)) (x DIV( 2:num)) ((if (x MOD( 2:num)) =( 1:num) then T else F) :: acc)))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn bools_of_nat_aux_defn; +val _ = Define ` + ((bools_of_nat:int -> num ->(bool)list) len n= (bools_of_nat_aux len n []))`; + (*List.reverse (bools_of_nat_aux n)*) + +(*val nat_of_bools_aux : Num.natural -> list bool -> Num.natural*) + val nat_of_bools_aux_defn = Hol_defn "nat_of_bools_aux" ` + ((nat_of_bools_aux:num ->(bool)list -> num) acc bs= ((case bs of + [] => acc + | T :: bs => nat_of_bools_aux ((( 2:num) * acc) +( 1:num)) bs + | F :: bs => nat_of_bools_aux (( 2:num) * acc) bs +)))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn nat_of_bools_aux_defn; +val _ = Define ` + ((nat_of_bools:(bool)list -> num) bs= (nat_of_bools_aux(( 0:num)) bs))`; + + +(*val unsigned_of_bools : list bool -> Num.integer*) +val _ = Define ` + ((unsigned_of_bools:(bool)list -> int) bs= (int_of_num (nat_of_bools bs)))`; + + +(*val signed_of_bools : list bool -> Num.integer*) +val _ = Define ` + ((signed_of_bools:(bool)list -> int) bs= + ((case bs of + T :: _ =>( 0 : int) - (( 1 : int) + (unsigned_of_bools (MAP (\ x. ~ x) bs))) + | F :: _ => unsigned_of_bools bs + | [] =>( 0 : int) (* Treat empty list as all zeros *) + )))`; + + +(*val int_of_bools : bool -> list bool -> Num.integer*) +val _ = Define ` + ((int_of_bools:bool ->(bool)list -> int) sign bs= (if sign then signed_of_bools bs else unsigned_of_bools bs))`; + + +(*val pad_list : forall 'a. 'a -> list 'a -> Num.integer -> list 'a*) + val pad_list_defn = Hol_defn "pad_list" ` + ((pad_list:'a -> 'a list -> int -> 'a list) x xs n= + (if n <=( 0 : int) then xs else pad_list x (x :: xs) (n -( 1 : int))))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn pad_list_defn; + +val _ = Define ` + ((ext_list:'a -> int -> 'a list -> 'a list) pad len xs= + (let longer = (len - (int_of_num (LENGTH xs))) in + if longer <( 0 : int) then DROP (nat_of_int (ABS (longer))) xs + else pad_list pad xs longer))`; + + +val _ = Define ` + ((extz_bools:int ->(bool)list ->(bool)list) len bs= (ext_list F len bs))`; + +val _ = Define ` + ((exts_bools:int ->(bool)list ->(bool)list) len bs= + ((case bs of + T :: _ => ext_list T len bs + | _ => ext_list F len bs + )))`; + + + val add_one_bool_ignore_overflow_aux_defn = Hol_defn "add_one_bool_ignore_overflow_aux" ` + ((add_one_bool_ignore_overflow_aux:(bool)list ->(bool)list) bits= ((case bits of + [] => [] + | F :: bits => T :: bits + | T :: bits => F :: add_one_bool_ignore_overflow_aux bits +)))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn add_one_bool_ignore_overflow_aux_defn; + +val _ = Define ` + ((add_one_bool_ignore_overflow:(bool)list ->(bool)list) bits= + (REVERSE (add_one_bool_ignore_overflow_aux (REVERSE bits))))`; + + +(*let bool_list_of_int n = + let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in + if n >= (0 : integer) then bs_abs + else add_one_bool_ignore_overflow (List.map not bs_abs) +let bools_of_int len n = exts_bools len (bool_list_of_int n)*) +val _ = Define ` + ((bools_of_int:int -> int ->(bool)list) len n= + (let bs_abs = (bools_of_nat len (Num (ABS (ABS n)))) in + if n >= (( 0 : int) : int) then bs_abs + else add_one_bool_ignore_overflow (MAP (\ x. ~ x) bs_abs)))`; + + +(*** Bit lists ***) + +(*val has_undefined_bits : list bitU -> bool*) +val _ = Define ` + ((has_undefined_bits:(bitU)list -> bool) bs= (EXISTS (\x . + (case x of BU => T | _ => F )) bs))`; + + +val _ = Define ` + ((bits_of_nat:int -> num ->(bitU)list) len n= (MAP bitU_of_bool (bools_of_nat len n)))`; + + +val _ = Define ` + ((nat_of_bits:(bitU)list ->(num)option) bits= + ((case (just_list (MAP bool_of_bitU bits)) of + SOME bs => SOME (nat_of_bools bs) + | NONE => NONE + )))`; + + +val _ = Define ` + ((not_bits:(bitU)list ->(bitU)list)= (MAP not_bit))`; + + +(*val binop_list : forall 'a. ('a -> 'a -> 'a) -> list 'a -> list 'a -> list 'a*) +val _ = Define ` + ((binop_list:('a -> 'a -> 'a) -> 'a list -> 'a list -> 'a list) op xs ys= + (FOLDR (\ (x, y) acc . op x y :: acc) [] (list_combine xs ys)))`; + + +val _ = Define ` + ((unsigned_of_bits:(bitU)list ->(int)option) bits= + ((case (just_list (MAP bool_of_bitU bits)) of + SOME bs => SOME (unsigned_of_bools bs) + | NONE => NONE + )))`; + + +val _ = Define ` + ((signed_of_bits:(bitU)list ->(int)option) bits= + ((case (just_list (MAP bool_of_bitU bits)) of + SOME bs => SOME (signed_of_bools bs) + | NONE => NONE + )))`; + + +(*val int_of_bits : bool -> list bitU -> Maybe.maybe Num.integer*) +val _ = Define ` + ((int_of_bits:bool ->(bitU)list ->(int)option) sign bs= (if sign then signed_of_bits bs else unsigned_of_bits bs))`; + + +val _ = Define ` + ((extz_bits:int ->(bitU)list ->(bitU)list) len bits= (ext_list B0 len bits))`; + +val _ = Define ` + ((exts_bits:int ->(bitU)list ->(bitU)list) len bits= + ((case bits of + BU :: _ => ext_list BU len bits + | B1 :: _ => ext_list B1 len bits + | _ => ext_list B0 len bits + )))`; + + + val add_one_bit_ignore_overflow_aux_defn = Hol_defn "add_one_bit_ignore_overflow_aux" ` + ((add_one_bit_ignore_overflow_aux:(bitU)list ->(bitU)list) bits= ((case bits of + [] => [] + | B0 :: bits => B1 :: bits + | B1 :: bits => B0 :: add_one_bit_ignore_overflow_aux bits + | BU :: bits => BU :: MAP (\b . + (case (b ) of ( _ ) => BU )) bits +)))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn add_one_bit_ignore_overflow_aux_defn; + +val _ = Define ` + ((add_one_bit_ignore_overflow:(bitU)list ->(bitU)list) bits= + (REVERSE (add_one_bit_ignore_overflow_aux (REVERSE bits))))`; + + +(*let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n) +let bits_of_int len n = exts_bits len (bit_list_of_int n)*) +val _ = Define ` + ((bits_of_int:int -> int ->(bitU)list) len n= (MAP bitU_of_bool (bools_of_int len n)))`; + + +(*val arith_op_bits : + (Num.integer -> Num.integer -> Num.integer) -> bool -> list bitU -> list bitU -> list bitU*) +val _ = Define ` + ((arith_op_bits:(int -> int -> int) -> bool ->(bitU)list ->(bitU)list ->(bitU)list) op sign l r= + ((case (int_of_bits sign l, int_of_bits sign r) of + (SOME li, SOME ri) => bits_of_int (int_of_num (LENGTH l)) (op li ri) + | (_, _) => repeat [BU] (int_of_num (LENGTH l)) + )))`; + + +val _ = Define ` + ((char_of_nibble:bitU#bitU#bitU#bitU ->(char)option)= + (\x . (case x of + (B0, B0, B0, B0) => SOME #"0" + | (B0, B0, B0, B1) => SOME #"1" + | (B0, B0, B1, B0) => SOME #"2" + | (B0, B0, B1, B1) => SOME #"3" + | (B0, B1, B0, B0) => SOME #"4" + | (B0, B1, B0, B1) => SOME #"5" + | (B0, B1, B1, B0) => SOME #"6" + | (B0, B1, B1, B1) => SOME #"7" + | (B1, B0, B0, B0) => SOME #"8" + | (B1, B0, B0, B1) => SOME #"9" + | (B1, B0, B1, B0) => SOME #"A" + | (B1, B0, B1, B1) => SOME #"B" + | (B1, B1, B0, B0) => SOME #"C" + | (B1, B1, B0, B1) => SOME #"D" + | (B1, B1, B1, B0) => SOME #"E" + | (B1, B1, B1, B1) => SOME #"F" + | _ => NONE + )))`; + + + val hexstring_of_bits_defn = Hol_defn "hexstring_of_bits" ` + ((hexstring_of_bits:(bitU)list ->((char)list)option) bs= ((case bs of + b1 :: b2 :: b3 :: b4 :: bs => + let n = (char_of_nibble (b1, b2, b3, b4)) in + let s = (hexstring_of_bits bs) in + (case (n, s) of + (SOME n, SOME s) => SOME (n :: s) + | _ => NONE + ) + | _ => NONE + )))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn hexstring_of_bits_defn; + +val _ = Define ` + ((show_bitlist:(bitU)list -> string) bs= + ((case hexstring_of_bits bs of + SOME s => IMPLODE (#"0" :: (#"x" :: s)) + | NONE => IMPLODE (#"0" :: (#"b" :: MAP bitU_char bs)) + )))`; + + +(*val subrange_list_inc : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a*) +val _ = Define ` + ((subrange_list_inc:'a list -> int -> int -> 'a list) xs i j= + (let (toJ,suffix0) = (TAKE (nat_of_int (j +( 1 : int))) xs, DROP (nat_of_int (j +( 1 : int))) xs) in + let (prefix0,fromItoJ) = (TAKE (nat_of_int i) toJ, DROP (nat_of_int i) toJ) in + fromItoJ))`; + + +(*val subrange_list_dec : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a*) +val _ = Define ` + ((subrange_list_dec:'a list -> int -> int -> 'a list) xs i j= + (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in + subrange_list_inc xs (top - i) (top - j)))`; + + +(*val subrange_list : forall 'a. bool -> list 'a -> Num.integer -> Num.integer -> list 'a*) +val _ = Define ` + ((subrange_list:bool -> 'a list -> int -> int -> 'a list) is_inc xs i j= (if is_inc then subrange_list_inc xs i j else subrange_list_dec xs i j))`; + + +(*val update_subrange_list_inc : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a -> list 'a*) +val _ = Define ` + ((update_subrange_list_inc:'a list -> int -> int -> 'a list -> 'a list) xs i j xs'= + (let (toJ,suffix) = (TAKE (nat_of_int (j +( 1 : int))) xs, DROP (nat_of_int (j +( 1 : int))) xs) in + let (prefix,fromItoJ0) = (TAKE (nat_of_int i) toJ, DROP (nat_of_int i) toJ) in +(prefix ++ xs') ++ suffix))`; + + +(*val update_subrange_list_dec : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a -> list 'a*) +val _ = Define ` + ((update_subrange_list_dec:'a list -> int -> int -> 'a list -> 'a list) xs i j xs'= + (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in + update_subrange_list_inc xs (top - i) (top - j) xs'))`; + + +(*val update_subrange_list : forall 'a. bool -> list 'a -> Num.integer -> Num.integer -> list 'a -> list 'a*) +val _ = Define ` + ((update_subrange_list:bool -> 'a list -> int -> int -> 'a list -> 'a list) is_inc xs i j xs'= + (if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs'))`; + + +(*val access_list_inc : forall 'a. list 'a -> Num.integer -> 'a*) +val _ = Define ` + ((access_list_inc:'a list -> int -> 'a) xs n= (EL (nat_of_int n) xs))`; + + +(*val access_list_dec : forall 'a. list 'a -> Num.integer -> 'a*) +val _ = Define ` + ((access_list_dec:'a list -> int -> 'a) xs n= + (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in + access_list_inc xs (top - n)))`; + + +(*val access_list : forall 'a. bool -> list 'a -> Num.integer -> 'a*) +val _ = Define ` + ((access_list:bool -> 'a list -> int -> 'a) is_inc xs n= + (if is_inc then access_list_inc xs n else access_list_dec xs n))`; + + +(*val update_list_inc : forall 'a. list 'a -> Num.integer -> 'a -> list 'a*) +val _ = Define ` + ((update_list_inc:'a list -> int -> 'a -> 'a list) xs n x= (LUPDATE x (nat_of_int n) xs))`; + + +(*val update_list_dec : forall 'a. list 'a -> Num.integer -> 'a -> list 'a*) +val _ = Define ` + ((update_list_dec:'a list -> int -> 'a -> 'a list) xs n x= + (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in + update_list_inc xs (top - n) x))`; + + +(*val update_list : forall 'a. bool -> list 'a -> Num.integer -> 'a -> list 'a*) +val _ = Define ` + ((update_list:bool -> 'a list -> int -> 'a -> 'a list) is_inc xs n x= + (if is_inc then update_list_inc xs n x else update_list_dec xs n x))`; + + +val _ = Define ` + ((extract_only_bit:(bitU)list -> bitU)= + (\x . (case x of [] => BU | [e] => e | _ => BU )))`; + + +(*** Machine words *) + +(*val length_mword : forall 'a. Machine_word.mword 'a -> Num.integer*) + +(*val slice_mword_dec : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((slice_mword_dec:'a words$word -> int -> int -> 'b words$word) w i j= (words$word_extract (nat_of_int j) (nat_of_int i) w))`; + + +(*val slice_mword_inc : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((slice_mword_inc:'a words$word -> int -> int -> 'b words$word) w i j= + (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in + slice_mword_dec w (top - i) (top - j)))`; + + +(*val slice_mword : forall 'a 'b. bool -> Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*) +val _ = Define ` + ((slice_mword:bool -> 'a words$word -> int -> int -> 'b words$word) is_inc w i j= (if is_inc then slice_mword_inc w i j else slice_mword_dec w i j))`; + + +(*val update_slice_mword_dec : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*) +val _ = Define ` + ((update_slice_mword_dec:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'= (words$bit_field_insert (nat_of_int j) (nat_of_int i) w' w))`; + + +(*val update_slice_mword_inc : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*) +val _ = Define ` + ((update_slice_mword_inc:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'= + (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in + update_slice_mword_dec w (top - i) (top - j) w'))`; + + +(*val update_slice_mword : forall 'a 'b. bool -> Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*) +val _ = Define ` + ((update_slice_mword:bool -> 'a words$word -> int -> int -> 'b words$word -> 'a words$word) is_inc w i j w'= + (if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w'))`; + + +(*val access_mword_dec : forall 'a. Machine_word.mword 'a -> Num.integer -> bitU*) +val _ = Define ` + ((access_mword_dec:'a words$word -> int -> bitU) w n= (bitU_of_bool (words$word_bit (nat_of_int n) w)))`; + + +(*val access_mword_inc : forall 'a. Machine_word.mword 'a -> Num.integer -> bitU*) +val _ = Define ` + ((access_mword_inc:'a words$word -> int -> bitU) w n= + (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in + access_mword_dec w (top - n)))`; + + +(*val access_mword : forall 'a. bool -> Machine_word.mword 'a -> Num.integer -> bitU*) +val _ = Define ` + ((access_mword:bool -> 'a words$word -> int -> bitU) is_inc w n= + (if is_inc then access_mword_inc w n else access_mword_dec w n))`; + + +(*val update_mword_bool_dec : forall 'a. Machine_word.mword 'a -> Num.integer -> bool -> Machine_word.mword 'a*) +val _ = Define ` + ((update_mword_bool_dec:'a words$word -> int -> bool -> 'a words$word) w n b= ($:+ (nat_of_int n) b w))`; + +val _ = Define ` + ((update_mword_dec:'a words$word -> int -> bitU ->('a words$word)option) w n b= (OPTION_MAP (update_mword_bool_dec w n) (bool_of_bitU b)))`; + + +(*val update_mword_bool_inc : forall 'a. Machine_word.mword 'a -> Num.integer -> bool -> Machine_word.mword 'a*) +val _ = Define ` + ((update_mword_bool_inc:'a words$word -> int -> bool -> 'a words$word) w n b= + (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in + update_mword_bool_dec w (top - n) b))`; + +val _ = Define ` + ((update_mword_inc:'a words$word -> int -> bitU ->('a words$word)option) w n b= (OPTION_MAP (update_mword_bool_inc w n) (bool_of_bitU b)))`; + + +(*val int_of_mword : forall 'a. bool -> Machine_word.mword 'a -> Num.integer*) +val _ = Define ` + ((int_of_mword:bool -> 'a words$word -> int) sign w= + (if sign then integer_word$w2i w else lem$w2ui w))`; + + +(* Translating between a type level number (itself 'n) and an integer *) + +val _ = Define ` + ((size_itself_int:'a itself -> int) x= (int_of_num (size_itself x)))`; + + +(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n), + the actual integer is ignored. *) + +(*val make_the_value : forall 'n. Num.integer -> Machine_word.itself 'n*) +val _ = Define ` + ((make_the_value:int -> 'n itself) _= the_value)`; + + +(*** Bitvectors *) + +val _ = Hol_datatype ` +(* 'a *) Bitvector_class= <| + bits_of_method : 'a -> bitU list; + (* We allow of_bits to be partial, as not all bitvector representations + support undefined bits *) + of_bits_method : bitU list -> 'a option; + of_bools_method : bool list -> 'a; + length_method : 'a -> int; + (* of_int: the first parameter specifies the desired length of the bitvector *) + of_int_method : int -> int -> 'a; + (* Conversion to integers is undefined if any bit is undefined *) + unsigned_method : 'a -> int option; + signed_method : 'a -> int option; + (* Lifting of integer operations to bitvectors: The boolean flag indicates + whether to treat the bitvectors as signed (true) or not (false). *) + arith_op_bv_method : (int -> int -> int) -> bool -> 'a -> 'a -> 'a +|>`; + + +(*val of_bits_failwith : forall 'a. Bitvector 'a => list bitU -> 'a*) +val _ = Define ` + ((of_bits_failwith:'a Bitvector_class ->(bitU)list -> 'a)dict_Sail_values_Bitvector_a bits= (maybe_failwith ( + dict_Sail_values_Bitvector_a.of_bits_method bits)))`; + + +val _ = Define ` + ((int_of_bv:'a Bitvector_class -> bool -> 'a ->(int)option)dict_Sail_values_Bitvector_a sign= (if sign then + dict_Sail_values_Bitvector_a.signed_method else dict_Sail_values_Bitvector_a.unsigned_method))`; + + +val _ = Define ` +((instance_Sail_values_Bitvector_list_dict:'a BitU_class ->('a list)Bitvector_class)dict_Sail_values_BitU_a= (<| + + bits_of_method := (\ v. MAP + dict_Sail_values_BitU_a.to_bitU_method v); + + of_bits_method := (\ v. SOME (MAP + dict_Sail_values_BitU_a.of_bitU_method v)); + + of_bools_method := (\ v. MAP + dict_Sail_values_BitU_a.of_bitU_method (MAP bitU_of_bool v)); + + length_method := (\ xs. int_of_num (LENGTH xs)); + + of_int_method := (\ len n. MAP + dict_Sail_values_BitU_a.of_bitU_method (bits_of_int len n)); + + unsigned_method := (\ v. unsigned_of_bits (MAP + dict_Sail_values_BitU_a.to_bitU_method v)); + + signed_method := (\ v. signed_of_bits (MAP + dict_Sail_values_BitU_a.to_bitU_method v)); + + arith_op_bv_method := (\ op sign l r. MAP + dict_Sail_values_BitU_a.of_bitU_method (arith_op_bits op sign (MAP + dict_Sail_values_BitU_a.to_bitU_method l) (MAP dict_Sail_values_BitU_a.to_bitU_method r)))|>))`; + + +val _ = Define ` +((instance_Sail_values_Bitvector_Machine_word_mword_dict:('a words$word)Bitvector_class)= (<| + + bits_of_method := (\ v. MAP bitU_of_bool (bitstring$w2v v)); + + of_bits_method := (\ v. OPTION_MAP bitstring$v2w (just_list (MAP bool_of_bitU v))); + + of_bools_method := (\ v. bitstring$v2w v); + + length_method := (\ v. int_of_num (words$word_len v)); + + of_int_method := (\i n . + (case (i ,n ) of ( _ , n ) => integer_word$i2w n )); + + unsigned_method := (\ v. SOME (lem$w2ui v)); + + signed_method := (\ v. SOME (integer_word$w2i v)); + + arith_op_bv_method := (\ op sign l r. integer_word$i2w (op (int_of_mword sign l) (int_of_mword sign r)))|>))`; + + +val _ = Define ` + ((access_bv_inc:'a Bitvector_class -> 'a -> int -> bitU)dict_Sail_values_Bitvector_a v n= (access_list T ( + dict_Sail_values_Bitvector_a.bits_of_method v) n))`; + +val _ = Define ` + ((access_bv_dec:'a Bitvector_class -> 'a -> int -> bitU)dict_Sail_values_Bitvector_a v n= (access_list F ( + dict_Sail_values_Bitvector_a.bits_of_method v) n))`; + + +val _ = Define ` + ((update_bv_inc:'a Bitvector_class -> 'a -> int -> bitU ->(bitU)list)dict_Sail_values_Bitvector_a v n b= (update_list T ( + dict_Sail_values_Bitvector_a.bits_of_method v) n b))`; + +val _ = Define ` + ((update_bv_dec:'a Bitvector_class -> 'a -> int -> bitU ->(bitU)list)dict_Sail_values_Bitvector_a v n b= (update_list F ( + dict_Sail_values_Bitvector_a.bits_of_method v) n b))`; + + +val _ = Define ` + ((subrange_bv_inc:'a Bitvector_class -> 'a -> int -> int ->(bitU)list)dict_Sail_values_Bitvector_a v i j= (subrange_list T ( + dict_Sail_values_Bitvector_a.bits_of_method v) i j))`; + +val _ = Define ` + ((subrange_bv_dec:'a Bitvector_class -> 'a -> int -> int ->(bitU)list)dict_Sail_values_Bitvector_a v i j= (subrange_list F ( + dict_Sail_values_Bitvector_a.bits_of_method v) i j))`; + + +val _ = Define ` + ((update_subrange_bv_inc:'a Bitvector_class -> 'b Bitvector_class -> 'b -> int -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b v i j v'= (update_subrange_list T ( + dict_Sail_values_Bitvector_b.bits_of_method v) i j (dict_Sail_values_Bitvector_a.bits_of_method v')))`; + +val _ = Define ` + ((update_subrange_bv_dec:'a Bitvector_class -> 'b Bitvector_class -> 'b -> int -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b v i j v'= (update_subrange_list F ( + dict_Sail_values_Bitvector_b.bits_of_method v) i j (dict_Sail_values_Bitvector_a.bits_of_method v')))`; + + +(*val extz_bv : forall 'a. Bitvector 'a => Num.integer -> 'a -> list bitU*) +val _ = Define ` + ((extz_bv:'a Bitvector_class -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a n v= (extz_bits n ( + dict_Sail_values_Bitvector_a.bits_of_method v)))`; + + +(*val exts_bv : forall 'a. Bitvector 'a => Num.integer -> 'a -> list bitU*) +val _ = Define ` + ((exts_bv:'a Bitvector_class -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a n v= (exts_bits n ( + dict_Sail_values_Bitvector_a.bits_of_method v)))`; + + +(*val string_of_bv : forall 'a. Bitvector 'a => 'a -> string*) +val _ = Define ` + ((string_of_bv:'a Bitvector_class -> 'a -> string)dict_Sail_values_Bitvector_a v= (show_bitlist ( + dict_Sail_values_Bitvector_a.bits_of_method v)))`; + + +(*** Bytes and addresses *) + +val _ = type_abbrev( "memory_byte" , ``: bitU list``); + +(*val byte_chunks : forall 'a. list 'a -> Maybe.maybe (list (list 'a))*) + val byte_chunks_defn = Hol_defn "byte_chunks" ` + ((byte_chunks:'a list ->(('a list)list)option) bs= ((case bs of + [] => SOME [] + | a::b::c::d::e::f::g::h::rest => + OPTION_BIND (byte_chunks rest) (\ rest . SOME ([a;b;c;d;e;f;g;h] :: rest)) + | _ => NONE +)))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn byte_chunks_defn; + +(*val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> Maybe.maybe (list memory_byte)*) +val _ = Define ` + ((bytes_of_bits:'a Bitvector_class -> 'a ->((memory_byte)list)option)dict_Sail_values_Bitvector_a bs= (byte_chunks ( + dict_Sail_values_Bitvector_a.bits_of_method bs)))`; + + +(*val bits_of_bytes : list memory_byte -> list bitU*) +val _ = Define ` + ((bits_of_bytes:((bitU)list)list ->(bitU)list) bs= (FLAT (MAP (\ v. MAP (\ b. b) v) bs)))`; + + +val _ = Define ` + ((mem_bytes_of_bits:'a Bitvector_class -> 'a ->(((bitU)list)list)option)dict_Sail_values_Bitvector_a bs= (OPTION_MAP REVERSE (bytes_of_bits + dict_Sail_values_Bitvector_a bs)))`; + +val _ = Define ` + ((bits_of_mem_bytes:((bitU)list)list ->(bitU)list) bs= (bits_of_bytes (REVERSE bs)))`; + + +(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU +let bitv_of_byte_lifteds v = + foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v + +val bitv_of_bytes : list Sail_impl_base.byte -> list bitU +let bitv_of_bytes v = + foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v + +val byte_lifteds_of_bitv : list bitU -> list byte_lifted +let byte_lifteds_of_bitv bits = + let bits = List.map bit_lifted_of_bitU bits in + byte_lifteds_of_bit_lifteds bits + +val bytes_of_bitv : list bitU -> list byte +let bytes_of_bitv bits = + let bits = List.map bit_of_bitU bits in + bytes_of_bits bits + +val bit_lifteds_of_bitUs : list bitU -> list bit_lifted +let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits + +val bit_lifteds_of_bitv : list bitU -> list bit_lifted +let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v + + +val address_lifted_of_bitv : list bitU -> address_lifted +let address_lifted_of_bitv v = + let byte_lifteds = byte_lifteds_of_bitv v in + let maybe_address_integer = + match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing + end in + Address_lifted byte_lifteds maybe_address_integer + +val bitv_of_address_lifted : address_lifted -> list bitU +let bitv_of_address_lifted (Address_lifted bs _) = bitv_of_byte_lifteds bs + +val address_of_bitv : list bitU -> address +let address_of_bitv v = + let bytes = bytes_of_bitv v in + address_of_byte_list bytes*) + + val reverse_endianness_list_defn = Hol_defn "reverse_endianness_list" ` + ((reverse_endianness_list:'a list -> 'a list) bits= + (if LENGTH bits <=( 8 : num) then bits else + reverse_endianness_list (drop_list(( 8 : int)) bits) ++ take_list(( 8 : int)) bits))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn reverse_endianness_list_defn; + + +(*** Registers *) + +(*type register_field = string +type register_field_index = string * (integer * integer) (* name, start and end *) + +type register = + | Register of string * (* name *) + integer * (* length *) + integer * (* start index *) + bool * (* is increasing *) + list register_field_index + | UndefinedRegister of integer (* length *) + | RegisterPair of register * register*) + +val _ = Hol_datatype ` +(* ( 'a_regstate, 'b_regval, 'c_a) *) register_ref = + <| name : string; + (*is_inc : bool;*) + read_from :'a_regstate -> 'c_a; + write_to :'c_a -> 'a_regstate -> 'a_regstate; + of_regval :'b_regval -> 'c_a option; + regval_of :'c_a -> 'b_regval |>`; + + +(* Register accessors: pair of functions for reading and writing register values *) +val _ = type_abbrev((* ( 'regstate, 'regval) *) "register_accessors" , ``: + ((string -> 'regstate -> 'regval option) # + (string -> 'regval -> 'regstate -> 'regstate option))``); + +val _ = Hol_datatype ` +(* ( 'a_regtype, 'b_a) *) field_ref = + <| field_name : string; + field_start : int; + field_is_inc : bool; + get_field :'a_regtype -> 'b_a; + set_field :'a_regtype -> 'b_a -> 'a_regtype |>`; + + +(*let name_of_reg = function + | Register name _ _ _ _ -> name + | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "name_of_reg RegisterPair" +end + +let size_of_reg = function + | Register _ size _ _ _ -> size + | UndefinedRegister size -> size + | RegisterPair _ _ -> failwith "size_of_reg RegisterPair" +end + +let start_of_reg = function + | Register _ _ start _ _ -> start + | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "start_of_reg RegisterPair" +end + +let is_inc_of_reg = function + | Register _ _ _ is_inc _ -> is_inc + | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair" +end + +let dir_of_reg = function + | Register _ _ _ is_inc _ -> dir_of_bool is_inc + | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair" +end + +let size_of_reg_nat reg = natFromInteger (size_of_reg reg) +let start_of_reg_nat reg = natFromInteger (start_of_reg reg) + +val register_field_indices_aux : register -> register_field -> maybe (integer * integer) +let rec register_field_indices_aux register rfield = + match register with + | Register _ _ _ _ rfields -> List.lookup rfield rfields + | RegisterPair r1 r2 -> + let m_indices = register_field_indices_aux r1 rfield in + if isJust m_indices then m_indices else register_field_indices_aux r2 rfield + | UndefinedRegister _ -> Nothing + end + +val register_field_indices : register -> register_field -> integer * integer +let register_field_indices register rfield = + match register_field_indices_aux register rfield with + | Just indices -> indices + | Nothing -> failwith "Invalid register/register-field combination" + end + +let register_field_indices_nat reg regfield= + let (i,j) = register_field_indices reg regfield in + (natFromInteger i,natFromInteger j)*) + +(*let rec external_reg_value reg_name v = + let (internal_start, external_start, direction) = + match reg_name with + | Reg _ start size dir -> + (start, (if dir = D_increasing then start else (start - (size +1))), dir) + | Reg_slice _ reg_start dir (slice_start, _) -> + ((if dir = D_increasing then slice_start else (reg_start - slice_start)), + slice_start, dir) + | Reg_field _ reg_start dir _ (slice_start, _) -> + ((if dir = D_increasing then slice_start else (reg_start - slice_start)), + slice_start, dir) + | Reg_f_slice _ reg_start dir _ _ (slice_start, _) -> + ((if dir = D_increasing then slice_start else (reg_start - slice_start)), + slice_start, dir) + end in + let bits = bit_lifteds_of_bitv v in + <| rv_bits = bits; + rv_dir = direction; + rv_start = external_start; + rv_start_internal = internal_start |> + +val internal_reg_value : register_value -> list bitU +let internal_reg_value v = + List.map bitU_of_bit_lifted v.rv_bits + (*(integerFromNat v.rv_start_internal) + (v.rv_dir = D_increasing)*) + + +let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = + match d with + (*This is the case the thread/concurrecny model expects, so no change needed*) + | D_increasing -> (i,j) + | D_decreasing -> let slice_i = start - i in + let slice_j = (i - j) + slice_i in + (slice_i,slice_j) + end *) + +(* TODO +let external_reg_whole r = + Reg (r.name) (natFromInteger r.start) (natFromInteger r.size) (dir_of_bool r.is_inc) + +let external_reg_slice r (i,j) = + let start = natFromInteger r.start in + let dir = dir_of_bool r.is_inc in + Reg_slice (r.name) start dir (external_slice dir start (i,j)) + +let external_reg_field_whole reg rfield = + let (m,n) = register_field_indices_nat reg rfield in + let start = start_of_reg_nat reg in + let dir = dir_of_reg reg in + Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n)) + +let external_reg_field_slice reg rfield (i,j) = + let (m,n) = register_field_indices_nat reg rfield in + let start = start_of_reg_nat reg in + let dir = dir_of_reg reg in + Reg_f_slice (name_of_reg reg) start dir rfield + (external_slice dir start (m,n)) + (external_slice dir start (i,j))*) + +(*val external_mem_value : list bitU -> memory_value +let external_mem_value v = + byte_lifteds_of_bitv v $> List.reverse + +val internal_mem_value : memory_value -> list bitU +let internal_mem_value bytes = + List.reverse bytes $> bitv_of_byte_lifteds*) + + +(*val foreach : forall 'a 'vars. + (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars*) + val foreach_defn = Hol_defn "foreach" ` + ((foreach:'a list -> 'vars ->('a -> 'vars -> 'vars) -> 'vars) l vars body= + ((case l of + [] => vars + | (x :: xs) => foreach xs (body x vars) body + )))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn foreach_defn; + +(*val index_list : Num.integer -> Num.integer -> Num.integer -> list Num.integer*) + val index_list_defn = Hol_defn "index_list" ` + ((index_list:int -> int -> int ->(int)list) from to step= + (if ((step >( 0 : int)) /\ (from <= to)) \/ ((step <( 0 : int)) /\ (to <= from)) then + from :: index_list (from + step) to step + else []))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn index_list_defn; + +(*val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars*) + val while_defn = Hol_defn "while" ` + ((while:'vars ->('vars -> bool) ->('vars -> 'vars) -> 'vars) vars cond body= + (if cond vars then while (body vars) cond body else vars))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn while_defn; + +(*val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars*) + val until_defn = Hol_defn "until" ` + ((until:'vars ->('vars -> bool) ->('vars -> 'vars) -> 'vars) vars cond body= + (let vars = (body vars) in + if cond vars then vars else until (body vars) cond body))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn until_defn; + + +(* convert numbers unsafely to naturals *) + +val _ = Hol_datatype ` +(* 'a *) ToNatural_class= <| toNatural_method : 'a -> num |>`; + +(* eta-expanded for Isabelle output, otherwise it breaks *) +val _ = Define ` +((instance_Sail_values_ToNatural_Num_integer_dict:(int)ToNatural_class)= (<| + + toNatural_method := (\ n . Num (ABS n))|>))`; + +val _ = Define ` +((instance_Sail_values_ToNatural_Num_int_dict:(int)ToNatural_class)= (<| + + toNatural_method := (\ n . ((Num (ABS n)):num))|>))`; + +val _ = Define ` +((instance_Sail_values_ToNatural_nat_dict:(num)ToNatural_class)= (<| + + toNatural_method := (\ n . ( n:num))|>))`; + +val _ = Define ` +((instance_Sail_values_ToNatural_Num_natural_dict:(num)ToNatural_class)= (<| + + toNatural_method := (\ n . n)|>))`; + + +val _ = Define ` + ((toNaturalFiveTup:'a ToNatural_class -> 'b ToNatural_class -> 'c ToNatural_class -> 'd ToNatural_class -> 'e ToNatural_class -> 'd#'c#'b#'a#'e -> num#num#num#num#num)dict_Sail_values_ToNatural_a dict_Sail_values_ToNatural_b dict_Sail_values_ToNatural_c dict_Sail_values_ToNatural_d dict_Sail_values_ToNatural_e (n1,n2,n3,n4,n5)= + (dict_Sail_values_ToNatural_d.toNatural_method n1, dict_Sail_values_ToNatural_c.toNatural_method n2, dict_Sail_values_ToNatural_b.toNatural_method n3, dict_Sail_values_ToNatural_a.toNatural_method n4, dict_Sail_values_ToNatural_e.toNatural_method n5))`; + + +(* Let the following types be generated by Sail per spec, using either bitlists + or machine words as bitvector representation *) +(*type regfp = + | RFull of (string) + | RSlice of (string * integer * integer) + | RSliceBit of (string * integer) + | RField of (string * string) + +type niafp = + | NIAFP_successor + | NIAFP_concrete_address of vector bitU + | NIAFP_indirect_address + +(* only for MIPS *) +type diafp = + | DIAFP_none + | DIAFP_concrete of vector bitU + | DIAFP_reg of regfp + +let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function + | RFull name -> + let (start,length,direction,_) = reg_info name Nothing in + Reg name start length direction + | RSlice (name,i,j) -> + let i = natFromInteger i in + let j = natFromInteger j in + let (start,length,direction,_) = reg_info name Nothing in + let slice = external_slice direction start (i,j) in + Reg_slice name start direction slice + | RSliceBit (name,i) -> + let i = natFromInteger i in + let (start,length,direction,_) = reg_info name Nothing in + let slice = external_slice direction start (i,i) in + Reg_slice name start direction slice + | RField (name,field_name) -> + let (start,length,direction,span) = reg_info name (Just field_name) in + let slice = external_slice direction start span in + Reg_field name start direction field_name slice +end + +let niafp_to_nia reginfo = function + | NIAFP_successor -> NIA_successor + | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) + | NIAFP_indirect_address -> NIA_indirect_address +end + +let diafp_to_dia reginfo = function + | DIAFP_none -> DIA_none + | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) + | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) +end +*) +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/stateScript.sml b/snapshots/hol4/sail/lib/hol/stateScript.sml new file mode 100644 index 00000000..0eb048a0 --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/stateScript.sml @@ -0,0 +1,119 @@ +(*Generated by Lem from ../../src/gen_lib/state.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory sail_valuesTheory state_monadTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "state" + +(*open import Pervasives_extra*) +(*open import Sail_values*) +(*open import State_monad*) +(*open import {isabelle} `State_monad_lemmas`*) + +(*val iterS_aux : forall 'rv 'a 'e. Num.integer -> (Num.integer -> 'a -> State_monad.monadS 'rv unit 'e) -> list 'a -> State_monad.monadS 'rv unit 'e*) + val iterS_aux_defn = Hol_defn "iterS_aux" ` + ((iterS_aux:int ->(int -> 'a -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'a list -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) i f xs= ((case xs of + x :: xs => seqS (f i x) (iterS_aux (i +( 1 : int)) f xs) + | [] => returnS () + )))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn iterS_aux_defn; + +(*val iteriS : forall 'rv 'a 'e. (Num.integer -> 'a -> State_monad.monadS 'rv unit 'e) -> list 'a -> State_monad.monadS 'rv unit 'e*) +val _ = Define ` + ((iteriS:(int -> 'a ->('rv,(unit),'e)state_monad$monadS) -> 'a list -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) f xs= (iterS_aux(( 0 : int)) f xs))`; + + +(*val iterS : forall 'rv 'a 'e. ('a -> State_monad.monadS 'rv unit 'e) -> list 'a -> State_monad.monadS 'rv unit 'e*) +val _ = Define ` + ((iterS:('a -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'a list -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) f xs= (iteriS (\i x . + (case (i ,x ) of ( _ , x ) => f x )) xs))`; + + +(*val foreachS : forall 'a 'rv 'vars 'e. + list 'a -> 'vars -> ('a -> 'vars -> State_monad.monadS 'rv 'vars 'e) -> State_monad.monadS 'rv 'vars 'e*) + val foreachS_defn = Hol_defn "foreachS" ` + ((foreachS:'a list -> 'vars ->('a -> 'vars -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) xs vars body= ((case xs of + [] => returnS vars + | x :: xs => bindS +(body x vars) (\ vars . + foreachS xs vars body) +)))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn foreachS_defn; + +(*val bool_of_bitU_fail : forall 'rv 'e. Sail_values.bitU -> State_monad.monadS 'rv bool 'e*) +val _ = Define ` + ((bool_of_bitU_fail:sail_values$bitU -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set)= + (\x . (case x of + B0 => returnS F + | B1 => returnS T + | BU => failS "bool_of_bitU" + )))`; + + +(*val bool_of_bitU_oracleS : forall 'rv 'e. Sail_values.bitU -> State_monad.monadS 'rv bool 'e*) +val _ = Define ` + ((bool_of_bitU_oracleS:sail_values$bitU -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set)= + (\x . (case x of + B0 => returnS F + | B1 => returnS T + | BU => undefined_boolS () + )))`; + + +(*val bools_of_bits_oracleS : forall 'rv 'e. list Sail_values.bitU -> State_monad.monadS 'rv (list bool) 'e*) +val _ = Define ` + ((bools_of_bits_oracleS:(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((bool)list),'e)state_monad$result#'rv state_monad$sequential_state)set) bits= + (foreachS bits [] + (\ b bools . bindS +(bool_of_bitU_oracleS b) (\ b . + returnS (bools ++ [b])))))`; + + +(*val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list Sail_values.bitU -> State_monad.monadS 'rv 'a 'e*) +val _ = Define ` + ((of_bits_oracleS:'a sail_values$Bitvector_class ->(sail_values$bitU)list ->('rv,'a,'e)state_monad$monadS)dict_Sail_values_Bitvector_a bits= (bindS +(bools_of_bits_oracleS bits) (\ bs . + returnS (dict_Sail_values_Bitvector_a.of_bools_method bs))))`; + + +(*val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list Sail_values.bitU -> State_monad.monadS 'rv 'a 'e*) +val _ = Define ` + ((of_bits_failS:'a sail_values$Bitvector_class ->(sail_values$bitU)list ->('rv,'a,'e)state_monad$monadS)dict_Sail_values_Bitvector_a bits= (maybe_failS "of_bits" ( + dict_Sail_values_Bitvector_a.of_bits_method bits)))`; + + +(*val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> State_monad.monadS 'rv (Machine_word.mword 'a) 'e*) +val _ = Define ` + ((mword_oracleS:unit -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) () = (bindS +(bools_of_bits_oracleS (repeat [BU] (int_of_num (dimindex (the_value : 'a itself))))) (\ bs . + returnS (bitstring$v2w bs))))`; + + + +(*val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> State_monad.monadS 'rv bool 'e) -> + ('vars -> State_monad.monadS 'rv 'vars 'e) -> State_monad.monadS 'rv 'vars 'e*) + val whileS_defn = Hol_defn "whileS" ` + ((whileS:'vars ->('vars -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set) ->('vars -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) vars cond body s= + (( bindS(cond vars) (\ cond_val s' . + if cond_val then + ( bindS(body vars) (\ vars s'' . whileS vars cond body s'')) s' + else returnS vars s')) s))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn whileS_defn; + +(*val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> State_monad.monadS 'rv bool 'e) -> + ('vars -> State_monad.monadS 'rv 'vars 'e) -> State_monad.monadS 'rv 'vars 'e*) + val untilS_defn = Hol_defn "untilS" ` + ((untilS:'vars ->('vars -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set) ->('vars -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) vars cond body s= + (( bindS(body vars) (\ vars s' . + ( bindS(cond vars) (\ cond_val s'' . + if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s))`; + +val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn untilS_defn; +val _ = export_theory() + diff --git a/snapshots/hol4/sail/lib/hol/state_monadScript.sml b/snapshots/hol4/sail/lib/hol/state_monadScript.sml new file mode 100644 index 00000000..cf4764c0 --- /dev/null +++ b/snapshots/hol4/sail/lib/hol/state_monadScript.sml @@ -0,0 +1,348 @@ +(*Generated by Lem from ../../src/gen_lib/state_monad.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory sail_valuesTheory sail_instr_kindsTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "state_monad" + +(*open import Pervasives_extra*) +(*open import Sail_instr_kinds*) +(*open import Sail_values*) + +(* 'a is result type *) + +val _ = type_abbrev( "memstate" , ``: (int, sail_values$memory_byte) fmap``); +val _ = type_abbrev( "tagstate" , ``: (int, sail_values$bitU) fmap``); +(* type regstate = map string (vector bitU) *) + +val _ = Hol_datatype ` +(* 'regs *) sequential_state = + <| regstate : 'regs; + memstate : memstate; + tagstate : tagstate; + write_ea : (sail_instr_kinds$write_kind # int # int)option; + last_exclusive_operation_was_load : bool; + (* Random bool generator for use as an undefined bit oracle *) + next_bool : num -> (bool # num); + seed : num |>`; + + +(*val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs*) +val _ = Define ` + ((init_state:'regs ->(num -> bool#num) -> num -> 'regs sequential_state) regs o1 s= + (<| regstate := regs; + memstate := FEMPTY; + tagstate := FEMPTY; + write_ea := NONE; + last_exclusive_operation_was_load := F; + next_bool := o1; + seed := s |>))`; + + +val _ = Hol_datatype ` + ex = + Failure of string + | Throw of 'e`; + + +val _ = Hol_datatype ` + result = + Value of 'a + | Ex of ( 'e ex)`; + + +(* State, nondeterminism and exception monad with result value type 'a + and exception type 'e. *) +val _ = type_abbrev((* ( 'a_regs, 'b_a, 'c_e) *) "monadS" , ``:'a_regs sequential_state -> (('b_a,'c_e)result #'a_regs sequential_state) set``); + +(*val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e*) +val _ = Define ` + ((returnS:'a -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) a s= ({(Value a,s)}))`; + + +(*val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e*) +val _ = Define ` + ((bindS:('regs sequential_state ->(('a,'e)result#'regs sequential_state)set) ->('a -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) m f (s : 'regs sequential_state)= + (BIGUNION (IMAGE (\x . + (case x of (Value a, s') => f a s' | (Ex e, s') => {(Ex e, s')} )) (m s))))`; + + +(*val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e*) +val _ = Define ` + ((seqS:('regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) ->('regs sequential_state ->(('b,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) m n= (bindS m (\u . + (case (u ) of ( (_ : unit) ) => n ))))`; + + +(*val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e*) +val _ = Define ` + ((chooseS:'a set -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) xs s= (IMAGE (\ x . (Value x, s)) xs))`; + + +(*val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e*) +val _ = Define ` + ((readS:('regs sequential_state -> 'a) -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) f= (\ s . returnS (f s) s))`; + + +(*val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e*) +val _ = Define ` + ((updateS:('regs sequential_state -> 'regs sequential_state) -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) f= (\ s . returnS () (f s)))`; + + +(*val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e*) +val _ = Define ` + ((failS:string -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) msg s= ({(Ex (Failure msg), s)}))`; + + +(*val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e*) +val _ = Define ` + ((undefined_boolS:unit -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) () = (bindS +(readS (\ s . s.next_bool (s.seed))) (\ (b, seed) . seqS +(updateS (\ s . ( s with<| seed := seed |>))) +(returnS b))))`; + + +(*val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e*) +val _ = Define ` + ((exitS:unit -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) () = (failS "exit"))`; + + +(*val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e*) +val _ = Define ` + ((throwS:'e -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) e s= ({(Ex (Throw e), s)}))`; + + +(*val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) -> monadS 'regs 'a 'e2*) +val _ = Define ` + ((try_catchS:('regs sequential_state ->(('a,'e1)result#'regs sequential_state)set) ->('e1 -> 'regs sequential_state ->(('a,'e2)result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,'e2)result#'regs sequential_state)set) m h s= + (BIGUNION (IMAGE (\x . + (case x of + (Value a, s') => returnS a s' + | (Ex (Throw e), s') => h e s' + | (Ex (Failure msg), s') => {(Ex (Failure msg), s')} + )) (m s))))`; + + +(*val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e*) +val _ = Define ` + ((assert_expS:bool -> string -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) exp msg= (if exp then returnS () else failS msg))`; + + +(* For early return, we abuse exceptions by throwing and catching + the return value. The exception type is "either 'r 'e", where "Right e" + represents a proper exception and "Left r" an early return of value "r". *) +val _ = type_abbrev((* ( 'a_regs, 'b_a, 'c_r, 'd_e) *) "monadRS" , ``:('a_regs,'b_a, (('c_r,'d_e)sum)) monadS``); + +(*val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e*) +val _ = Define ` + ((early_returnS:'r -> 'regs sequential_state ->(('a,(('r,'e)sum))result#'regs sequential_state)set) r= (throwS (INL r)))`; + + +(*val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e*) +val _ = Define ` + ((catch_early_returnS:('regs sequential_state ->(('a,(('a,'e)sum))result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) m= + (try_catchS m + (\x . (case x of INL a => returnS a | INR e => throwS e ))))`; + + +(* Lift to monad with early return by wrapping exceptions *) +(*val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e*) +val _ = Define ` + ((liftRS:('regs sequential_state ->(('a,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,(('r,'e)sum))result#'regs sequential_state)set) m= (try_catchS m (\ e . throwS (INR e))))`; + + +(* Catch exceptions in the presence of early returns *) +(*val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2*) +val _ = Define ` + ((try_catchRS:('regs sequential_state ->(('a,(('r,'e1)sum))result#'regs sequential_state)set) ->('e1 -> 'regs sequential_state ->(('a,(('r,'e2)sum))result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,(('r,'e2)sum))result#'regs sequential_state)set) m h= + (try_catchS m + (\x . (case x of INL r => throwS (INL r) | INR e => h e ))))`; + + +(*val maybe_failS : forall 'regs 'a 'e. string -> Maybe.maybe 'a -> monadS 'regs 'a 'e*) +val _ = Define ` + ((maybe_failS:string -> 'a option -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) msg= + (\x . (case x of SOME a => returnS a | NONE => failS msg )))`; + + +(*val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs Sail_values.bitU 'e*) +val _ = Define ` + ((read_tagS:'a sail_values$Bitvector_class -> 'a ->('regs,(sail_values$bitU),'e)monadS)dict_Sail_values_Bitvector_a addr= (bindS +(maybe_failS "unsigned" ( + dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . + readS (\ s . option_CASE (FLOOKUP s.tagstate addr) B0 I))))`; + + +(* Read bytes from memory and return in little endian order *) +(*val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => Sail_instr_kinds.read_kind -> 'a -> nat -> monadS 'regs (list Sail_values.memory_byte) 'e*) +val _ = Define ` + ((read_mem_bytesS:'a sail_values$Bitvector_class -> sail_instr_kinds$read_kind -> 'a -> num ->('regs,((sail_values$memory_byte)list),'e)monadS)dict_Sail_values_Bitvector_a read_kind addr sz= (bindS +(maybe_failS "unsigned" ( + dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . + let sz = (int_of_num sz) in + let addrs = (index_list addr ((addr+sz)-( 1 : int))(( 1 : int))) in + let read_byte = (\ s addr . FLOOKUP s.memstate addr) in + bindS (readS (\ s . just_list (MAP (read_byte s) addrs))) + (\x . (case x of + SOME mem_val => seqS + (updateS + (\ s . + if read_is_exclusive read_kind then + ( s with<| last_exclusive_operation_was_load := T |>) + else s)) (returnS mem_val) + | NONE => failS "read_memS" + )))))`; + + +(*val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => Sail_instr_kinds.read_kind -> 'a -> Num.integer -> monadS 'regs 'b 'e*) +val _ = Define ` + ((read_memS:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> sail_instr_kinds$read_kind -> 'a -> int ->('regs,'b,'e)monadS)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b rk a sz= (bindS +(read_mem_bytesS dict_Sail_values_Bitvector_a rk a (nat_of_int sz)) (\ bytes . + maybe_failS "bits_of_mem_bytes" ( + dict_Sail_values_Bitvector_b.of_bits_method (bits_of_mem_bytes bytes)))))`; + + +(*val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e*) +val _ = Define ` + ((excl_resultS:unit -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) () = (bindS +(readS (\ s . s.last_exclusive_operation_was_load)) (\ excl_load . seqS +(updateS (\ s . ( s with<| last_exclusive_operation_was_load := F |>))) +(chooseS (if excl_load then {F; T} else {F})))))`; + + +(*val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => Sail_instr_kinds.write_kind -> 'a -> nat -> monadS 'regs unit 'e*) +val _ = Define ` + ((write_mem_eaS:'a sail_values$Bitvector_class -> sail_instr_kinds$write_kind -> 'a -> num ->('regs,(unit),'e)monadS)dict_Sail_values_Bitvector_a write_kind addr sz= (bindS +(maybe_failS "unsigned" ( + dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . + let sz = (int_of_num sz) in + updateS (\ s . ( s with<| write_ea := (SOME (write_kind, addr, sz)) |>)))))`; + + +(* Write little-endian list of bytes to previously announced address *) +(*val write_mem_bytesS : forall 'regs 'e. list Sail_values.memory_byte -> monadS 'regs bool 'e*) +val _ = Define ` + ((write_mem_bytesS:((sail_values$bitU)list)list -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) v= (bindS +(readS (\ s . s.write_ea)) (\x . + (case x of + NONE => failS "write ea has not been announced yet" + | SOME (_, addr, sz) => + let addrs = (index_list addr ((addr + sz) - ( 1 : int)) (( 1 : int))) in + (*let v = external_mem_value (bits_of v) in*) + let a_v = (lem_list$list_combine addrs v) in + let write_byte = (\mem p . (case (mem ,p ) of + ( mem , (addr, v) ) => mem |+ ( addr , + v ) + )) in + seqS + (updateS + (\ s . ( s with<| memstate := (FOLDL write_byte s.memstate a_v) |>))) + (returnS T) + ))))`; + + +(*val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e*) +val _ = Define ` + ((write_mem_valS:'a sail_values$Bitvector_class -> 'a ->('regs,(bool),'e)monadS)dict_Sail_values_Bitvector_a v= ((case mem_bytes_of_bits + dict_Sail_values_Bitvector_a v of + SOME v => write_mem_bytesS v + | NONE => failS "write_mem_val" +)))`; + + +(*val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> Sail_values.bitU -> monadS 'regs bool 'e*) +val _ = Define ` + ((write_tagS:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU ->('regs,(bool),'e)monadS)dict_Sail_values_Bitvector_a addr t= (bindS +(maybe_failS "unsigned" ( + dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . seqS +(updateS (\ s . ( s with<| tagstate := (s.tagstate |+ (addr, t)) |>))) +(returnS T))))`; + + +(*val read_regS : forall 'regs 'rv 'a 'e. Sail_values.register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e*) +val _ = Define ` + ((read_regS:('regs,'rv,'a)sail_values$register_ref -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) reg= (readS (\ s . reg.read_from s.regstate)))`; + + +(* TODO +let read_reg_range reg i j state = + let v = slice (get_reg state (name_of_reg reg)) i j in + [(Value (vec_to_bvec v),state)] +let read_reg_bit reg i state = + let v = access (get_reg state (name_of_reg reg)) i in + [(Value v,state)] +let read_reg_field reg regfield = + let (i,j) = register_field_indices reg regfield in + read_reg_range reg i j +let read_reg_bitfield reg regfield = + let (i,_) = register_field_indices reg regfield in + read_reg_bit reg i *) + +(*val read_regvalS : forall 'regs 'rv 'e. + Sail_values.register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e*) +val _ = Define ` + ((read_regvalS:(string -> 'regs -> 'rv option)#(string -> 'rv -> 'regs -> 'regs option) -> string -> 'regs sequential_state ->(('rv,'e)result#'regs sequential_state)set) (read, _) reg= (bindS +(readS (\ s . read reg s.regstate)) (\x . + (case x of + SOME v => returnS v + | NONE => failS ( STRCAT "read_regvalS " reg) + ))))`; + + +(*val write_regvalS : forall 'regs 'rv 'e. + Sail_values.register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e*) +val _ = Define ` + ((write_regvalS:(string -> 'regs -> 'rv option)#(string -> 'rv -> 'regs -> 'regs option) -> string -> 'rv -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) (_, write) reg v= (bindS +(readS (\ s . write reg v s.regstate)) (\x . + (case x of + SOME rs' => updateS (\ s . ( s with<| regstate := rs' |>)) + | NONE => failS ( STRCAT "write_regvalS " reg) + ))))`; + + +(*val write_regS : forall 'regs 'rv 'a 'e. Sail_values.register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e*) +val _ = Define ` + ((write_regS:('regs,'rv,'a)sail_values$register_ref -> 'a -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) reg v= + (updateS (\ s . ( s with<| regstate := (reg.write_to v s.regstate) |>))))`; + + +(* TODO +val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e +let update_reg reg f v state = + let current_value = get_reg state reg in + let new_value = f current_value v in + [(Value (), set_reg state reg new_value)] + +let write_reg_field reg regfield = update_reg reg regfield.set_field + +val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a +let update_reg_range reg i j reg_val new_val = set_bits (reg.is_inc) reg_val i j (bits_of new_val) +let write_reg_range reg i j = update_reg reg (update_reg_range reg i j) + +let update_reg_pos reg i reg_val x = update_list reg.is_inc reg_val i x +let write_reg_pos reg i = update_reg reg (update_reg_pos reg i) + +let update_reg_bit reg i reg_val bit = set_bit (reg.is_inc) reg_val i (to_bitU bit) +let write_reg_bit reg i = update_reg reg (update_reg_bit reg i) + +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in + regfield.set_field reg_val new_field_value +let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j) + +let update_reg_field_pos regfield i reg_val x = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update_list regfield.field_is_inc current_field_value i x in + regfield.set_field reg_val new_field_value +let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i) + +let update_reg_field_bit regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in + regfield.set_field reg_val new_field_value +let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*) +val _ = export_theory() + -- cgit v1.2.3