

@2760

8 years 
sacerdot 
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …



@2756

8 years 
sacerdot 
WARNING: this commit breaks things, sorry, Paolo is going to fix …



@2705

8 years 
sacerdot 
More progress in ASM towards implementing the new pseudoinstructions.



@2504

8 years 
mckinna 
More refactoring to support the tidied up compiler.ma



@2283

9 years 
mulligan 
Work from today.



@2280

9 years 
sacerdot 
Proof repaired.



@2279

9 years 
sacerdot 
1. Bug fixed in the semantics of PUSH (no indirection performed)
2. …



@2272

9 years 
mulligan 
Changed proof strategy for main lemma after noticed that the current …



@2264

9 years 
sacerdot 
1) Major change: we now always use the efficient way of resolving …



@2212

9 years 
mulligan 
More work on the INC case



@2160

9 years 
mulligan 
Added a new scratch file Test.ma for working on lemmas that are needed …



@2130

9 years 
sacerdot 
Proof repaired after Dominic's bug fix.



@2129

9 years 
mulligan 
Large changes from today trying to complete the main theorem. Again :(



@2124

9 years 
sacerdot 
Much more shuffling around to proper places



@2108

9 years 
mulligan 
Various axioms closed and others moved around. Uncommented main lemma …



@2062

9 years 
sacerdot 
Everything repaired (broken because of new proof obligation for fetch).



@2056

9 years 
sacerdot 
Repaired, ported to new fetch_pseudo_assembly.
The execute_n is …



@2051

9 years 
mulligan 
Finished the Jmp case in the main theorem.



@2047

9 years 
mulligan 
Big bugs in policy calculations found. Waiting for Jaap's commit.



@2040

9 years 
sacerdot 
Repaired using new /demod/ that allows to specify the rules to be used.



@2036

9 years 
sacerdot 
New daemon inserted because /demod/ got worst :(



@2032

9 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@2014

9 years 
mulligan 
Fixed problem in James' email message.



@1971

9 years 
sacerdot 
1. Interpret.ma:
we need to prove
\sigma (execute_preinstruction …



@1969

9 years 
sacerdot 
Some more progress, but now we must prove something on a Russell …



@1964

9 years 
tranquil 
introduced as_label_of_cost and adapted accordingly. Equality of cost …



@1962

9 years 
sacerdot 
More examples are now indexed.



@1951

9 years 
sacerdot 
Bug with overloaded names in the context.



@1948

9 years 
mulligan 
Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …



@1946

9 years 
sacerdot 
\snd half_add => add everywhere



@1939

9 years 
mulligan 
Changes to get things to compile and to avoid the dependency …



@1938

9 years 
sacerdot 
Definitions moved to the right places, now everything compiles again.



@1935

9 years 
mulligan 
Generalized some lemma in ASM/CostsProof.ma to work on abstract …



@1928

9 years 
mulligan 
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …



@1910

9 years 
mulligan 
Finished proof modulo termination argument



@1909

9 years 
mulligan 
Ported new statements to remainder of Interpret.ma file.



@1710

9 years 
mulligan 
changes from friday afternoon



@1709

9 years 
mulligan 
Changes to the execution of the MOVC instruction



@1666

9 years 
sacerdot 
PreStatus? datatype change: the code_memory field is not a left …



@1606

9 years 
sacerdot 
Porting to last library of Matita.



@1600

9 years 
sacerdot 
utilities and ASM ported to the new standard library



@1588

9 years 
sacerdot 
All goals generated by Russell for execute_1* are now closed, mostly …



@1587

9 years 
mulligan 
changes from today, including removing indexing of problematic …



@1582

9 years 
mulligan 
more added to the proof of execute_1_preinstruction  ~260 cases now …



@1581

9 years 
mulligan 
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1



@1577

9 years 
mulligan 
A lot more cases added to the proof at the bottom of …



@1575

9 years 
mulligan 
Changes to specifications on execute functions



@1573

9 years 
mulligan 
more complicated than it appears :(



@1547

9 years 
sacerdot 
Invariant on cost of one execution step strengthened.



@1541

9 years 
mulligan 
interpret.ma now compiles



@1540

9 years 
mulligan 
changes to proof in interrupt.ma



@1538

9 years 
mulligan 
changes to execute_1_0 proof



@1534

9 years 
mulligan 
committing my changes to interpret to prevent any further conflicts



@1533

9 years 
sacerdot 
Proof of execute_1 with Russell completed (up to some daemon used before).



@1527

9 years 
sacerdot 
More on Russell.



@1526

9 years 
sacerdot 
Using Russell to prove some properties.



@1522

9 years 
mulligan 
changes to preamble and lin to asm pass, resolved conflict in interpret



@1519

9 years 
campbell 
More syntax updates.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1514

9 years 
mulligan 
changes from today. matita keeps dieing



@1511

9 years 
mulligan 
proofs, added, changes to execute_1_0 function therefore required to …



@1494

9 years 
mulligan 
changes to get everything compiling again



@1037

10 years 
sacerdot 
Main theorem: comments are working again.



@985

10 years 
sacerdot 
1) Major refactoring: proofs moved where they should be.
2) New …



@936

10 years 
sacerdot 
Ticks are now handled correctly everywhere and the main proof takes …



@928

10 years 
sacerdot 
Technical splitting.



@910

10 years 
mulligan 
removed bug in execute_1_pseudoinstruction



@865

10 years 
sacerdot 
Renaming.



@856

10 years 
sacerdot 
1. if_then_else is now a notation for match with (to allow Russell to …



@843

10 years 
sacerdot 
Function moved from Interpret to Status.



@827

10 years 
sacerdot 
The preamble is now part of the PseudoStatus?.



@825

10 years 
mulligan 
lots of refactoring, finally got something to prove



@822

10 years 
mulligan 
removed all axioms



@821

10 years 
mulligan 
changes to introduce pseudostatus



@820

10 years 
mulligan 
changes to get the semantics of pseudoassembly working



@757

10 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@712

10 years 
mulligan 
Changes to get things to typecheck.



@698

10 years 
mulligan 
Commit with changes to files to get our files to typecheck.



@690

10 years 
mulligan 
Moved new matita files into correct place.


copied from src/ASM/newmatitadevelopment/Interpret.ma:



@688

10 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
