diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 01:24:49 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 01:24:49 -0500 |
| commit | 4cd3cf5521c2c2bf29ec8db127b1fbb59805d242 (patch) | |
| tree | 98ca7b67c437b7fad0e79bb38eaa2455e5a442fd /src/SpecificGen/GF5211_32Bounded.v | |
| parent | a408ad1ff2cd5ebc694ff8f5515922256b3beb2d (diff) | |
for i in *.json; do ./copy_bounds.sh $i; done
Diffstat (limited to 'src/SpecificGen/GF5211_32Bounded.v')
| -rw-r--r-- | src/SpecificGen/GF5211_32Bounded.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v index 3574afadc..d77609534 100644 --- a/src/SpecificGen/GF5211_32Bounded.v +++ b/src/SpecificGen/GF5211_32Bounded.v @@ -83,9 +83,11 @@ Definition postfreezeW : fe5211_32W -> fe5211_32W := Definition freezeW (f : fe5211_32W) : fe5211_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f). Local Transparent Let_In. -Definition powW (f : fe5211_32W) chain := fold_chain_opt (proj1_fe5211_32W one) mulW chain [f]. +(* Wrapper to allow extracted code to not unfold [mulW] *) +Definition mulW_noinline := mulW. +Definition powW (f : fe5211_32W) chain := fold_chain_opt (proj1_fe5211_32W one) mulW_noinline chain [f]. Definition invW (f : fe5211_32W) : fe5211_32W - := Eval cbv -[Let_In fe5211_32W mulW] in powW f (chain inv_ec). + := Eval cbv -[Let_In fe5211_32W mulW_noinline] in powW f (chain inv_ec). Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := change opW with (interp_rop); @@ -229,7 +231,7 @@ Lemma invW_correct_and_bounded : iunop_correct_and_bounded invW inv. Proof. intro f. assert (H : forall f, invW f = powW f (chain inv_ec)) - by abstract (cbv -[Let_In fe5211_32W mulW]; reflexivity). + by abstract (cbv -[Let_In fe5211_32W mulW_noinline]; reflexivity). rewrite H. rewrite inv_correct. cbv [inv_opt]. @@ -300,7 +302,7 @@ Definition sqrt_m1W : fe5211_32W := Definition GF5211_32sqrt x : GF5211_32.fe5211_32 := dlet powx := powW (fe5211_32ZToW x) (chain GF5211_32.sqrt_ec) in - GF5211_32.sqrt (fe5211_32WToZ powx) (fe5211_32WToZ (mulW powx powx)) x. + GF5211_32.sqrt (fe5211_32WToZ powx) (fe5211_32WToZ (mulW_noinline powx powx)) x. Definition sqrtW_sig : { sqrtW | iunop_correct_and_bounded sqrtW GF5211_32sqrt }. @@ -325,6 +327,7 @@ Proof. | [ |- is_bounded (fe5211_32WToZ ?op) = true ] => lazymatch op with | mulW _ _ => apply mulW_correct_and_bounded + | mulW_noinline _ _ => apply mulW_correct_and_bounded | powW _ _ => apply powW_correct_and_bounded | sqrt_m1W => vm_compute; reflexivity | _ => assumption |