|
|
@2875
|
8 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
@2832
|
8 years |
sacerdot |
Added abstraction in front of cases daemon for code extraction.
|
|
|
@2796
|
8 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
@2782
|
8 years |
sacerdot |
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
|
|
|
@2781
|
8 years |
sacerdot |
One more computational daemon closed.
|
|
|
@2771
|
8 years |
sacerdot |
Some speed up in Policy.ma.
|
|
|
@2770
|
8 years |
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
|
@2767
|
8 years |
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
|
@2764
|
8 years |
sacerdot |
preclassified_system for object code
|
|
|
@2763
|
8 years |
sacerdot |
All daemons in compiler.ma closed (i.e. proof obligations added
to the …
|
|
|
@2762
|
8 years |
sacerdot |
All repaired up to compiler.ma.
Note: one daemon is left for one …
|
|
|
@2761
|
8 years |
sacerdot |
Unused (but not useless) code commented out.
|
|
|
@2760
|
8 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
@2757
|
8 years |
tranquil |
many things are still broken, but there is a partial backtrack on …
|
|
|
@2756
|
8 years |
sacerdot |
WARNING: this commit breaks things, sorry, Paolo is going to fix …
|
|
|
@2754
|
8 years |
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
|
@2750
|
8 years |
mckinna |
Miscellany on 216 bounds, memory, lemmas+definitions.
Completes …
|
|
|
@2745
|
8 years |
sacerdot |
1. Complexity of policy computation lowered from O(n2) to O(n)
2. …
|
|
|
@2714
|
8 years |
sacerdot |
PolicyStep?.ma repaired
|
|
|
@2713
|
8 years |
sacerdot |
PolicyFront?.ma repaired
|
|
|
@2710
|
8 years |
sacerdot |
ASMCosts.ma repaired
|
|
|
@2708
|
8 years |
tranquil |
fixed linearise and LINToASM
LINToASM has now correct transformation …
|
|
|
@2707
|
8 years |
sacerdot |
Assembly repaired.
|
|
|
@2705
|
8 years |
sacerdot |
More progress in ASM towards implementing the new pseudoinstructions.
|
|
|
@2704
|
8 years |
tranquil |
moved JMP from instructions to preinstructions, and added MovSuccessor? …
|
|
|
@2702
|
8 years |
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
|
|
@2700
|
8 years |
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
|
@2688
|
8 years |
tranquil |
* in Arithmeticcs.ma: commented include that breaks script in latest …
|
|
|
@2684
|
8 years |
sacerdot |
…
|
|
|
@2679
|
8 years |
mckinna |
Further tweak to Brian's changes: no normalization reqd at all!
|
|
|
@2676
|
8 years |
campbell |
Less aggressive normalisation in ASMCosts to prevent memory blowup.
|
|
|
@2673
|
8 years |
tranquil |
corrected some compilation errors (that might depend on some matita update)
|
|
|
@2672
|
8 years |
sacerdot |
One less axiom on bitvectors.
|
|
|
@2671
|
8 years |
sacerdot |
simplification
|
|
|
@2665
|
8 years |
sacerdot |
…
|
|
|
@2664
|
8 years |
sacerdot |
Tailcall case implemented (it does not happen ATM).
|
|
|
@2657
|
8 years |
sacerdot |
Cost proof fully repaired. It was broken by the definitions used in …
|
|
|
@2656
|
8 years |
sacerdot |
Ported to tailcalls (currently nothing is classified as a tailcall).
|
|
|
@2653
|
8 years |
sacerdot |
…
|
|
|
@2652
|
8 years |
sacerdot |
String type changed definition.
|
|
|
@2651
|
8 years |
sacerdot |
Type String changed.
|
|
|
@2647
|
8 years |
sacerdot |
Stupid typo fixed.
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
@2643
|
8 years |
sacerdot |
We are not proving erasure, so this is dead code.
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
@2593
|
8 years |
mckinna |
Finally chased down wicked failure to close case 1.1: of …
|
|
|
@2575
|
8 years |
mckinna |
temporary commit
localised the source of trouble in the proof of
…
|
|
|
@2573
|
8 years |
mckinna |
temporary fixes to ensure {compiler,correctness}.ma recompile
after …
|
|
|
@2531
|
8 years |
mckinna |
Trivial tweaks.
|
|
|
@2516
|
8 years |
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
|
|
@2508
|
8 years |
mckinna |
more tweaks. compiler and correctness still build.
|
|
|
@2504
|
8 years |
mckinna |
More refactoring to support the tidied up compiler.ma
|
|
|
@2498
|
8 years |
mckinna |
Refactor:
Typedefs object_code and costlabel_map lifted out from …
|
|
|
@2475
|
8 years |
campbell |
Get compiler.ma and correctness.ma checking again. Note that the …
|
|
|
@2327
|
8 years |
mulligan |
Fixed typos in paper highlighted by referees. More substantial …
|
|
|
@2318
|
8 years |
boender |
- now it compiles
|
|
|
@2317
|
8 years |
boender |
- small changes to make things compile
|
|
|
@2316
|
8 years |
boender |
- committed temporary version: true version has to wait until I …
|
|
|
@2314
|
8 years |
campbell |
Move generic definitions from recent commit to appropriate places.
|
|
|
@2311
|
8 years |
garnier |
Some more cleaning of switchRemoval …
|
|
|
@2307
|
8 years |
campbell |
Half the proofs for sound cost labelling check.
|
|
|
@2301
|
8 years |
mulligan |
Trying to get the big proof working again
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
@2285
|
8 years |
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
|
|
@2284
|
8 years |
sacerdot |
PUSH finished
|
|
|
@2283
|
8 years |
mulligan |
Work from today.
|
|
|
@2282
|
8 years |
sacerdot |
PUSH case almost finished
|
|
|
@2281
|
8 years |
sacerdot |
…
|
|
|
@2280
|
8 years |
sacerdot |
Proof repaired.
|
|
|
@2279
|
8 years |
sacerdot |
1. Bug fixed in the semantics of PUSH (no indirection performed)
2. …
|
|
|
@2278
|
8 years |
mulligan |
Half of JC case complete
|
|
|
@2276
|
8 years |
sacerdot |
…
|
|
|
@2275
|
8 years |
tranquil |
* moved around some code (I8051.ma does not depend on ByteValues?.ma …
|
|
|
@2274
|
8 years |
sacerdot |
Dead code commented out and code out of place moved to Test.ma.
|
|
|
@2273
|
8 years |
sacerdot |
1. lemmas moved from all files to Test.ma
2. most of the lemmas in …
|
|
|
@2272
|
8 years |
mulligan |
Changed proof strategy for main lemma after noticed that the current …
|
|
|
@2270
|
8 years |
mulligan |
Bug spotted and fixed in write_at_stack_pointer
|
|
|
@2269
|
8 years |
sacerdot |
Proof completely repaired up to …
|
|
|
@2268
|
8 years |
mulligan |
Bug spotted in instruction_size (lookup_datalabels cannot just be a …
|
|
|
@2267
|
8 years |
sacerdot |
Call is now proved using the new strategy.
|
|
|
@2266
|
8 years |
sacerdot |
All daemons closed in Jmp case.
|
|
|
@2265
|
8 years |
sacerdot |
Commented out code removed.
|
|
|
@2264
|
8 years |
sacerdot |
1) Major change: we now always use the efficient way of resolving …
|
|
|
@2262
|
8 years |
mulligan |
Changes from today.
|
|
|
@2261
|
8 years |
mulligan |
Resolved conflict
|
|
|
@2260
|
8 years |
sacerdot |
Now we use the efficient lookup_address.
|
|
|
@2259
|
8 years |
mulligan |
For Claudio
|
|
|
@2258
|
8 years |
sacerdot |
1. lemma generalized
2. automation replaced with expansion to make …
|
|
|
@2257
|
8 years |
mulligan |
Daemon in SETB case closed.
|
|
|
@2256
|
8 years |
mulligan |
MOV and MOVX cases complete
|
|
|
@2248
|
8 years |
sacerdot |
Final changes. All daemons removed, but the real one (open goal).
|
|
|
@2247
|
8 years |
mulligan |
Work on the MOV instruction from today and bug fixes in set_arg_1.
|
|
|
@2246
|
8 years |
sacerdot |
Final technical lemma streamlined. Maybe it can be streamlined even more.
|
|
|
@2245
|
8 years |
sacerdot |
Temporary commit to have a backtracking point. Yes, I know this breaks …
|
|
|
@2244
|
8 years |
sacerdot |
Technical lemma used.
|
|
|
@2243
|
8 years |
sacerdot |
One more lemma streamlined, one to go + one to be completed.
|
|
|
@2242
|
8 years |
sacerdot |
jump_expansion_step3 streamlined
|
|
|
@2241
|
8 years |
boender |
- merged changes by Claudio
|
|
|
@2240
|
8 years |
sacerdot |
All "interesting" technical lemmas singled out, proofs to be uncommented.
|
|
|
@2239
|
8 years |
sacerdot |
One more lemma polished.
|
|
|