|
|
@2151
|
9 years |
sacerdot |
1. Lemmas from AssemblyProof? anticipated to Assembly.ma
2. Jaap's …
|
|
|
@2149
|
9 years |
sacerdot |
Code shuffling to proper places.
|
|
|
@2148
|
9 years |
sacerdot |
1. specification made more user-friendly for AssemblyProof?
2. no more …
|
|
|
@2147
|
9 years |
sacerdot |
Theorem closed (up to one more lemma on overflow), but new proof …
|
|
|
@2146
|
9 years |
sacerdot |
1. specification fixed again
2. the proof in AssemblyProof? is now …
|
|
|
@2144
|
9 years |
sacerdot |
1. Policy specification fixed
2. Proof of monotonicity of sigma
|
|
|
@2143
|
9 years |
mulligan |
Changes to the subaddressing mode elim functions moved into their …
|
|
|
@2142
|
9 years |
sacerdot |
Down to one daemon that requires one lemma (monotonicity of sigma).
|
|
|
@2138
|
9 years |
sacerdot |
Invariant exported from proof of assembly_ok.
|
|
|
@2136
|
9 years |
sacerdot |
…
|
|
|
@2135
|
9 years |
sacerdot |
One complex daemon changed to two simpler ones.
|
|
|
@2132
|
9 years |
sacerdot |
Two more daemons closed, one left.
|
|
|
@2131
|
9 years |
sacerdot |
No more need for functional extensionality.
|
|
|
@2129
|
9 years |
mulligan |
Large changes from today trying to complete the main theorem. Again :(
|
|
|
@2128
|
9 years |
sacerdot |
Final shuffling around
|
|
|
@2124
|
9 years |
sacerdot |
Much more shuffling around to proper places
|
|
|
@2122
|
9 years |
sacerdot |
More stuff moved around in proper places
|
|
|
@2121
|
9 years |
sacerdot |
More functions moved to the places they belong to
|
|
|
@2119
|
9 years |
sacerdot |
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
|
|
|
@2115
|
9 years |
sacerdot |
Old commented out code removed
|
|
|
@2113
|
9 years |
sacerdot |
Proof by cases repaired; dead code removed.
|
|
|
@2112
|
9 years |
sacerdot |
WARNING: this commit may break some code.
- dead/useless code removed
|
|
|
@2111
|
9 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
@2110
|
9 years |
sacerdot |
…
|
|
|
@2108
|
9 years |
mulligan |
Various axioms closed and others moved around. Uncommented main lemma …
|
|
|
@2078
|
9 years |
sacerdot |
sigma_policy_specification has been
1) strengthened
2) made nicer to …
|
|
|
@2075
|
9 years |
mulligan |
Solved conflict in AssemblyProof?
|
|
|
@2057
|
9 years |
sacerdot |
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@2024
|
9 years |
mulligan |
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
|
|
|
@2021
|
9 years |
sacerdot |
Proof skeleton in place. Several daemons to be closed adding invariants.
|
|
|
@1984
|
9 years |
mulligan |
Most proof obligations closed in main_lemma apart from those of the …
|
|
|
@1983
|
9 years |
mulligan |
Changes to simplify the simpler cases of the main_lemma.
|
|
|
@1975
|
9 years |
mulligan |
Work from today on closing main_thm.
|
|
|
@1972
|
9 years |
mulligan |
Simple lemma with strangely complex proof complete.
|
|
|
@1966
|
9 years |
mulligan |
Progress made on main_thm proof: trying to find a pattern to use …
|
|
|
@1957
|
9 years |
mulligan |
Stitching proofs back together after slight change in statement of …
|
|
|
@1955
|
9 years |
mulligan |
Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
|
|
|
@1953
|
9 years |
mulligan |
Commit to avoid conflicts.
|
|
|
@1952
|
9 years |
sacerdot |
AssemblyProof? splitted.
|
|
|
@1948
|
9 years |
mulligan |
Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
|
|
|
@1947
|
9 years |
sacerdot |
Failure of automation/demod investigated a little bit.
|
|
|
@1946
|
9 years |
sacerdot |
\snd half_add => add everywhere
|
|
|
@1945
|
9 years |
sacerdot |
All proof statements repaired.
|
|
|
@1941
|
9 years |
mulligan |
Changes to the AssemblyProof? with a few more (large) axioms closed.
|
|
|
@1939
|
9 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
@1936
|
9 years |
mulligan |
Some holes filled in AssemblyProof?.ma.
|
|
|
@1668
|
9 years |
boender |
- split build_maps into build_maps and build_maps_ok
- work with CSC …
|
|
|
@1667
|
9 years |
sacerdot |
Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
|
|
|
@1666
|
9 years |
sacerdot |
PreStatus? datatype change: the code_memory field is not a left …
|
|
|
@1649
|
9 years |
boender |
- changes to Assembly for integration with Policy and easier use of …
|
|
|
@1616
|
9 years |
sacerdot |
Partially ported to new Matita syntax.
Because of some changes in …
|
|
|
@1607
|
9 years |
sacerdot |
Porting to new library.
|
|
|
@1484
|
9 years |
sacerdot |
…
|
|
|
@1333
|
10 years |
sacerdot |
Avoid using the name of the construction of jmeq.
|
|
|
@1045
|
10 years |
mulligan |
resolved conflict in rtlabs
|
|
|
@1043
|
10 years |
sacerdot |
Axiom commented out.
|
|
|
@1042
|
10 years |
sacerdot |
Dead code removed.
Slow code uncommented.
|
|
|
@1041
|
10 years |
sacerdot |
fetch_assembly is still working after bug fix
|
|
|
@1039
|
10 years |
sacerdot |
fetch_assembly_pseudo2 repaired from dependent type madness
|
|
|
@1037
|
10 years |
sacerdot |
Main theorem: comments are working again.
|
|
|
@1036
|
10 years |
sacerdot |
…
|
|
|
@1035
|
10 years |
sacerdot |
Main theorem (broken because of dependent types) almost restored.
|
|
|
@1015
|
10 years |
sacerdot |
One intermediate version of main_thm0 close to be repaired.
|
|
|
@1014
|
10 years |
sacerdot |
The main theorem is completely broken (again).
|
|
|
@998
|
10 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
@994
|
10 years |
mulligan |
small changes
|
|
|
@993
|
10 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
@992
|
10 years |
mulligan |
a few more axioms closed
|
|
|
@991
|
10 years |
mulligan |
loads of axioms related to equality on instructions closed
|
|
|
@989
|
10 years |
sacerdot |
Type of build_maps strengthened.
|
|
|
@988
|
10 years |
sacerdot |
Proof restored.
|
|
|
@987
|
10 years |
sacerdot |
Real parameterization over the policy.
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@982
|
10 years |
boender |
- this should work (see previous commit)
|
|
|
@979
|
10 years |
sacerdot |
…
|
|
|
@977
|
10 years |
sacerdot |
#$%@#$@#$
|
|
|
@975
|
10 years |
sacerdot |
…
|
|
|
@972
|
10 years |
sacerdot |
…
|
|
|
@971
|
10 years |
sacerdot |
…
|
|
|
@959
|
10 years |
sacerdot |
…
|
|
|
@951
|
10 years |
sacerdot |
long call case completed
|
|
|
@950
|
10 years |
sacerdot |
Horrible sub-proof finished :-)
|
|
|
@949
|
10 years |
mulligan |
resolved conflict, work from today
|
|
|
@948
|
10 years |
sacerdot |
Some progress on the Call case.
|
|
|
@946
|
10 years |
sacerdot |
Jmp case repaired after addition of MAP hypothesis.
|
|
|
@945
|
10 years |
mulligan |
more small changes to proof of main thrm
|
|
|
@944
|
10 years |
mulligan |
split definition
|
|
|
@943
|
10 years |
sacerdot |
…
|
|
|
@942
|
10 years |
sacerdot |
New invariant for the main theorem.
The new invariant is much more …
|
|
|
@941
|
10 years |
sacerdot |
Jmp case finished up to arithmetical properties.
|
|
|
@940
|
10 years |
mulligan |
more changes to inc case of main theorem
|
|
|
@939
|
10 years |
sacerdot |
Long Jmp case finished.
|
|
|
@938
|
10 years |
sacerdot |
…
|
|
|
@937
|
10 years |
mulligan |
resolved conflict in assembly_proof, more lemmas added
|
|
|
@936
|
10 years |
sacerdot |
Ticks are now handled correctly everywhere and the main proof takes …
|
|
|
@935
|
10 years |
mulligan |
changes to status and assembly proof
|
|
|
@934
|
10 years |
sacerdot |
…
|
|
|
@933
|
10 years |
sacerdot |
New proof strategy.
|
|
|
@932
|
10 years |
sacerdot |
…
|
|
|