From 2d6a0bfabd662a7cd567d39a13aed980f40f273b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 13 Mar 2018 15:58:35 -0400 Subject: Add commented out example of using the full end-to-end lemma inline --- src/Experiments/SimplyTypedArithmetic.v | 42 +++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) (limited to 'src') diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index d4ff6ed07..56dea254f 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -6329,6 +6329,48 @@ Module PrintingNotations. Notation "'MUL_256'" := (mul uint128 uint128 uint256) : nexpr_scope.*) End PrintingNotations. +(* +Notation "a ∈ b" := (ZRange.type.is_bounded_by b%zrange a = true) (at level 10) : type_scope. +Notation Interp := (expr.Interp _). +Notation "'ℤ'" := (type.type_primitive type.Z). +Set Printing Width 70. +Goal False. + let rop' := Reify (fun v1v2 : Z * Z => fst v1v2 + snd v1v2) in + pose rop' as rop. + pose (@Pipeline.BoundsPipeline_full + false (fun v => Some v) (type.Z * type.Z) type.Z + rop + (r[0~>10], r[0~>10])%zrange + r[0~>20]%zrange + ) as E. + simple refine (let Ev := _ in + let compiler_outputs_Ev : E = Pipeline.Success Ev := _ in + _); [ shelve | .. ]; revgoals. + clearbody compiler_outputs_Ev. + refine (let H' := + (fun H'' => + @Pipeline.BoundsPipeline_full_correct + _ _ + H'' _ _ _ _ _ _ compiler_outputs_Ev) _ + in _); + clearbody H'. + Focus 2. + { cbv [Pipeline.BoundsPipeline_full] in E. + remember (Pipeline.PrePipeline rop) as cache eqn:Hcache in (value of E). + lazy in Hcache. + subst cache. + lazy in E. + subst E Ev; reflexivity. + } Unfocus. + cbv [rop] in H'; cbn [expr.Interp expr.interp for_reification.ident.interp] in H'. +(* + H' : forall arg : type.interp (ℤ * ℤ), + arg ∈ (r[0 ~> 10], r[0 ~> 10]) -> + (Interp Ev arg) ∈ r[0 ~> 20] /\ + Interp Ev arg = fst arg + snd arg +*) +Abort. +*) Module X25519_64. Definition n := 5%nat. -- cgit v1.2.3