Denis Merigoux denismerigoux
denismerigoux
/ gist:1f9659985ef09a7596b1b656dd8c1b65
Created
June 8, 2017 21:41
Effect of early sealing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // When sealing ebb1 before creating the v4 instruction | |
| function ""() { | |
| ebb0: | |
| v0 = iconst.i32 1 | |
| v1 = iconst.i32 2 | |
| v2 = iadd v0, v1 | |
| brnz v1, ebb1 | |
| v3 = iadd v0, v2 | |
| ebb1: |
denismerigoux
/ int_exprs.wast.0.cton
Created
June 19, 2017 23:35
First translation from wasm to Cretonne IL
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| function %(i32, i32) -> i32 { | |
| ebb0(v0: i32, v1: i32): | |
| v2 = iconst.i32 1 | |
| v3 = iadd v2, v0 | |
| v4 = iconst.i32 1 | |
| v5 = iadd v4, v1 | |
| v6 = icmp slt v5, v3 | |
| v7 = sextend.i32 v6 | |
| return v7 | |
| } |
denismerigoux
/ example
Created
August 8, 2017 22:54
Example of ebb splitting that lead to differences in Ebb postorder
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| base_func { | |
| ebb0: | |
| brz ebb1 | |
| jump ebb2 | |
| ebb1: | |
| brz ebb3 | |
| jump ebb3 | |
| ebb2: | |
| jump ebb3 | |
| ebb3: |
denismerigoux
/ Loop statistics
Last active
August 9, 2017 21:57
Diverse Cretonne stats for translated WASM modules
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Setup: the modules are translated into Cretonne IL using wasm2cretonne and the dummy runtime, | |
| then a full-fledge context is created (cfg, dominator tree, loop analysis) and the LICM pass | |
| is run. | |
| ===== cv-wasm.wasm ========== | |
| Loops: 16,978 | |
| Ebbs partially in a loop: 13,229 | |
| Ebb entirely in loop: 64,909 | |
| Ebb total: 162,640 | |
| Splits during analysis: 8 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst b/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst | |
| index e63032e..f0bc332 100644 | |
| --- a/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst | |
| +++ b/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst | |
| @@ -10,10 +10,11 @@ val secret_expand: | |
| expanded:lbuffer uint8 64ul | |
| -> secret:lbuffer uint8 32ul -> | |
| Stack unit | |
| - (requires fun h -> live h expanded /\ live h secret) | |
| + (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret) |
denismerigoux
/ tax_credit.catala
Last active
June 12, 2020 16:15
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /* | |
| # First structure and signatures definitions | |
| declaration structure Person | |
| data name content string | |
| data income content amount | |
| date number_of_children content integer | |
| declaration scope TaxCreditA : |
denismerigoux
/ impots_revenus_2019.py
Last active
October 11, 2020 10:29
Python implementation of the French income tax computation, generated by https://gitlab.inria.fr/verifisc/mlang
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # -*- coding: utf-8 -*- | |
| # File generated by the Mlang compiler | |
| import yaml | |
| from math import floor | |
| class Singleton(type): | |
| _instances = {} |
denismerigoux
/ allocations_familiales.js
Created
February 1, 2021 19:17
Run the French family benefits computation in JS!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| var Law = require("./french_law.js"); | |
| var Benchmark = require("benchmark"); | |
| var suite = new Benchmark.Suite(); | |
| suite | |
| .add("AllocationFamiliales#benchmark", function () { | |
| Law.computeAllocationsFamiliales({ | |
| currentDate: new Date("2020-05-20"), | |
| children: [ | |
| { |
denismerigoux
/ Chacha20.Rustspec.json
Created
April 30, 2021 15:43
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "items": [ | |
| [ | |
| { | |
| "ArrayDecl": [ | |
| [ | |
| "State", | |
| null | |
| ], | |
| [ |
denismerigoux
/ HTML generated by pygmentize for Catala
Created
May 12, 2021 07:48
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <head> | |
| <style> | |
| pre { line-height: 125%; } | |
| td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; } | |
| span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; } | |
| td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; } | |
| span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; } | |
| .catala-code .hll { background-color: #ffffcc } | |
| .catala-code { background: #ffffff; } | |
| .catala-code .c { color: #888888 } /* Comment */ |
OlderNewer