

@3112

7 years 
tranquil 
added invariant that costlabels are only assigned to NOPs (not proved …



@3104

7 years 
sacerdot 
Performance improvement.



@3076

7 years 
mckinna 
simplified include dependencies



@3066

7 years 
tranquil 
* implemented get_arg_16 for ACC_DPTR
* LINToASM is now agnostic as to …



@3065

7 years 
sacerdot 
Efficiency of semantics of assembled improved: ticks_of was …



@3057

7 years 
tranquil 
lookup of function identifiers was not corrected with sigma



@3039

7 years 
tranquil 
* merged and extended MovSuccessor? and Mov in one instruction (Mov dst …



@3034

7 years 
sacerdot 
Bug fixed: COST instructions are now assembled as NOP to prevent the …



@2999

7 years 
sacerdot 
code_memory added to labelled_object_code to avoid recomputing it …



@2899

7 years 
sacerdot 
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …



@2781

7 years 
sacerdot 
One more computational daemon closed.



@2761

7 years 
sacerdot 
Unused (but not useless) code commented out.



@2760

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



@2754

7 years 
sacerdot 
1. WARNING: I commented out one of James's function used in …



@2707

7 years 
sacerdot 
Assembly repaired.



@2705

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



@2651

7 years 
sacerdot 
Type String changed.



@2516

7 years 
mckinna 
removed typedefs; restored older versions; moved typedefs to …



@2498

7 years 
mckinna 
Refactor:
Typedefs object_code and costlabel_map lifted out from …



@2316

7 years 
boender 
 committed temporary version: true version has to wait until I …



@2268

8 years 
mulligan 
Bug spotted in instruction_size (lookup_datalabels cannot just be a …



@2264

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



@2221

8 years 
boender 
 removed cases daemon from PolicyFront?



@2199

8 years 
sacerdot 
No longer used lemma containing the last daemon removed.
The proof is …



@2197

8 years 
sacerdot 
Main lemmas all closed.



@2194

8 years 
sacerdot 
1. monotone moved to Assembly
2. some easier daemons, one shows an …



@2193

8 years 
sacerdot 
Statement cleanup.



@2192

8 years 
sacerdot 
Shuffling around.



@2191

8 years 
sacerdot 
Only one daemon left.



@2190

8 years 
sacerdot 
Two daemons left.



@2189

8 years 
sacerdot 
Proof very close to completion.



@2188

8 years 
sacerdot 
1. Policy specification generalized
2. All invariants but the main one …



@2161

8 years 
sacerdot 
Most of the old proof restored.



@2159

8 years 
sacerdot 
One daemon left, back to original proof.



@2158

8 years 
sacerdot 
One less daemon.



@2157

8 years 
sacerdot 
Anticipating a proof needed before.



@2156

8 years 
sacerdot 
One more invariant, one less daemon.



@2154

8 years 
sacerdot 
Code shuffled around.



@2151

8 years 
sacerdot 
1. Lemmas from AssemblyProof? anticipated to Assembly.ma
2. Jaap's …



@2148

8 years 
sacerdot 
1. specification made more userfriendly for AssemblyProof?
2. no more …



@2147

8 years 
sacerdot 
Theorem closed (up to one more lemma on overflow), but new proof …



@2146

8 years 
sacerdot 
1. specification fixed again
2. the proof in AssemblyProof? is now …



@2144

8 years 
sacerdot 
1. Policy specification fixed
2. Proof of monotonicity of sigma



@2138

8 years 
sacerdot 
Invariant exported from proof of assembly_ok.



@2137

8 years 
sacerdot 
Bug fixed in specification.



@2111

8 years 
sacerdot 
Cleanup: lemmas/theorems/axioms moved to the right places.



@2110

8 years 
sacerdot 
…



@2108

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



@2101

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



@2081

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



@2079

8 years 
sacerdot 
sigma_policy_specification restyled



@2078

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



@2073

8 years 
sacerdot 
All false daemons removed.



@2072

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



@2071

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



@2070

8 years 
sacerdot 
More daemons closed.



@2055

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



@2051

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



@2048

8 years 
boender 
 factorised jump decisions



@2047

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



@2032

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



@2028

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



@2022

8 years 
boender 
 corrected jump calculation algorithm



@2021

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



@2015

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



@2005

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



@1948

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



@1946

8 years 
sacerdot 
\snd half_add => add everywhere



@1943

8 years 
boender 
 changed 'labels okay' part of create_label_cost_map



@1942

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



@1934

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



@1925

8 years 
boender 
 readded jump_lenggh



@1905

8 years 
boender 
 plugging gap in assembly proof



@1887

8 years 
boender 
 added SEFM2012 directory
 some progress in assembly



@1885

8 years 
boender 
 updated assembler with new definition of occurs_exactly_once



@1870

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



@1668

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



@1667

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



@1649

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



@1615

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



@1614

8 years 
boender 
 split policy from assembly



@1613

8 years 
sacerdot 
Coercion moved to Matita standard lib.



@1609

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



@1607

8 years 
sacerdot 
Porting to new library.



@1606

8 years 
sacerdot 
Porting to last library of Matita.



@1593

8 years 
boender 
 cleaned up Assembly, moved some definitions elsewhere



@1592

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



@1578

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



@1562

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



@1556

8 years 
mulligan 
submitting to avoid conflicts



@1555

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



@1528

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



@1493

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



@1482

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



@1479

8 years 
boender 
 added insert_lookup_opt
 assembly compiles now



@1459

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



@1417

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



@1404

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



@1393

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



@1363

8 years 
boender 
 done stuff with create_label_trie


