|
|
@2072
|
8 years |
sacerdot |
We need to import Jaap's invariants now.
|
|
|
@2071
|
8 years |
sacerdot |
More daemons closed, but one is suspect now.
|
|
|
@2070
|
8 years |
sacerdot |
More daemons closed.
|
|
|
@2069
|
8 years |
sacerdot |
…
|
|
|
@2068
|
8 years |
sacerdot |
…
|
|
|
@2067
|
8 years |
sacerdot |
…
|
|
|
@2066
|
8 years |
mulligan |
Finished for the day.
|
|
|
@2065
|
8 years |
boender |
- committed another draft
|
|
|
@2064
|
8 years |
boender |
- more progress
|
|
|
@2063
|
8 years |
mulligan |
Minor fixes
|
|
|
@2062
|
8 years |
sacerdot |
Everything repaired (broken because of new proof obligation for fetch).
|
|
|
@2061
|
8 years |
mulligan |
Added Randall Holmes' Usenet post on branch displacement optimisation …
|
|
|
@2060
|
8 years |
mulligan |
More work on paper.
|
|
|
@2059
|
8 years |
boender |
- updated Policy to work better
|
|
|
@2058
|
8 years |
mulligan |
First draft of changes to main sections (i.e. those describing the …
|
|
|
@2057
|
8 years |
sacerdot |
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
|
|
|
@2056
|
8 years |
sacerdot |
Repaired, ported to new fetch_pseudo_assembly.
The execute_n is …
|
|
|
@2055
|
8 years |
sacerdot |
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
|
|
|
@2054
|
8 years |
boender |
- progress
|
|
|
@2053
|
8 years |
mulligan |
Introduction changed, with many paragraphs deleted.
|
|
|
@2052
|
8 years |
mulligan |
Initial commit of proposed CPP 2012 paper on the proof of correctness …
|
|
|
@2051
|
8 years |
mulligan |
Finished the Jmp case in the main theorem.
|
|
|
@2049
|
8 years |
boender |
- progress
|
|
|
@2048
|
8 years |
boender |
- factorised jump decisions
|
|
|
@2047
|
8 years |
mulligan |
Big bugs in policy calculations found. Waiting for Jaap's commit.
|
|
|
@2046
|
8 years |
boender |
- removed old paper directory
|
|
|
@2045
|
8 years |
boender |
- renamed paper directory
|
|
|
@2040
|
8 years |
sacerdot |
Repaired using new /demod/ that allows to specify the rules to be used.
|
|
|
@2039
|
8 years |
sacerdot |
New, better interface for subaddressing_mode_elim
|
|
|
@2038
|
8 years |
sacerdot |
split => vsplit
|
|
|
@2037
|
8 years |
sacerdot |
flatten is now part of stdlib
|
|
|
@2036
|
8 years |
sacerdot |
New daemon inserted because /demod/ got worst :-(
|
|
|
@2034
|
8 years |
boender |
- split Policy into three separate files for ease (and indeed …
|
|
|
@2032
|
8 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@2028
|
8 years |
boender |
- bugfix to Assembly (forgotten sigma)
- added …
|
|
|
@2027
|
8 years |
mulligan |
Got the main lemma to apply in the proof of main theorem again and …
|
|
|
@2026
|
8 years |
mulligan |
Added a new file to house the main theorem as the type checking time …
|
|
|
@2024
|
8 years |
mulligan |
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
|
|
|
@2023
|
8 years |
mulligan |
Closed main lemma modulo closing trivial subgoals about commutations …
|
|
|
@2022
|
8 years |
boender |
- corrected jump calculation algorithm
|
|
|
@2021
|
8 years |
sacerdot |
Proof skeleton in place. Several daemons to be closed adding invariants.
|
|
|
@2020
|
8 years |
mulligan |
CJNE case complete, DJNZ case almost complete
|
|
|
@2018
|
8 years |
mulligan |
CJNE case a complete mess.
|
|
|
@2017
|
8 years |
mulligan |
Large swathes of proof of main lemma added.
|
|
|
@2015
|
8 years |
mulligan |
Changes following a conversation with Jaap: as it stands computation …
|
|
|
@2014
|
8 years |
mulligan |
Fixed problem in James' email message.
|
|
|
@2008
|
8 years |
boender |
- substantial closing of holes in proof
|
|
|
@2006
|
8 years |
boender |
- added alias for bitvector zero
- changed extralib bounded …
|
|
|
@2005
|
8 years |
boender |
- minor changes to make things compile with a clean checkout
|
|
|
@2001
|
8 years |
campbell |
Get the compiler to output more.
|
|
|
@1996
|
8 years |
campbell |
Work on correctness from yesterday.
|
|
|
@1987
|
8 years |
campbell |
Move BEValues to common to reflect their use in the memory model for …
|
|
|
@1985
|
8 years |
mulligan |
A single `false' case for unconditional jumps completed.
|
|
|
@1984
|
8 years |
mulligan |
Most proof obligations closed in main_lemma apart from those of the …
|
|
|
@1983
|
8 years |
mulligan |
Changes to simplify the simpler cases of the main_lemma.
|
|
|
@1979
|
8 years |
sacerdot |
Very very very tricky lemma closed. A dreadful mix of JM equality …
|
|
|
@1978
|
8 years |
sacerdot |
Two more cases completed.
|
|
|
@1977
|
8 years |
sacerdot |
Unblocked: let ... as hides two different terms, one that uses Leibniz …
|
|
|
@1976
|
8 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
@1975
|
8 years |
mulligan |
Work from today on closing main_thm.
|
|
|
@1973
|
8 years |
boender |
- removed superfluous match
- displaced 'cases daemon'
|
|
|
@1972
|
8 years |
mulligan |
Simple lemma with strangely complex proof complete.
|
|
|
@1971
|
8 years |
sacerdot |
1. Interpret.ma:
we need to prove
\sigma (execute_preinstruction …
|
|
|
@1969
|
8 years |
sacerdot |
Some more progress, but now we must prove something on a Russell …
|
|
|
@1967
|
8 years |
sacerdot |
Mov case completed.
|
|
|
@1966
|
8 years |
mulligan |
Progress made on main_thm proof: trying to find a pattern to use …
|
|
|
@1965
|
8 years |
boender |
- further completed proof, changed jump_expansion' to reflect new type …
|
|
|
@1964
|
8 years |
tranquil |
introduced as_label_of_cost and adapted accordingly. Equality of cost …
|
|
|
@1963
|
8 years |
sacerdot |
More progress in restoring the original proof.
|
|
|
@1962
|
8 years |
sacerdot |
More examples are now indexed.
|
|
|
@1961
|
8 years |
sacerdot |
No more interaction required.
|
|
|
@1959
|
8 years |
mulligan |
Commented out diverging application of demodulation and closed goals …
|
|
|
@1958
|
8 years |
mulligan |
Marked divergence in StatusProofs?.ma
|
|
|
@1957
|
8 years |
mulligan |
Stitching proofs back together after slight change in statement of …
|
|
|
@1956
|
8 years |
boender |
- finished proof of lemma (where auto does strange things again)
|
|
|
@1955
|
8 years |
mulligan |
Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
|
|
|
@1953
|
8 years |
mulligan |
Commit to avoid conflicts.
|
|
|
@1952
|
8 years |
sacerdot |
AssemblyProof? splitted.
|
|
|
@1951
|
8 years |
sacerdot |
Bug with overloaded names in the context.
|
|
|
@1950
|
8 years |
boender |
- advances in policy
|
|
|
@1948
|
8 years |
mulligan |
Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
|
|
|
@1947
|
8 years |
sacerdot |
Failure of automation/demod investigated a little bit.
|
|
|
@1946
|
8 years |
sacerdot |
\snd half_add => add everywhere
|
|
|
@1945
|
8 years |
sacerdot |
All proof statements repaired.
|
|
|
@1944
|
8 years |
sacerdot |
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
|
|
|
@1943
|
8 years |
boender |
- changed 'labels okay' part of create_label_cost_map
|
|
|
@1942
|
8 years |
mulligan |
Work on showing the equivalence of two methods of looking up from the maps.
|
|
|
@1941
|
8 years |
mulligan |
Changes to the AssemblyProof? with a few more (large) axioms closed.
|
|
|
@1940
|
8 years |
boender |
- committed new version of final invariant
|
|
|
@1939
|
8 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
@1938
|
8 years |
sacerdot |
Definitions moved to the right places, now everything compiles again.
|
|
|
@1937
|
8 years |
boender |
- filled in some of the gaps in the proof of Policy
- reverted …
|
|
|
@1936
|
8 years |
mulligan |
Some holes filled in AssemblyProof?.ma.
|
|
|
@1935
|
8 years |
mulligan |
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
|
|
|
@1934
|
8 years |
boender |
- various & sundry moves of lemmas to better places
- integrated …
|
|
|
@1933
|
8 years |
boender |
- slight revamp
|
|
|
@1932
|
8 years |
boender |
- added some more dependent types (we love 'em)
|
|
|
@1931
|
8 years |
boender |
- added latest bvt alias
- temporary "cases daemon" commit of new …
|
|
|
@1929
|
8 years |
mulligan |
Simplified proof by removing most of the invariants on the statements …
|
|
|
@1928
|
8 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|