

@2280

8 years 
sacerdot 
Proof repaired.



@2279

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



@2272

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



@2264

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



@2212

8 years 
mulligan 
More work on the INC case



@2160

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



@2130

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



@2129

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



@2124

8 years 
sacerdot 
Much more shuffling around to proper places



@2108

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



@2062

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



@2056

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



@2051

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



@2047

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



@2040

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



@2036

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



@2032

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



@2014

8 years 
mulligan 
Fixed problem in James' email message.



@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 …



@1964

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



@1962

8 years 
sacerdot 
More examples are now indexed.



@1951

8 years 
sacerdot 
Bug with overloaded names in the context.



@1948

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



@1946

8 years 
sacerdot 
\snd half_add => add everywhere



@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.



@1935

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



@1928

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



@1910

8 years 
mulligan 
Finished proof modulo termination argument



@1909

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



@1710

8 years 
mulligan 
changes from friday afternoon



@1709

8 years 
mulligan 
Changes to the execution of the MOVC instruction



@1666

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



@1606

8 years 
sacerdot 
Porting to last library of Matita.



@1600

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



@1588

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



@1587

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



@1582

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



@1581

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



@1577

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



@1575

8 years 
mulligan 
Changes to specifications on execute functions



@1573

8 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

9 years 
sacerdot 
Main theorem: comments are working again.



@985

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



@936

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



@928

9 years 
sacerdot 
Technical splitting.



@910

9 years 
mulligan 
removed bug in execute_1_pseudoinstruction



@865

9 years 
sacerdot 
Renaming.



@856

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



@843

9 years 
sacerdot 
Function moved from Interpret to Status.



@827

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



@825

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



@822

9 years 
mulligan 
removed all axioms



@821

9 years 
mulligan 
changes to introduce pseudostatus



@820

9 years 
mulligan 
changes to get the semantics of pseudoassembly working



@757

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



@712

9 years 
mulligan 
Changes to get things to typecheck.



@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/newmatitadevelopment/Interpret.ma:



@688

9 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
