diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Compilers/Named/DeadCodeElimination.v | 10 | ||||
| -rw-r--r-- | src/Compilers/Named/DeadCodeEliminationInterp.v | 67 | ||||
| -rw-r--r-- | src/Compilers/Z/Named/DeadCodeElimination.v | 4 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v | 2 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestLadderstep130Display.log | 517 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestSubDisplay.log | 59 |
7 files changed, 287 insertions, 373 deletions
diff --git a/_CoqProject b/_CoqProject index 2422bb9f1..6f0bdce2f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -82,6 +82,7 @@ src/Compilers/Named/ContextOn.v src/Compilers/Named/ContextProperties.v src/Compilers/Named/CountLets.v src/Compilers/Named/DeadCodeElimination.v +src/Compilers/Named/DeadCodeEliminationInterp.v src/Compilers/Named/EstablishLiveness.v src/Compilers/Named/FMapContext.v src/Compilers/Named/GetNames.v diff --git a/src/Compilers/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v index 22e823fd1..340c5dd0d 100644 --- a/src/Compilers/Named/DeadCodeElimination.v +++ b/src/Compilers/Named/DeadCodeElimination.v @@ -20,6 +20,8 @@ Section language. Context (base_type_code : Type) (op : flat_type base_type_code -> flat_type base_type_code -> Type) (Name : Type) + {base_type_code_beq : base_type_code -> base_type_code -> bool} + (base_type_code_bl : forall t1 t2, base_type_code_beq t1 t2 = true -> t1 = t2) {Context : Context Name (fun _ : base_type_code => positive)}. Local Notation flat_type := (flat_type base_type_code). @@ -30,11 +32,13 @@ Section language. Local Notation nexprf := (@Named.exprf base_type_code op Name). Local Notation nexpr := (@Named.expr base_type_code op Name). + Local Notation PContext var := (@PositiveContext base_type_code var base_type_code_beq base_type_code_bl). + Definition EliminateDeadCode {t} (e : @Named.expr base_type_code op _ t) (ls : list Name) : option (nexpr t) := Let_In (insert_dead_names (Context:=PositiveContext_nd) None e ls) (* help vm_compute by factoring this out *) - (fun names => register_reassign (InContext:=PositiveContext_nd) (ReverseContext:=Context) Pos.eqb empty empty e names). + (fun names => register_reassign (InContext:=PContext _) (ReverseContext:=Context) Pos.eqb empty empty e names). Definition CompileAndEliminateDeadCode {t} (e : Expr t) (ls : list Name) @@ -46,5 +50,5 @@ Section language. end. End language. -Global Arguments EliminateDeadCode {_ _ _ _ t} e ls. -Global Arguments CompileAndEliminateDeadCode {_ _ _ _ t} e ls. +Global Arguments EliminateDeadCode {_ _ _ _ _ _ t} e ls. +Global Arguments CompileAndEliminateDeadCode {_ _ _ _ _ _ t} e ls. diff --git a/src/Compilers/Named/DeadCodeEliminationInterp.v b/src/Compilers/Named/DeadCodeEliminationInterp.v new file mode 100644 index 000000000..185a84acd --- /dev/null +++ b/src/Compilers/Named/DeadCodeEliminationInterp.v @@ -0,0 +1,67 @@ +Require Import Coq.PArith.BinPos. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.PositiveContext. +Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Compilers.Named.RegisterAssignInterp. +Require Import Crypto.Compilers.Named.DeadCodeElimination. +Require Import Crypto.Util.Decidable. + +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {interp_base_type : base_type_code -> Type} + {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d} + {Name : Type} + {InContext : Context Name (fun _ : base_type_code => BinNums.positive)} + {InContextOk : ContextOk InContext} + {Name_beq : Name -> Name -> bool} + {InterpContext : Context Name interp_base_type} + {InterpContextOk : ContextOk InterpContext} + {base_type_code_beq : base_type_code -> base_type_code -> bool} + (base_type_code_bl : forall t1 t2, base_type_code_beq t1 t2 = true -> t1 = t2) + (base_type_code_lb : forall t1 t2, t1 = t2 -> base_type_code_beq t1 t2 = true) + (Name_bl : forall n1 n2, Name_beq n1 n2 = true -> n1 = n2) + (Name_lb : forall n1 n2, n1 = n2 -> Name_beq n1 n2 = true). + + Local Notation EliminateDeadCode := (@EliminateDeadCode base_type_code op Name _ base_type_code_bl InContext). + Local Notation PContext var := (@PositiveContext base_type_code var base_type_code_beq base_type_code_bl). + + Local Instance Name_dec : DecidableRel (@eq Name) + := dec_rel_of_bool_dec_rel Name_beq Name_bl Name_lb. + Local Instance base_type_code_dec : DecidableRel (@eq base_type_code) + := dec_rel_of_bool_dec_rel base_type_code_beq base_type_code_bl base_type_code_lb. + + Lemma interp_EliminateDeadCode + t e new_names + (ctxi_interp : PositiveContext _ _ base_type_code_beq base_type_code_bl) + (ctxr_interp : InterpContext) + eout v1 v2 x + : @EliminateDeadCode t e new_names = Some eout + -> interp (interp_op:=interp_op) (ctx:=ctxr_interp) eout x = Some v1 + -> interp (interp_op:=interp_op) (ctx:=ctxi_interp) e x = Some v2 + -> v1 = v2. + Proof using InContextOk InterpContextOk Name_bl Name_lb base_type_code_lb. + eapply @interp_register_reassign; + first [ assumption + | apply @PositiveContextOk; assumption + | apply Peqb_true_eq + | apply Pos.eqb_eq + | exact _ + | intros *; rewrite !lookupb_empty by (try apply @PositiveContextOk; assumption); + congruence ]. + Qed. + + Lemma InterpEliminateDeadCode + t e new_names + eout + v1 v2 x + : @EliminateDeadCode t e new_names = Some eout + -> Interp (Context:=InterpContext) (interp_op:=interp_op) eout x = Some v1 + -> Interp (Context:=PContext _) (interp_op:=interp_op) e x = Some v2 + -> v1 = v2. + Proof using InContextOk InterpContextOk Name_bl Name_lb base_type_code_lb. + apply interp_EliminateDeadCode. + Qed. +End language. diff --git a/src/Compilers/Z/Named/DeadCodeElimination.v b/src/Compilers/Z/Named/DeadCodeElimination.v index b74064ff9..449494e74 100644 --- a/src/Compilers/Z/Named/DeadCodeElimination.v +++ b/src/Compilers/Z/Named/DeadCodeElimination.v @@ -8,7 +8,7 @@ Section language. {Context : Context Name (fun _ : base_type => positive)}. Definition EliminateDeadCode {t} e ls - := @EliminateDeadCode base_type op Name Context t e ls. + := @EliminateDeadCode base_type op Name _ internal_base_type_dec_bl Context t e ls. Definition CompileAndEliminateDeadCode {t} e ls - := @CompileAndEliminateDeadCode base_type op Name Context t e ls. + := @CompileAndEliminateDeadCode base_type op Name _ internal_base_type_dec_bl Context t e ls. End language. diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index cd54402ea..e28196f43 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -228,7 +228,7 @@ Section assemble. Definition AssembleSyntax' {t} (e : Expr base_type op t) (ls : list Register) : option (syntax t) - := CompileAndEliminateDeadCode (Context:=RegisterContext) e ls. + := CompileAndEliminateDeadCode (base_type_code_bl:=internal_base_type_dec_bl) (Context:=RegisterContext) e ls. Definition AssembleSyntax {t} e ls (res := @AssembleSyntax' t e ls) := match res return match res with None => _ | _ => _ end with | Some v => v diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log index c60adbe6e..95f2237c0 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.log +++ b/src/Specific/IntegrationTestLadderstep130Display.log @@ -5,365 +5,214 @@ let (a, b) := Interp-η uint128_t x33 = x17 + x21; uint128_t x34 = x18 + x22; uint128_t x35 = x16 + x20; - uint128_t x36 = 0x3ffffffffffffffffffffeL + x17; - uint128_t x37 = x36 - x21; - uint128_t x38 = 0x3ffffffffffffffffffffeL + x18; - uint128_t x39 = x38 - x22; - uint128_t x40 = 0x3ffffffffffffffffffff6L + x16; - uint128_t x41 = x40 - x20; - uint256_t x42 = (uint256_t) x35 * x33; - uint256_t x43 = (uint256_t) x34 * x34; - uint256_t x44 = (uint256_t) x33 * x35; - uint256_t x45 = x43 + x44; - uint256_t x46 = x42 + x45; - uint256_t x47 = (uint256_t) x35 * x34; - uint256_t x48 = (uint256_t) x34 * x35; - uint256_t x49 = x47 + x48; - uint256_t x50 = (uint256_t) x33 * x33; - uint256_t x51 = 0x5 * x50; - uint256_t x52 = x49 + x51; - uint256_t x53 = (uint256_t) x35 * x35; - uint256_t x54 = (uint256_t) x34 * x33; - uint256_t x55 = (uint256_t) x33 * x34; - uint256_t x56 = x54 + x55; - uint256_t x57 = 0x5 * x56; - uint256_t x58 = x53 + x57; - uint128_t x59 = (uint128_t) (x58 >> 0x55); - uint128_t x60 = (uint128_t) x58 & 0x1fffffffffffffffffffffL; - uint256_t x61 = x59 + x52; - uint128_t x62 = (uint128_t) (x61 >> 0x55); - uint128_t x63 = (uint128_t) x61 & 0x1fffffffffffffffffffffL; - uint256_t x64 = x62 + x46; - uint128_t x65 = (uint128_t) (x64 >> 0x55); - uint128_t x66 = (uint128_t) x64 & 0x1fffffffffffffffffffffL; - uint128_t x67 = 0x5 * x65; - uint128_t x68 = x60 + x67; + uint128_t x36 = 0x3ffffffffffffffffffffeL + x17 - x21; + uint128_t x37 = 0x3ffffffffffffffffffffeL + x18 - x22; + uint128_t x38 = 0x3ffffffffffffffffffff6L + x16 - x20; + uint256_t x39 = (uint256_t) x35 * x33 + ((uint256_t) x34 * x34 + (uint256_t) x33 * x35); + uint256_t x40 = (uint256_t) x35 * x34 + (uint256_t) x34 * x35 + 0x5 * ((uint256_t) x33 * x33); + uint256_t x41 = (uint256_t) x35 * x35 + 0x5 * ((uint256_t) x34 * x33 + (uint256_t) x33 * x34); + uint128_t x42 = (uint128_t) (x41 >> 0x55); + uint128_t x43 = (uint128_t) x41 & 0x1fffffffffffffffffffffL; + uint256_t x44 = x42 + x40; + uint128_t x45 = (uint128_t) (x44 >> 0x55); + uint128_t x46 = (uint128_t) x44 & 0x1fffffffffffffffffffffL; + uint256_t x47 = x45 + x39; + uint128_t x48 = (uint128_t) (x47 >> 0x55); + uint128_t x49 = (uint128_t) x47 & 0x1fffffffffffffffffffffL; + uint128_t x50 = x43 + 0x5 * x48; + uint128_t x51 = x50 >> 0x55; + uint128_t x52 = x50 & 0x1fffffffffffffffffffffL; + uint128_t x53 = x51 + x46; + uint128_t x54 = x53 >> 0x55; + uint128_t x55 = x53 & 0x1fffffffffffffffffffffL; + uint128_t x56 = x54 + x49; + uint256_t x57 = (uint256_t) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38); + uint256_t x58 = (uint256_t) x38 * x37 + (uint256_t) x37 * x38 + 0x5 * ((uint256_t) x36 * x36); + uint256_t x59 = (uint256_t) x38 * x38 + 0x5 * ((uint256_t) x37 * x36 + (uint256_t) x36 * x37); + uint128_t x60 = (uint128_t) (x59 >> 0x55); + uint128_t x61 = (uint128_t) x59 & 0x1fffffffffffffffffffffL; + uint256_t x62 = x60 + x58; + uint128_t x63 = (uint128_t) (x62 >> 0x55); + uint128_t x64 = (uint128_t) x62 & 0x1fffffffffffffffffffffL; + uint256_t x65 = x63 + x57; + uint128_t x66 = (uint128_t) (x65 >> 0x55); + uint128_t x67 = (uint128_t) x65 & 0x1fffffffffffffffffffffL; + uint128_t x68 = x61 + 0x5 * x66; uint128_t x69 = x68 >> 0x55; uint128_t x70 = x68 & 0x1fffffffffffffffffffffL; - uint128_t x71 = x69 + x63; + uint128_t x71 = x69 + x64; uint128_t x72 = x71 >> 0x55; uint128_t x73 = x71 & 0x1fffffffffffffffffffffL; - uint128_t x74 = x72 + x66; - uint256_t x75 = (uint256_t) x41 * x37; - uint256_t x76 = (uint256_t) x39 * x39; - uint256_t x77 = (uint256_t) x37 * x41; - uint256_t x78 = x76 + x77; - uint256_t x79 = x75 + x78; - uint256_t x80 = (uint256_t) x41 * x39; - uint256_t x81 = (uint256_t) x39 * x41; - uint256_t x82 = x80 + x81; - uint256_t x83 = (uint256_t) x37 * x37; - uint256_t x84 = 0x5 * x83; - uint256_t x85 = x82 + x84; - uint256_t x86 = (uint256_t) x41 * x41; - uint256_t x87 = (uint256_t) x39 * x37; - uint256_t x88 = (uint256_t) x37 * x39; - uint256_t x89 = x87 + x88; - uint256_t x90 = 0x5 * x89; - uint256_t x91 = x86 + x90; - uint128_t x92 = (uint128_t) (x91 >> 0x55); - uint128_t x93 = (uint128_t) x91 & 0x1fffffffffffffffffffffL; - uint256_t x94 = x92 + x85; - uint128_t x95 = (uint128_t) (x94 >> 0x55); - uint128_t x96 = (uint128_t) x94 & 0x1fffffffffffffffffffffL; - uint256_t x97 = x95 + x79; - uint128_t x98 = (uint128_t) (x97 >> 0x55); - uint128_t x99 = (uint128_t) x97 & 0x1fffffffffffffffffffffL; - uint128_t x100 = 0x5 * x98; - uint128_t x101 = x93 + x100; + uint128_t x74 = x72 + x67; + uint256_t x75 = (uint256_t) x52 * x74 + ((uint256_t) x55 * x73 + (uint256_t) x56 * x70); + uint256_t x76 = (uint256_t) x52 * x73 + (uint256_t) x55 * x70 + 0x5 * ((uint256_t) x56 * x74); + uint256_t x77 = (uint256_t) x52 * x70 + 0x5 * ((uint256_t) x55 * x74 + (uint256_t) x56 * x73); + uint128_t x78 = (uint128_t) (x77 >> 0x55); + uint128_t x79 = (uint128_t) x77 & 0x1fffffffffffffffffffffL; + uint256_t x80 = x78 + x76; + uint128_t x81 = (uint128_t) (x80 >> 0x55); + uint128_t x82 = (uint128_t) x80 & 0x1fffffffffffffffffffffL; + uint256_t x83 = x81 + x75; + uint128_t x84 = (uint128_t) (x83 >> 0x55); + uint128_t x85 = (uint128_t) x83 & 0x1fffffffffffffffffffffL; + uint128_t x86 = x79 + 0x5 * x84; + uint128_t x87 = x86 >> 0x55; + uint128_t x88 = x86 & 0x1fffffffffffffffffffffL; + uint128_t x89 = x87 + x82; + uint128_t x90 = x89 >> 0x55; + uint128_t x91 = x89 & 0x1fffffffffffffffffffffL; + uint128_t x92 = x90 + x85; + uint128_t x93 = 0x3ffffffffffffffffffffeL + x56 - x74; + uint128_t x94 = 0x3ffffffffffffffffffffeL + x55 - x73; + uint128_t x95 = 0x3ffffffffffffffffffff6L + x52 - x70; + uint128_t x96 = 0x1db41 * x93; + uint128_t x97 = 0x1db41 * x94; + uint128_t x98 = 0x1db41 * x95; + uint128_t x99 = x98 >> 0x55; + uint128_t x100 = x98 & 0x1fffffffffffffffffffffL; + uint128_t x101 = x99 + x97; uint128_t x102 = x101 >> 0x55; uint128_t x103 = x101 & 0x1fffffffffffffffffffffL; uint128_t x104 = x102 + x96; uint128_t x105 = x104 >> 0x55; uint128_t x106 = x104 & 0x1fffffffffffffffffffffL; - uint128_t x107 = x105 + x99; - uint256_t x108 = (uint256_t) x70 * x107; - uint256_t x109 = (uint256_t) x73 * x106; - uint256_t x110 = (uint256_t) x74 * x103; - uint256_t x111 = x109 + x110; - uint256_t x112 = x108 + x111; - uint256_t x113 = (uint256_t) x70 * x106; - uint256_t x114 = (uint256_t) x73 * x103; - uint256_t x115 = x113 + x114; - uint256_t x116 = (uint256_t) x74 * x107; - uint256_t x117 = 0x5 * x116; - uint256_t x118 = x115 + x117; - uint256_t x119 = (uint256_t) x70 * x103; - uint256_t x120 = (uint256_t) x73 * x107; - uint256_t x121 = (uint256_t) x74 * x106; - uint256_t x122 = x120 + x121; - uint256_t x123 = 0x5 * x122; - uint256_t x124 = x119 + x123; - uint128_t x125 = (uint128_t) (x124 >> 0x55); - uint128_t x126 = (uint128_t) x124 & 0x1fffffffffffffffffffffL; - uint256_t x127 = x125 + x118; - uint128_t x128 = (uint128_t) (x127 >> 0x55); - uint128_t x129 = (uint128_t) x127 & 0x1fffffffffffffffffffffL; - uint256_t x130 = x128 + x112; - uint128_t x131 = (uint128_t) (x130 >> 0x55); - uint128_t x132 = (uint128_t) x130 & 0x1fffffffffffffffffffffL; - uint128_t x133 = 0x5 * x131; - uint128_t x134 = x126 + x133; - uint128_t x135 = x134 >> 0x55; - uint128_t x136 = x134 & 0x1fffffffffffffffffffffL; - uint128_t x137 = x135 + x129; - uint128_t x138 = x137 >> 0x55; - uint128_t x139 = x137 & 0x1fffffffffffffffffffffL; - uint128_t x140 = x138 + x132; - uint128_t x141 = 0x3ffffffffffffffffffffeL + x74; - uint128_t x142 = x141 - x107; - uint128_t x143 = 0x3ffffffffffffffffffffeL + x73; - uint128_t x144 = x143 - x106; - uint128_t x145 = 0x3ffffffffffffffffffff6L + x70; - uint128_t x146 = x145 - x103; - uint128_t x147 = 0x1db41 * x142; - uint128_t x148 = 0x1db41 * x144; - uint128_t x149 = 0x1db41 * x146; - uint128_t x150 = x149 >> 0x55; - uint128_t x151 = x149 & 0x1fffffffffffffffffffffL; - uint128_t x152 = x150 + x148; + uint128_t x107 = x100 + 0x5 * x105; + uint128_t x108 = x107 >> 0x55; + uint128_t x109 = x107 & 0x1fffffffffffffffffffffL; + uint128_t x110 = x108 + x103; + uint128_t x111 = x110 >> 0x55; + uint128_t x112 = x110 & 0x1fffffffffffffffffffffL; + uint128_t x113 = x111 + x106; + uint128_t x114 = x56 + x113; + uint128_t x115 = x55 + x112; + uint128_t x116 = x52 + x109; + uint256_t x117 = (uint256_t) x95 * x114 + ((uint256_t) x94 * x115 + (uint256_t) x93 * x116); + uint256_t x118 = (uint256_t) x95 * x115 + (uint256_t) x94 * x116 + 0x5 * ((uint256_t) x93 * x114); + uint256_t x119 = (uint256_t) x95 * x116 + 0x5 * ((uint256_t) x94 * x114 + (uint256_t) x93 * x115); + uint128_t x120 = (uint128_t) (x119 >> 0x55); + uint128_t x121 = (uint128_t) x119 & 0x1fffffffffffffffffffffL; + uint256_t x122 = x120 + x118; + uint128_t x123 = (uint128_t) (x122 >> 0x55); + uint128_t x124 = (uint128_t) x122 & 0x1fffffffffffffffffffffL; + uint256_t x125 = x123 + x117; + uint128_t x126 = (uint128_t) (x125 >> 0x55); + uint128_t x127 = (uint128_t) x125 & 0x1fffffffffffffffffffffL; + uint128_t x128 = x121 + 0x5 * x126; + uint128_t x129 = x128 >> 0x55; + uint128_t x130 = x128 & 0x1fffffffffffffffffffffL; + uint128_t x131 = x129 + x124; + uint128_t x132 = x131 >> 0x55; + uint128_t x133 = x131 & 0x1fffffffffffffffffffffL; + uint128_t x134 = x132 + x127; + uint128_t x135 = x27 + x31; + uint128_t x136 = x28 + x32; + uint128_t x137 = x26 + x30; + uint128_t x138 = 0x3ffffffffffffffffffffeL + x27 - x31; + uint128_t x139 = 0x3ffffffffffffffffffffeL + x28 - x32; + uint128_t x140 = 0x3ffffffffffffffffffff6L + x26 - x30; + uint256_t x141 = (uint256_t) x137 * x36 + ((uint256_t) x136 * x37 + (uint256_t) x135 * x38); + uint256_t x142 = (uint256_t) x137 * x37 + (uint256_t) x136 * x38 + 0x5 * ((uint256_t) x135 * x36); + uint256_t x143 = (uint256_t) x137 * x38 + 0x5 * ((uint256_t) x136 * x36 + (uint256_t) x135 * x37); + uint128_t x144 = (uint128_t) (x143 >> 0x55); + uint128_t x145 = (uint128_t) x143 & 0x1fffffffffffffffffffffL; + uint256_t x146 = x144 + x142; + uint128_t x147 = (uint128_t) (x146 >> 0x55); + uint128_t x148 = (uint128_t) x146 & 0x1fffffffffffffffffffffL; + uint256_t x149 = x147 + x141; + uint128_t x150 = (uint128_t) (x149 >> 0x55); + uint128_t x151 = (uint128_t) x149 & 0x1fffffffffffffffffffffL; + uint128_t x152 = x145 + 0x5 * x150; uint128_t x153 = x152 >> 0x55; uint128_t x154 = x152 & 0x1fffffffffffffffffffffL; - uint128_t x155 = x153 + x147; + uint128_t x155 = x153 + x148; uint128_t x156 = x155 >> 0x55; uint128_t x157 = x155 & 0x1fffffffffffffffffffffL; - uint128_t x158 = 0x5 * x156; - uint128_t x159 = x151 + x158; - uint128_t x160 = x159 >> 0x55; - uint128_t x161 = x159 & 0x1fffffffffffffffffffffL; - uint128_t x162 = x160 + x154; - uint128_t x163 = x162 >> 0x55; - uint128_t x164 = x162 & 0x1fffffffffffffffffffffL; - uint128_t x165 = x163 + x157; - uint128_t x166 = x74 + x165; - uint128_t x167 = x73 + x164; - uint128_t x168 = x70 + x161; - uint256_t x169 = (uint256_t) x146 * x166; - uint256_t x170 = (uint256_t) x144 * x167; - uint256_t x171 = (uint256_t) x142 * x168; - uint256_t x172 = x170 + x171; - uint256_t x173 = x169 + x172; - uint256_t x174 = (uint256_t) x146 * x167; - uint256_t x175 = (uint256_t) x144 * x168; - uint256_t x176 = x174 + x175; - uint256_t x177 = (uint256_t) x142 * x166; - uint256_t x178 = 0x5 * x177; - uint256_t x179 = x176 + x178; - uint256_t x180 = (uint256_t) x146 * x168; - uint256_t x181 = (uint256_t) x144 * x166; - uint256_t x182 = (uint256_t) x142 * x167; - uint256_t x183 = x181 + x182; - uint256_t x184 = 0x5 * x183; - uint256_t x185 = x180 + x184; + uint128_t x158 = x156 + x151; + uint256_t x159 = (uint256_t) x140 * x33 + ((uint256_t) x139 * x34 + (uint256_t) x138 * x35); + uint256_t x160 = (uint256_t) x140 * x34 + (uint256_t) x139 * x35 + 0x5 * ((uint256_t) x138 * x33); + uint256_t x161 = (uint256_t) x140 * x35 + 0x5 * ((uint256_t) x139 * x33 + (uint256_t) x138 * x34); + uint128_t x162 = (uint128_t) (x161 >> 0x55); + uint128_t x163 = (uint128_t) x161 & 0x1fffffffffffffffffffffL; + uint256_t x164 = x162 + x160; + uint128_t x165 = (uint128_t) (x164 >> 0x55); + uint128_t x166 = (uint128_t) x164 & 0x1fffffffffffffffffffffL; + uint256_t x167 = x165 + x159; + uint128_t x168 = (uint128_t) (x167 >> 0x55); + uint128_t x169 = (uint128_t) x167 & 0x1fffffffffffffffffffffL; + uint128_t x170 = x163 + 0x5 * x168; + uint128_t x171 = x170 >> 0x55; + uint128_t x172 = x170 & 0x1fffffffffffffffffffffL; + uint128_t x173 = x171 + x166; + uint128_t x174 = x173 >> 0x55; + uint128_t x175 = x173 & 0x1fffffffffffffffffffffL; + uint128_t x176 = x174 + x169; + uint128_t x177 = x176 + x158; + uint128_t x178 = x175 + x157; + uint128_t x179 = x172 + x154; + uint128_t x180 = x176 + x158; + uint128_t x181 = x175 + x157; + uint128_t x182 = x172 + x154; + uint256_t x183 = (uint256_t) x179 * x180 + ((uint256_t) x178 * x181 + (uint256_t) x177 * x182); + uint256_t x184 = (uint256_t) x179 * x181 + (uint256_t) x178 * x182 + 0x5 * ((uint256_t) x177 * x180); + uint256_t x185 = (uint256_t) x179 * x182 + 0x5 * ((uint256_t) x178 * x180 + (uint256_t) x177 * x181); uint128_t x186 = (uint128_t) (x185 >> 0x55); uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; - uint256_t x188 = x186 + x179; + uint256_t x188 = x186 + x184; uint128_t x189 = (uint128_t) (x188 >> 0x55); uint128_t x190 = (uint128_t) x188 & 0x1fffffffffffffffffffffL; - uint256_t x191 = x189 + x173; + uint256_t x191 = x189 + x183; uint128_t x192 = (uint128_t) (x191 >> 0x55); uint128_t x193 = (uint128_t) x191 & 0x1fffffffffffffffffffffL; - uint128_t x194 = 0x5 * x192; - uint128_t x195 = x187 + x194; - uint128_t x196 = x195 >> 0x55; - uint128_t x197 = x195 & 0x1fffffffffffffffffffffL; - uint128_t x198 = x196 + x190; - uint128_t x199 = x198 >> 0x55; - uint128_t x200 = x198 & 0x1fffffffffffffffffffffL; - uint128_t x201 = x199 + x193; - uint128_t x202 = x27 + x31; - uint128_t x203 = x28 + x32; - uint128_t x204 = x26 + x30; - uint128_t x205 = 0x3ffffffffffffffffffffeL + x27; - uint128_t x206 = x205 - x31; - uint128_t x207 = 0x3ffffffffffffffffffffeL + x28; - uint128_t x208 = x207 - x32; - uint128_t x209 = 0x3ffffffffffffffffffff6L + x26; - uint128_t x210 = x209 - x30; - uint256_t x211 = (uint256_t) x204 * x37; - uint256_t x212 = (uint256_t) x203 * x39; - uint256_t x213 = (uint256_t) x202 * x41; - uint256_t x214 = x212 + x213; - uint256_t x215 = x211 + x214; - uint256_t x216 = (uint256_t) x204 * x39; - uint256_t x217 = (uint256_t) x203 * x41; - uint256_t x218 = x216 + x217; - uint256_t x219 = (uint256_t) x202 * x37; - uint256_t x220 = 0x5 * x219; - uint256_t x221 = x218 + x220; - uint256_t x222 = (uint256_t) x204 * x41; - uint256_t x223 = (uint256_t) x203 * x37; - uint256_t x224 = (uint256_t) x202 * x39; - uint256_t x225 = x223 + x224; - uint256_t x226 = 0x5 * x225; - uint256_t x227 = x222 + x226; + uint128_t x194 = x187 + 0x5 * x192; + uint128_t x195 = x194 >> 0x55; + uint128_t x196 = x194 & 0x1fffffffffffffffffffffL; + uint128_t x197 = x195 + x190; + uint128_t x198 = x197 >> 0x55; + uint128_t x199 = x197 & 0x1fffffffffffffffffffffL; + uint128_t x200 = x198 + x193; + uint128_t x201 = 0x3ffffffffffffffffffffeL + x176 - x158; + uint128_t x202 = 0x3ffffffffffffffffffffeL + x175 - x157; + uint128_t x203 = 0x3ffffffffffffffffffff6L + x172 - x154; + uint128_t x204 = 0x3ffffffffffffffffffffeL + x176 - x158; + uint128_t x205 = 0x3ffffffffffffffffffffeL + x175 - x157; + uint128_t x206 = 0x3ffffffffffffffffffff6L + x172 - x154; + uint256_t x207 = (uint256_t) x203 * x204 + ((uint256_t) x202 * x205 + (uint256_t) x201 * x206); + uint256_t x208 = (uint256_t) x203 * x205 + (uint256_t) x202 * x206 + 0x5 * ((uint256_t) x201 * x204); + uint256_t x209 = (uint256_t) x203 * x206 + 0x5 * ((uint256_t) x202 * x204 + (uint256_t) x201 * x205); + uint128_t x210 = (uint128_t) (x209 >> 0x55); + uint128_t x211 = (uint128_t) x209 & 0x1fffffffffffffffffffffL; + uint256_t x212 = x210 + x208; + uint128_t x213 = (uint128_t) (x212 >> 0x55); + uint128_t x214 = (uint128_t) x212 & 0x1fffffffffffffffffffffL; + uint256_t x215 = x213 + x207; + uint128_t x216 = (uint128_t) (x215 >> 0x55); + uint128_t x217 = (uint128_t) x215 & 0x1fffffffffffffffffffffL; + uint128_t x218 = x211 + 0x5 * x216; + uint128_t x219 = x218 >> 0x55; + uint128_t x220 = x218 & 0x1fffffffffffffffffffffL; + uint128_t x221 = x219 + x214; + uint128_t x222 = x221 >> 0x55; + uint128_t x223 = x221 & 0x1fffffffffffffffffffffL; + uint128_t x224 = x222 + x217; + uint256_t x225 = (uint256_t) x10 * x224 + ((uint256_t) x12 * x223 + (uint256_t) x11 * x220); + uint256_t x226 = (uint256_t) x10 * x223 + (uint256_t) x12 * x220 + 0x5 * ((uint256_t) x11 * x224); + uint256_t x227 = (uint256_t) x10 * x220 + 0x5 * ((uint256_t) x12 * x224 + (uint256_t) x11 * x223); uint128_t x228 = (uint128_t) (x227 >> 0x55); uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; - uint256_t x230 = x228 + x221; + uint256_t x230 = x228 + x226; uint128_t x231 = (uint128_t) (x230 >> 0x55); uint128_t x232 = (uint128_t) x230 & 0x1fffffffffffffffffffffL; - uint256_t x233 = x231 + x215; + uint256_t x233 = x231 + x225; uint128_t x234 = (uint128_t) (x233 >> 0x55); uint128_t x235 = (uint128_t) x233 & 0x1fffffffffffffffffffffL; - uint128_t x236 = 0x5 * x234; - uint128_t x237 = x229 + x236; - uint128_t x238 = x237 >> 0x55; - uint128_t x239 = x237 & 0x1fffffffffffffffffffffL; - uint128_t x240 = x238 + x232; - uint128_t x241 = x240 >> 0x55; - uint128_t x242 = x240 & 0x1fffffffffffffffffffffL; - uint128_t x243 = x241 + x235; - uint256_t x244 = (uint256_t) x210 * x33; - uint256_t x245 = (uint256_t) x208 * x34; - uint256_t x246 = (uint256_t) x206 * x35; - uint256_t x247 = x245 + x246; - uint256_t x248 = x244 + x247; - uint256_t x249 = (uint256_t) x210 * x34; - uint256_t x250 = (uint256_t) x208 * x35; - uint256_t x251 = x249 + x250; - uint256_t x252 = (uint256_t) x206 * x33; - uint256_t x253 = 0x5 * x252; - uint256_t x254 = x251 + x253; - uint256_t x255 = (uint256_t) x210 * x35; - uint256_t x256 = (uint256_t) x208 * x33; - uint256_t x257 = (uint256_t) x206 * x34; - uint256_t x258 = x256 + x257; - uint256_t x259 = 0x5 * x258; - uint256_t x260 = x255 + x259; - uint128_t x261 = (uint128_t) (x260 >> 0x55); - uint128_t x262 = (uint128_t) x260 & 0x1fffffffffffffffffffffL; - uint256_t x263 = x261 + x254; - uint128_t x264 = (uint128_t) (x263 >> 0x55); - uint128_t x265 = (uint128_t) x263 & 0x1fffffffffffffffffffffL; - uint256_t x266 = x264 + x248; - uint128_t x267 = (uint128_t) (x266 >> 0x55); - uint128_t x268 = (uint128_t) x266 & 0x1fffffffffffffffffffffL; - uint128_t x269 = 0x5 * x267; - uint128_t x270 = x262 + x269; - uint128_t x271 = x270 >> 0x55; - uint128_t x272 = x270 & 0x1fffffffffffffffffffffL; - uint128_t x273 = x271 + x265; - uint128_t x274 = x273 >> 0x55; - uint128_t x275 = x273 & 0x1fffffffffffffffffffffL; - uint128_t x276 = x274 + x268; - uint128_t x277 = x276 + x243; - uint128_t x278 = x275 + x242; - uint128_t x279 = x272 + x239; - uint128_t x280 = x276 + x243; - uint128_t x281 = x275 + x242; - uint128_t x282 = x272 + x239; - uint256_t x283 = (uint256_t) x279 * x280; - uint256_t x284 = (uint256_t) x278 * x281; - uint256_t x285 = (uint256_t) x277 * x282; - uint256_t x286 = x284 + x285; - uint256_t x287 = x283 + x286; - uint256_t x288 = (uint256_t) x279 * x281; - uint256_t x289 = (uint256_t) x278 * x282; - uint256_t x290 = x288 + x289; - uint256_t x291 = (uint256_t) x277 * x280; - uint256_t x292 = 0x5 * x291; - uint256_t x293 = x290 + x292; - uint256_t x294 = (uint256_t) x279 * x282; - uint256_t x295 = (uint256_t) x278 * x280; - uint256_t x296 = (uint256_t) x277 * x281; - uint256_t x297 = x295 + x296; - uint256_t x298 = 0x5 * x297; - uint256_t x299 = x294 + x298; - uint128_t x300 = (uint128_t) (x299 >> 0x55); - uint128_t x301 = (uint128_t) x299 & 0x1fffffffffffffffffffffL; - uint256_t x302 = x300 + x293; - uint128_t x303 = (uint128_t) (x302 >> 0x55); - uint128_t x304 = (uint128_t) x302 & 0x1fffffffffffffffffffffL; - uint256_t x305 = x303 + x287; - uint128_t x306 = (uint128_t) (x305 >> 0x55); - uint128_t x307 = (uint128_t) x305 & 0x1fffffffffffffffffffffL; - uint128_t x308 = 0x5 * x306; - uint128_t x309 = x301 + x308; - uint128_t x310 = x309 >> 0x55; - uint128_t x311 = x309 & 0x1fffffffffffffffffffffL; - uint128_t x312 = x310 + x304; - uint128_t x313 = x312 >> 0x55; - uint128_t x314 = x312 & 0x1fffffffffffffffffffffL; - uint128_t x315 = x313 + x307; - uint128_t x316 = 0x3ffffffffffffffffffffeL + x276; - uint128_t x317 = x316 - x243; - uint128_t x318 = 0x3ffffffffffffffffffffeL + x275; - uint128_t x319 = x318 - x242; - uint128_t x320 = 0x3ffffffffffffffffffff6L + x272; - uint128_t x321 = x320 - x239; - uint128_t x322 = 0x3ffffffffffffffffffffeL + x276; - uint128_t x323 = x322 - x243; - uint128_t x324 = 0x3ffffffffffffffffffffeL + x275; - uint128_t x325 = x324 - x242; - uint128_t x326 = 0x3ffffffffffffffffffff6L + x272; - uint128_t x327 = x326 - x239; - uint256_t x328 = (uint256_t) x321 * x323; - uint256_t x329 = (uint256_t) x319 * x325; - uint256_t x330 = (uint256_t) x317 * x327; - uint256_t x331 = x329 + x330; - uint256_t x332 = x328 + x331; - uint256_t x333 = (uint256_t) x321 * x325; - uint256_t x334 = (uint256_t) x319 * x327; - uint256_t x335 = x333 + x334; - uint256_t x336 = (uint256_t) x317 * x323; - uint256_t x337 = 0x5 * x336; - uint256_t x338 = x335 + x337; - uint256_t x339 = (uint256_t) x321 * x327; - uint256_t x340 = (uint256_t) x319 * x323; - uint256_t x341 = (uint256_t) x317 * x325; - uint256_t x342 = x340 + x341; - uint256_t x343 = 0x5 * x342; - uint256_t x344 = x339 + x343; - uint128_t x345 = (uint128_t) (x344 >> 0x55); - uint128_t x346 = (uint128_t) x344 & 0x1fffffffffffffffffffffL; - uint256_t x347 = x345 + x338; - uint128_t x348 = (uint128_t) (x347 >> 0x55); - uint128_t x349 = (uint128_t) x347 & 0x1fffffffffffffffffffffL; - uint256_t x350 = x348 + x332; - uint128_t x351 = (uint128_t) (x350 >> 0x55); - uint128_t x352 = (uint128_t) x350 & 0x1fffffffffffffffffffffL; - uint128_t x353 = 0x5 * x351; - uint128_t x354 = x346 + x353; - uint128_t x355 = x354 >> 0x55; - uint128_t x356 = x354 & 0x1fffffffffffffffffffffL; - uint128_t x357 = x355 + x349; - uint128_t x358 = x357 >> 0x55; - uint128_t x359 = x357 & 0x1fffffffffffffffffffffL; - uint128_t x360 = x358 + x352; - uint256_t x361 = (uint256_t) x10 * x360; - uint256_t x362 = (uint256_t) x12 * x359; - uint256_t x363 = (uint256_t) x11 * x356; - uint256_t x364 = x362 + x363; - uint256_t x365 = x361 + x364; - uint256_t x366 = (uint256_t) x10 * x359; - uint256_t x367 = (uint256_t) x12 * x356; - uint256_t x368 = x366 + x367; - uint256_t x369 = (uint256_t) x11 * x360; - uint256_t x370 = 0x5 * x369; - uint256_t x371 = x368 + x370; - uint256_t x372 = (uint256_t) x10 * x356; - uint256_t x373 = (uint256_t) x12 * x360; - uint256_t x374 = (uint256_t) x11 * x359; - uint256_t x375 = x373 + x374; - uint256_t x376 = 0x5 * x375; - uint256_t x377 = x372 + x376; - uint128_t x378 = (uint128_t) (x377 >> 0x55); - uint128_t x379 = (uint128_t) x377 & 0x1fffffffffffffffffffffL; - uint256_t x380 = x378 + x371; - uint128_t x381 = (uint128_t) (x380 >> 0x55); - uint128_t x382 = (uint128_t) x380 & 0x1fffffffffffffffffffffL; - uint256_t x383 = x381 + x365; - uint128_t x384 = (uint128_t) (x383 >> 0x55); - uint128_t x385 = (uint128_t) x383 & 0x1fffffffffffffffffffffL; - uint128_t x386 = 0x5 * x384; - uint128_t x387 = x379 + x386; - uint128_t x388 = x387 >> 0x55; - uint128_t x389 = x387 & 0x1fffffffffffffffffffffL; - uint128_t x390 = x388 + x382; - uint128_t x391 = x390 >> 0x55; - uint128_t x392 = x390 & 0x1fffffffffffffffffffffL; - uint128_t x393 = x391 + x385; - return (Return x140, Return x139, Return x136, (Return x201, Return x200, Return x197), (Return x315, Return x314, Return x311, (Return x393, Return x392, Return x389)))) + uint128_t x236 = x229 + 0x5 * x234; + uint128_t x237 = x236 >> 0x55; + uint128_t x238 = x236 & 0x1fffffffffffffffffffffL; + uint128_t x239 = x237 + x232; + uint128_t x240 = x239 >> 0x55; + uint128_t x241 = x239 & 0x1fffffffffffffffffffffL; + uint128_t x242 = x240 + x235; + return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238)))) (x, (x0, x1), (x2, x3))%core in (let (a0, b0) := a in (a0, b0), let (a0, b0) := b in diff --git a/src/Specific/IntegrationTestSubDisplay.log b/src/Specific/IntegrationTestSubDisplay.log index 7bf04267e..ae675b0e7 100644 --- a/src/Specific/IntegrationTestSubDisplay.log +++ b/src/Specific/IntegrationTestSubDisplay.log @@ -2,38 +2,31 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - uint64_t x20 = 0xffffffffffffe + x10; - uint64_t x21 = x20 - x18; - uint64_t x22 = 0xffffffffffffe + x11; - uint64_t x23 = x22 - x19; - uint64_t x24 = 0xffffffffffffe + x9; - uint64_t x25 = x24 - x17; - uint64_t x26 = 0xffffffffffffe + x7; - uint64_t x27 = x26 - x15; - uint64_t x28 = 0xfffffffffffda + x5; - uint64_t x29 = x28 - x13; - uint64_t x30 = x29 >> 0x33; - uint64_t x31 = x29 & 0x7ffffffffffff; - uint64_t x32 = x30 + x27; - uint64_t x33 = x32 >> 0x33; - uint64_t x34 = x32 & 0x7ffffffffffff; - uint64_t x35 = x33 + x25; - uint64_t x36 = x35 >> 0x33; - uint64_t x37 = x35 & 0x7ffffffffffff; - uint64_t x38 = x36 + x23; - uint64_t x39 = x38 >> 0x33; - uint64_t x40 = x38 & 0x7ffffffffffff; - uint64_t x41 = x39 + x21; - uint64_t x42 = x41 >> 0x33; - uint64_t x43 = x41 & 0x7ffffffffffff; - uint64_t x44 = 0x13 * x42; - uint64_t x45 = x31 + x44; - uint64_t x46 = x45 >> 0x33; - uint64_t x47 = x45 & 0x7ffffffffffff; - uint64_t x48 = x46 + x34; - uint64_t x49 = x48 >> 0x33; - uint64_t x50 = x48 & 0x7ffffffffffff; - uint64_t x51 = x49 + x37; - return (x43, x40, x51, x50, x47)) + uint64_t x20 = 0xffffffffffffe + x10 - x18; + uint64_t x21 = 0xffffffffffffe + x11 - x19; + uint64_t x22 = 0xffffffffffffe + x9 - x17; + uint64_t x23 = 0xffffffffffffe + x7 - x15; + uint64_t x24 = 0xfffffffffffda + x5 - x13; + uint64_t x25 = x24 >> 0x33; + uint64_t x26 = x24 & 0x7ffffffffffff; + uint64_t x27 = x25 + x23; + uint64_t x28 = x27 >> 0x33; + uint64_t x29 = x27 & 0x7ffffffffffff; + uint64_t x30 = x28 + x22; + uint64_t x31 = x30 >> 0x33; + uint64_t x32 = x30 & 0x7ffffffffffff; + uint64_t x33 = x31 + x21; + uint64_t x34 = x33 >> 0x33; + uint64_t x35 = x33 & 0x7ffffffffffff; + uint64_t x36 = x34 + x20; + uint64_t x37 = x36 >> 0x33; + uint64_t x38 = x36 & 0x7ffffffffffff; + uint64_t x39 = x26 + 0x13 * x37; + uint64_t x40 = x39 >> 0x33; + uint64_t x41 = x39 & 0x7ffffffffffff; + uint64_t x42 = x40 + x29; + uint64_t x43 = x42 >> 0x33; + uint64_t x44 = x42 & 0x7ffffffffffff; + return (Return x38, Return x35, x43 + x32, Return x44, Return x41)) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) |