

@2138

9 years 
sacerdot 
Invariant exported from proof of assembly_ok.



@2137

9 years 
sacerdot 
Bug fixed in specification.



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



@2101

9 years 
boender 
 renamed medium to absolute jump
 revised proofs of policy, some …



@2081

9 years 
sacerdot 
Type of assembly fixed to be compatible with the old one and to take …



@2079

9 years 
sacerdot 
sigma_policy_specification restyled



@2078

9 years 
sacerdot 
sigma_policy_specification has been
1) strengthened
2) made nicer to …



@2073

9 years 
sacerdot 
All false daemons removed.



@2072

9 years 
sacerdot 
We need to import Jaap's invariants now.



@2071

9 years 
sacerdot 
More daemons closed, but one is suspect now.



@2070

9 years 
sacerdot 
More daemons closed.



@2055

9 years 
sacerdot 
Warning: this commit adds an hypothesis that breaks all of assembly stuff.



@2051

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



@2048

9 years 
boender 
 factorised jump decisions



@2047

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



@2032

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



@2028

9 years 
boender 
 bugfix to Assembly (forgotten sigma)
 added …



@2022

9 years 
boender 
 corrected jump calculation algorithm



@2021

9 years 
sacerdot 
Proof skeleton in place. Several daemons to be closed adding invariants.



@2015

9 years 
mulligan 
Changes following a conversation with Jaap: as it stands computation …



@2005

9 years 
boender 
 minor changes to make things compile with a clean checkout



@1948

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



@1946

9 years 
sacerdot 
\snd half_add => add everywhere



@1943

9 years 
boender 
 changed 'labels okay' part of create_label_cost_map



@1942

9 years 
mulligan 
Work on showing the equivalence of two methods of looking up from the maps.



@1934

9 years 
boender 
 various & sundry moves of lemmas to better places
 integrated …



@1925

9 years 
boender 
 readded jump_lenggh



@1905

9 years 
boender 
 plugging gap in assembly proof



@1887

9 years 
boender 
 added SEFM2012 directory
 some progress in assembly



@1885

9 years 
boender 
 updated assembler with new definition of occurs_exactly_once



@1870

9 years 
boender 
 changed sigma00 in Assembly to use foldl_strong + proved invariants …



@1668

10 years 
boender 
 split build_maps into build_maps and build_maps_ok
 work with CSC …



@1667

10 years 
sacerdot 
Main lemma for the main_thm of AssemblyProof? redeclared as an axiom …



@1649

10 years 
boender 
 changes to Assembly for integration with Policy and easier use of …



@1615

10 years 
sacerdot 
Policy now depends on Assembly and not the other way around.



@1614

10 years 
boender 
 split policy from assembly



@1613

10 years 
sacerdot 
Coercion moved to Matita standard lib.



@1609

10 years 
boender 
 added alias to ASM/BitVectorTrie
 removed double include from …



@1607

10 years 
sacerdot 
Porting to new library.



@1606

10 years 
sacerdot 
Porting to last library of Matita.



@1593

10 years 
boender 
 cleaned up Assembly, moved some definitions elsewhere



@1592

10 years 
boender 
 updated definitions to work with programs of maximum 2^{16 instructions}



@1578

10 years 
boender 
 proof of termination of policy completed (needs some cleanup work …



@1562

10 years 
mulligan 
new version of assembly, fixed conflict in positivemap.ma, changed …



@1556

10 years 
mulligan 
submitting to avoid conflicts



@1555

10 years 
boender 
 changes to assembly
 added lookup to PositiveMap?
 lightly changed …



@1528

10 years 
campbell 
Update most of Assembly.ma with new syntax and identifier maps.
Change …



@1493

10 years 
mulligan 
finished well labeled check, up to injectivity of the label map



@1482

10 years 
sacerdot 
1. very long standing conflict committed (but don't ask me what the …



@1479

10 years 
boender 
 added insert_lookup_opt
 assembly compiles now



@1459

10 years 
boender 
 moved stronger occurs_exactly_once lemma to its proper place in …



@1417

10 years 
boender 
 proved that jumps always increase  this should make termination easy



@1404

10 years 
boender 
 reworked + added
 added an axiom to arithmetic, but should be provable



@1393

10 years 
boender 
 added invariant for policy trie to assembly
 change (syntax only) …



@1363

10 years 
boender 
 done stuff with create_label_trie



@1309

10 years 
boender 
 refounded JEP



@1103

10 years 
boender 
 reverted to old policy



@1054

10 years 
boender 
 proven policy safe



@1040

10 years 
sacerdot 
Bug fixed in assembly.



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



@993

10 years 
sacerdot 
More Russell everywhere; getting closer to the goal.



@989

10 years 
sacerdot 
Type of build_maps strengthened.



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



@938

10 years 
sacerdot 
…



@922

10 years 
mulligan 
changes to get assemblyproof to compile



@920

10 years 
boender 
 corrected mov instruction



@914

10 years 
boender 
 complete.



@913

10 years 
boender 
 temporary commit s.t. Assembly compiles



@907

10 years 
boender 
 added quadruples to Util
 start of implementation of new jump …



@846

10 years 
mulligan 
changes



@844

10 years 
sacerdot 
Useless code removed.



@842

10 years 
sacerdot 
Bug fixed.



@840

10 years 
sacerdot 
sigma defined



@837

10 years 
mulligan 
changes complete



@836

10 years 
mulligan 
changes to assembly functions



@833

10 years 
sacerdot 
Bug fixed to make the file compile.
But the type of the assembly …



@832

10 years 
mulligan 
work from today



@825

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



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



@719

10 years 
mulligan 
Added missing assembly file ported to matita.
