diff options
| author | Brian Campbell | 2018-07-03 14:13:19 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-03 14:20:09 +0100 |
| commit | a3a05ed727e2e7d8f0f3e54a444c556dbe2dfd83 (patch) | |
| tree | 3caf11ef6094492650eaf02ad3c8d79f60c5c8f5 | |
| parent | 9502f9ffabc5ec8f423974bd89da3d9810e4df80 (diff) | |
Fill in a few Coq functions for CHERI from the MIPS prelude
| -rw-r--r-- | mips/mips_extras.v | 8 | ||||
| -rw-r--r-- | mips/prelude.sail | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 94e4779c..49899107 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -152,3 +152,11 @@ Qed. Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. + + +Definition print_endline (_:string) : unit := tt. +Definition prerr_endline (_:string) : unit := tt. +Definition prerr_string (_:string) : unit := tt. +Definition putchar {T} (_:T) : unit := tt. +Require DecimalString. +Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). diff --git a/mips/prelude.sail b/mips/prelude.sail index b3349799..697ef74a 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -55,7 +55,7 @@ val "prerr_string" : string -> unit val putchar = {c:"sail_putchar", _:"putchar"} : forall ('a : Type). 'a -> unit -val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string +val concat_str = {lem: "stringAppend", coq: "String.append", _: "concat_str"} : (string, string) -> string val string_of_int = "string_of_int" : int -> string /* Unused? |