c4dc578bc3
Fix up proofs after word lemma moves
2018-10-10 14:15:01 +11:00
d75740201c
Remove pure word lemmas from proof/*
...
Removes redundant lemmas after moving them up to Word_Lib.
2018-10-10 14:15:00 +11:00
a1d1b69776
Isabelle2018 arm: CRefine
2018-08-20 09:06:37 +10:00
6b9d9d24dd
Isabelle2018: new "op x" syntax; now is "(x)"
...
(result of "isabelle update_op -m <dir>")
2018-08-20 09:06:35 +10:00
011e08458e
Isabelle2018: new comment syntax
...
(result of "isabelle update_comments <dirs>")
2018-08-20 09:06:35 +10:00
571ef6d0ca
crefine+drefine+access+infoflow: update proofs for SetTLSBase (VER-807)
2018-07-03 13:42:22 +10:00
2d0baab462
Proof update for crunch changes
2018-04-04 14:13:55 +10:00
9b0441e288
arm + arm_hyp: crefine for ctcb_offset C AUXUPD
2018-03-26 14:37:22 +11:00
2f540e802c
add constant definitions for bounds on untyped object sizes
2017-12-18 12:58:27 +11:00
a2dd6d1777
autocorres-crefine: update CRefine proofs for AutoCorres
2017-11-22 15:37:36 +11:00
48b3a8b4ca
update object and field widths for x64, and remove some magic numbers
...
In X64 update the following to match the C kernel:
- TCB size-bits (11).
- Endpoint size-bits (4).
- Guard bits (58).
- Message registers.
For all architectures, replace magic numbers with defined constants in
specifications, and as far as possible in proofs:
- tcb_bits in abstract spec.
- tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell
spec, Haskell and C refinement proofs.
2017-10-26 14:05:35 +11:00
238e8b307e
x64: merge master
2017-07-21 11:27:12 +10:00
796887d9b1
Removes all trailing whitespaces
2017-07-12 15:13:51 +10:00
17776ce6d3
arm crefine: Refactors proofs for new definitions (pteBits, pdeBits, etc)
2017-06-19 14:32:45 +10:00
f00bd94abe
crefine: move crefine/* into crefine/ARM/*
2017-03-31 16:13:41 +11:00
Edward Pierzchalski
Gerwin Klein
Corey Lewis
Matthew Brecknell
Alejandro Gomez-Londono
Alejandro Gomez-Londono
Rafal Kolanski