|
|
|
@3075
|
7 years |
mckinna |
Apologies for late folding in of old changes which were left over from …
|
|
|
|
@3066
|
7 years |
tranquil |
* implemented get_arg_16 for ACC_DPTR
* LINToASM is now agnostic as to …
|
|
|
|
@3056
|
7 years |
tranquil |
fixed a merge gone wrong
|
|
|
|
@3051
|
7 years |
tranquil |
fixed order of global initialization in LINToASM. For the moment …
|
|
|
|
@3045
|
7 years |
tranquil |
fixed what made test3 fail. However it involves a different notion of …
|
|
|
|
@3024
|
7 years |
sacerdot |
Bug fixed: set_flags was ignoring the cy and ov flags.
|
|
|
|
@2907
|
7 years |
sacerdot |
1. a few bugs fixed
2. as_return implemented for ASM & OC
|
|
|
|
@2770
|
7 years |
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
|
|
@2757
|
7 years |
tranquil |
many things are still broken, but there is a partial backtrack on …
|
|
|
|
@2754
|
7 years |
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
|
|
@2710
|
7 years |
sacerdot |
ASMCosts.ma repaired
|
|
|
|
@2316
|
7 years |
boender |
- committed temporary version: true version has to wait until I …
|
|
|
|
@2272
|
7 years |
mulligan |
Changed proof strategy for main lemma after noticed that the current …
|
|
|
|
@2270
|
7 years |
mulligan |
Bug spotted and fixed in write_at_stack_pointer
|
|
|
|
@2264
|
7 years |
sacerdot |
1) Major change: we now always use the efficient way of resolving …
|
|
|
|
@2247
|
7 years |
mulligan |
Work on the MOV instruction from today and bug fixes in set_arg_1.
|
|
|
|
@2172
|
7 years |
mulligan |
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
|
|
|
|
@2160
|
7 years |
mulligan |
Added a new scratch file Test.ma for working on lemmas that are needed …
|
|
|
|
@2139
|
7 years |
mulligan |
Changes to get the main lemma compiling again. Changes pushed into …
|
|
|
|
@2123
|
7 years |
boender |
- moved is_well_labeled_p to Status and instruction_is_label to ASM
…
|
|
|
|
@2119
|
7 years |
sacerdot |
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
|
|
|
|
@2111
|
7 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
|
@2055
|
8 years |
sacerdot |
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
|
|
|
|
@2032
|
8 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@1946
|
8 years |
sacerdot |
\snd half_add => add everywhere
|
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1666
|
8 years |
sacerdot |
PreStatus? datatype change: the code_memory field is not a left …
|
|
|
|
@1600
|
8 years |
sacerdot |
utilities and ASM ported to the new standard library
|
|
|
|
@1599
|
8 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1588
|
8 years |
sacerdot |
All goals generated by Russell for execute_1* are now closed, mostly …
|
|
|
|
@1581
|
8 years |
mulligan |
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
|
|
|
|
@1541
|
8 years |
mulligan |
interpret.ma now compiles
|
|
|
|
@1526
|
8 years |
sacerdot |
Using Russell to prove some properties.
|
|
|
|
@1522
|
8 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
|
@1521
|
8 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1518
|
8 years |
campbell |
Update to new syntax.
|
|
|
|
@1516
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
8 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1459
|
8 years |
boender |
- moved stronger occurs_exactly_once lemma to its proper place in …
|
|
|
|
@1393
|
8 years |
boender |
- added invariant for policy trie to assembly
- change (syntax only) …
|
|
|
|
@993
|
8 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
|
@990
|
8 years |
sacerdot |
Do no longer use the daemon automatically :-)
|
|
|
|
@985
|
8 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
|
@949
|
9 years |
mulligan |
resolved conflict, work from today
|
|
|
|
@935
|
9 years |
mulligan |
changes to status and assembly proof
|
|
|
|
@911
|
9 years |
sacerdot |
Type of set_code_memory generalized.
|
|
|
|
@843
|
9 years |
sacerdot |
Function moved from Interpret to Status.
|
|
|
|
@827
|
9 years |
sacerdot |
The preamble is now part of the PseudoStatus?.
|
|
|
|
@821
|
9 years |
mulligan |
changes to introduce pseudostatus
|
|
|
|
@757
|
9 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@705
|
9 years |
sacerdot |
Ported to new library (notation).
|
|
|
|
@698
|
9 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
|
@690
|
9 years |
mulligan |
Moved new matita files into correct place.
|
|
copied from src/ASM/new-matita-development/Status.ma:
|
|
|
|
@688
|
9 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
