Version 1.3 release

shentufoundation · Jan 28, 2021 · 25a3636 · 25a3636
1 parent b399696
commit 25a3636
Show file tree

Hide file tree

Showing 250 changed files with 67,025 additions and 8,736 deletions.
diff --git a/DeepSEA language reference.pdf b/DeepSEA language reference.pdf
diff --git a/binaries/MacOS/dsc b/binaries/MacOS/dsc
diff --git a/binaries/MacOS/dsc_antchain b/binaries/MacOS/dsc_antchain
diff --git a/binaries/MacOS/minicc b/binaries/MacOS/minicc
diff --git a/binaries/linux/dsc b/binaries/linux/dsc
diff --git a/binaries/linux/dsc_antchain b/binaries/linux/dsc_antchain
diff --git a/binaries/linux/minicc b/binaries/linux/minicc
diff --git a/contracts/amm/amm/RefineAMM.v b/contracts/amm/amm/RefineAMM.v
@@ -0,0 +1,259 @@
+(* WARNING: This file is generated by Edsger, the DeepSEA compiler.
+            All modification will be lost when regenerating. *)
+(* Module amm.RefineAMM for amm.ds *)
+Require Import BinPos.
+Require Import DeepSpec.Runtime.
+Require Import DeepSpec.Linking.
+Require Import amm.EdsgerIdents.
+Require Import amm.DataTypes.
+Require Import amm.DataTypeOps.
+Require Import amm.DataTypeProofs.
+Require Import layerlib.LayerCalculusLemma.
+Require Import layerlib.RefinementTactic.
+Require Import layerlib.RefinementTacticAux.
+Require Import liblayers.compcertx.MakeProgram.
+Require Import liblayers.compcertx.MemWithData.
+
+Require Import amm.LayerAMM.
+Require Import amm.LSimAMMLIB.
+
+Section EdsgerGen.
+
+
+Context {mem}`{Hmem: Mem.MemoryModel mem}.
+Context`{Hmwd: UseMemWithData mem}.
+Context`{make_program_ops: !MakeProgramOps Clight.function Ctypes.type Clight.fundef Ctypes.type}.
+Context`{Hmake_program: !MakeProgram Clight.function Ctypes.type Clight.fundef Ctypes.type}.
+Instance GlobalLayerSpec : LayerSpecClass := {
+  make_program_ops := make_program_ops;
+  Hmake_program := Hmake_program;
+  GetHighData := global_abstract_data_type
+}.
+Context`{global_abdata : !GlobalAbData init_global_abstract_data global_low_level_invariant}.
+Context`{CTXT_prf : !Layer_AMM_Context_prf}.
+Context`{AMMLIB_pres_inv : !AMMLIB_preserves_invariants}.
+Context`{AMM_pres_inv : !AMM_preserves_invariants}.
+
+Existing Instances AMM_overlay_spec AMM_underlay_spec.
+
+Record relate_RData (j : meminj) (habd : GetHighData) (labd : GetLowData) : Prop
+    := mkrelate_RData {
+  (* FixedSupplyToken *)
+  FixedSupplyToken__totalSupply_re : ;
+  FixedSupplyToken_balances_re : ;
+  FixedSupplyToken_allowances_re : ;
+  (* FixedSupplyToken1 *)
+  FixedSupplyToken1__totalSupply_re : ;
+  FixedSupplyToken1_balances_re : ;
+  FixedSupplyToken1_allowances_re : ;
+  (* LiquidityToken *)
+  LiquidityToken__totalSupply_re : ;
+  LiquidityToken_balances_re : ;
+  LiquidityToken_allowances_re : 
+}.
+
+Record match_RData (habd : GetHighData) (m : mem) (j : meminj) : Prop
+    := MATCH_RDATA {
+  AutomatedMarketMaker__token0_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker__token0_var habd m;
+  AutomatedMarketMaker__token1_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker__token1_var habd m;
+  AutomatedMarketMaker__owner_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker__owner_var habd m;
+  AutomatedMarketMaker__reserve0_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker__reserve0_var habd m;
+  AutomatedMarketMaker__reserve1_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker__reserve1_var habd m;
+  AutomatedMarketMaker_blockTimestampLast_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker_blockTimestampLast_var habd m;
+  AutomatedMarketMaker_price0CumulativeLast_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker_price0CumulativeLast_var habd m;
+  AutomatedMarketMaker_price1CumulativeLast_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker_price1CumulativeLast_var habd m;
+  AutomatedMarketMaker_kLast_ma : variable_match AutomatedMarketMaker_AutomatedMarketMaker_kLast_var habd m
+}.
+
+Local Hint Resolve MATCH_RDATA.
+
+Global Instance rel_ops: CompatRelOps GetHighDataX GetLowDataX :=
+{
+  relate_AbData f d1 d2 := relate_RData f d1 d2;
+  match_AbData d1 m f := match_RData d1 m f;
+  new_glbl := var_AutomatedMarketMaker_AutomatedMarketMaker__token0_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker__token1_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker__owner_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker__reserve0_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker__reserve1_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker_blockTimestampLast_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker_price0CumulativeLast_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker_price1CumulativeLast_ident :: var_AutomatedMarketMaker_AutomatedMarketMaker_kLast_ident :: nil
+}.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker__token0_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker__token0_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker__token0_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker__token1_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker__token1_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker__token1_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker__owner_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker__owner_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker__owner_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker__reserve0_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker__reserve0_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker__reserve0_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker__reserve1_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker__reserve1_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker__reserve1_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker_blockTimestampLast_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker_blockTimestampLast_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker_blockTimestampLast_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker_price0CumulativeLast_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker_price0CumulativeLast_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker_price0CumulativeLast_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker_price1CumulativeLast_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker_price1CumulativeLast_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker_price1CumulativeLast_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Global Instance AutomatedMarketMaker_AutomatedMarketMaker_kLast_hyper_ltype_static :
+    HyperLTypeStatic AutomatedMarketMaker_AutomatedMarketMaker_kLast_var new_glbl.
+Proof.
+  split; try solve
+    [ Decision.decision
+    | simpl; auto
+    | simpl AutomatedMarketMaker_AutomatedMarketMaker_kLast_var.(ltype_offset);
+      rewrite Int256.unsigned_zero; apply Z.divide_0_r ].
+Qed.
+
+Lemma relate_incr:
+  forall abd abd' f f',
+    relate_RData f abd abd' ->
+    inject_incr f f' ->
+    relate_RData f' abd abd'.
+Proof.
+  inversion 1; subst; intros; simpl in *.
+  repeat match goal with
+  | H : _ /\ _ |- _ => destruct H
+  end.
+  repeat (constructor; simpl; eauto).
+Qed.
+Global Instance rel_prf: CompatRel GetHighDataX GetLowDataX.
+Proof.
+  constructor; [ destruct 1 .. |]; intros.
+  - constructor; eapply inject_match_correct; eauto with typeclass_instances.
+  - constructor; eapply store_match_correct; eauto with typeclass_instances.
+  - constructor; eapply alloc_match_correct; eauto with typeclass_instances.
+  - constructor; eapply free_match_correct; eauto with typeclass_instances.
+  - constructor; eapply storebytes_match_correct; eauto with typeclass_instances.
+  - eapply relate_incr; eauto.
+Qed.
+
+(*
+Local Instance: ExternalCallsOps (mwd GetLowDataX) := CompatExternalCalls.compatlayer_extcall_ops AMMLIB_Layer.
+Local Instance: CompilerConfigOps _ := CompatExternalCalls.compatlayer_compiler_config_ops AMMLIB_Layer.
+*)
+
+Instance AMM_hypermem : MemoryModel.HyperMem
+  := { Hcompatrel := {| crel_prf := rel_prf |} }.
+
+Class AMM_Underlay_preserves_invariants := {
+  AMM_Underlay_FixedSupplyToken_constructor_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken_constructor_spec | 5;
+  AMM_Underlay_FixedSupplyToken_balanceOf_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken_balanceOf_spec | 5;
+  AMM_Underlay_FixedSupplyToken_transfer_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken_transfer_spec | 5;
+  AMM_Underlay_FixedSupplyToken_approve_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken_approve_spec | 5;
+  AMM_Underlay_FixedSupplyToken_transferFrom_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken_transferFrom_spec | 5;
+  AMM_Underlay_FixedSupplyToken1_constructor_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken1_constructor_spec | 5;
+  AMM_Underlay_FixedSupplyToken1_balanceOf_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken1_balanceOf_spec | 5;
+  AMM_Underlay_FixedSupplyToken1_transfer_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken1_transfer_spec | 5;
+  AMM_Underlay_FixedSupplyToken1_approve_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken1_approve_spec | 5;
+  AMM_Underlay_FixedSupplyToken1_transferFrom_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) FixedSupplyToken1_transferFrom_spec | 5;
+  AMM_Underlay_LiquidityToken_constructor_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_constructor_spec | 5;
+  AMM_Underlay_LiquidityToken_mint_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_mint_spec | 5;
+  AMM_Underlay_LiquidityToken_burn_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_burn_spec | 5;
+  AMM_Underlay_LiquidityToken_totalSupply_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_totalSupply_spec | 5;
+  AMM_Underlay_LiquidityToken_balanceOf_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_balanceOf_spec | 5;
+  AMM_Underlay_LiquidityToken_transfer_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_transfer_spec | 5;
+  AMM_Underlay_LiquidityToken_approve_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_approve_spec | 5;
+  AMM_Underlay_LiquidityToken_transferFrom_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) LiquidityToken_transferFrom_spec | 5;
+  AMM_Underlay_AutomatedMarketMakerLib_constructor_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) AutomatedMarketMakerLib_constructor_spec | 5;
+  AMM_Underlay_AutomatedMarketMakerLib_getAmountIn_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) AutomatedMarketMakerLib_getAmountIn_spec | 5;
+  AMM_Underlay_AutomatedMarketMakerLib_getBalanceAdjusted_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) AutomatedMarketMakerLib_getBalanceAdjusted_spec | 5;
+  AMM_Underlay_AutomatedMarketMakerLib_min_preserves_invariants :>
+    CompatGenSem.PreservesInvariants (HD := cdataLow) AutomatedMarketMakerLib_min_spec | 5
+}.
+Instance AMM'AMMLIB_preserves_invariants : AMM_Underlay_preserves_invariants.
+Proof. esplit; apply AMMLIB_pres_inv. Defined.
+
+(*
+Lemma passthrough_correct:
+  sim (crel (CompatRel0 := rel_prf) _ _) AMM_Layer_passthrough AMMLIB_Layer.
+Proof.
+  Local Opaque simRR mapsto layer_mapsto_primitive.
+  unfold GlobalLayerSpec, MemoryModel.GetHighDataX.
+  simpl.
+
+  sim_oplus; simpl.
+
+  Local Transparent simRR mapsto layer_mapsto_primitive.
+Qed.*)
+End EdsgerGen.