sail/test/hol, branch sail2 Formal specification language for ISAs Simplify treating of undefined_bool in Lem library 2018-07-09T13:38:51+00:00 Thomas Bauereiss 2018-06-22T18:03:02+00:00 edc2be164fcf53c333796e55b93f94bf6c9ed152 Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list. 
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
Prove test_raw_add theorem for init_state 2018-06-12T08:19:09+00:00 Ramana Kumar 2018-06-12T08:17:21+00:00 0903f6dd0b6d51fde7b9b3bd45216f02fee4bd85 It can be proved almost entirely by symbolic execution (in <15s) _if_ the right definitions are in the compset. It took a lot of interactive stumbling about to discover that LUPDATE was missing from the standard list compset. 
It can be proved almost entirely by symbolic execution (in <15s) _if_
the right definitions are in the compset. It took a lot of interactive
stumbling about to discover that LUPDATE was missing from the standard
list compset.
Make progress on HOL4 test_raw_add 2018-06-12T08:19:09+00:00 Ramana Kumar 2018-06-08T16:36:55+00:00 2cfd94cc91ff21c23c5d0475e8d9b4d762797db0 The proof now gets through simulation of the first instruction of the test. 
The proof now gets through simulation of the first instruction of the test.
Work on HOL symbolic evaluation of installing code 2018-06-12T08:19:09+00:00 Ramana Kumar 2018-06-04T17:18:44+00:00 a7f257af55d6a43bbc595b5a1d31230a0204da6d 






Experimentation with PrePost for test_raw_add
2018-06-12T08:19:09+00:00

Ramana Kumar

2018-05-31T17:32:29+00:00

50f21b5a4ca0fbe554c5ce0e82e7a1ea52d66a31












Speculation on executing a CHERI test in HOL4
2018-06-12T08:19:09+00:00

Ramana Kumar

2018-05-30T12:50:53+00:00

59625e79c2465b3b362e72e2337204ba8dc161a0